Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Constr et kind_of_term

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Constr et kind_of_term


chronological Thread 
  • From: "Devisschere Yann" <devissch AT enseirb.fr>
  • To: <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] Constr et kind_of_term
  • Date: Fri, 15 Apr 2005 16:58:50 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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



Archive powered by MhonArc 2.6.16.

Top of Page