Pierre Boutillier writes: Why do we keep a camlp5 in transitionnal mode ? I assumed somebody needs transitional mode. Supporting only strict mode is of course much simpler. For packages, Coq and ledit support strict mode. The only remaining question is about ulex. How about ssreflect? Bye, Hendrik