aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/tacinvutils.ml
Commit message (Expand)AuthorAge
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Correcting a bug occuring when the mimicked function had aGravatar courtieu2003-03-31
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* The contribution of Pierre Courtieu on generating specialized induction schemesGravatar bertot2003-02-27