aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
AgeCommit message (Expand)Author
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-29Obsolete, cf Funind.v dans test-suiteherbelin
2003-11-27Retour des _eq en v8herbelin
2003-11-12petits changements de syntaxebarras
2003-10-07Compatibilite V7 des noms d'hypothesesherbelin
2003-10-03Cacher les .v8herbelin
2003-10-02Plus de nom commencant par '_' en V8herbelin
2003-09-12Simplification vis a vis de Declareherbelin
2003-06-10Typoherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
2003-03-01Added some tests to make more robust the tactique "Functionalcourtieu
2003-02-27Adding tests for the "functional induction" facility.bertot
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 02:36:07 +0000