aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/tacinvutils.ml
AgeCommit message (Expand)Author
2003-09-12Simplification vis a vis de Declareherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
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-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot