aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind
Commit message (Expand)AuthorAge
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* 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
* Added some tests to make more robust the tactique "FunctionalGravatar courtieu2003-03-01
* Adding tests for the "functional induction" facility.Gravatar bertot2003-02-27
* The contribution of Pierre Courtieu on generating specialized induction schemesGravatar bertot2003-02-27