There is a consolidated tendency to rely onto #if instead of #ifdef, and I believe it would be a nice thing if we follow the common practices. Currently, the STRONG_NORMALIZATION symbol is the only one that needs to be cured. The symbol definition should also be commented so that the comment shows up in the developer's manual. Ciao Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it