aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/decl_proof_instr.mli
Commit message (Expand)AuthorAge
* fix previous commitGravatar corbinea2009-10-27
* fixed czar bug with parametric inductivesGravatar corbinea2009-10-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
* fin des conclusions multiplesGravatar corbinea2007-04-26
* decl mode: anonymous factsGravatar corbinea2007-01-25
* Declarative Proof Language: main commitGravatar corbinea2006-09-20