aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/tacinv.ml4
Commit message (Expand)AuthorAge
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* Correcting a bug occuring when the mimicked function had aGravatar courtieu2003-03-31
* Added some tests to make more robust the tactique "FunctionalGravatar courtieu2003-03-01
* The contribution of Pierre Courtieu on generating specialized induction schemesGravatar bertot2003-02-27