aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
AgeCommit message (Collapse)Author
2003-03-01Added some tests to make more robust the tactique "Functionalcourtieu
Induction". Namely: check that the given function is a really a constant, and check that the number of given argument is exactly the arity of the given function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3723 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Adding tests for the "functional induction" facility.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot
for recursive functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3710 85f007b7-540e-0410-9357-904b9bb8a0f7