aboutsummaryrefslogtreecommitdiff
path: root/tactics/decl_proof_instr.mli
AgeCommit message (Expand)Author
2009-10-27fix previous commitcorbinea
2009-10-27fixed czar bug with parametric inductivescorbinea
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
2007-04-26fin des conclusions multiplescorbinea
2007-01-25decl mode: anonymous factscorbinea
2006-09-20Declarative Proof Language: main commitcorbinea