The Coq mailing list

["Devisschere Yann" <devissch AT enseirb.fr>]

I'd like to know if the view kind_of_term and the constructors mklambda, mkprod, mkind, mkrel... is will remain among the different version of coq or if it could change.

 

In fact I'm working on generating lemmas and their proofs from a definition. I first did a ML module that allows me to generate the lemmas and proofs by a new command added in coq with VERNAC COMMAND EXTEND and which parameter is the definition name.

I'd like to keep valid my code among version and I'm wondering if the constr and kind_of_term will remain or if it would be better to externally generate a coq file by preprossessing a basic file containig only my definition.

 

Thanks