coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
|
- [Coq-Club] Constr et kind_of_term, Devisschere Yann
- Re: [Coq-Club] Constr et kind_of_term, Claudio Sacerdoti Coen
Archive powered by MhonArc 2.6.16.