aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/tacinv.ml4
AgeCommit message (Expand)Author
2006-05-31Replacing the old version of "functional induction" with the new one. jforest
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into to...jforest
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-08More exception handling in functional scheme.coq
2005-09-16changed the syntax categories of arguments of functional schemecoq
2005-08-18code cleaning. No changes as far as tested.coq
2005-05-26Correction of a bug in functional scheme. It raised with mutualcoq
2005-02-12Uniformisation de destApplication en destAppherbelin
2004-12-10Hugo fixed a bug of refine, and it revealed a bug of functionalcoq
2004-12-06Code mortherbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-08-24Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1herbelin
2004-02-10Correction of a bug in Functional Scheme discovered when porting thecoq
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
2003-11-27Retour des _eq en v8herbelin
2003-11-12petits changements de syntaxebarras
2003-10-07Compatibilite V7 des noms d'hypothesesherbelin
2003-10-02Plus de nom commencant par '_' en V8herbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
2003-03-01Added some tests to make more robust the tactique "Functionalcourtieu
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 06:59:35 +0000