aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
AgeCommit message (Collapse)Author
2003-11-27Retour des _eq en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5010 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Compatibilite V7 des noms d'hypothesesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4533 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Plus de nom commencant par '_' en V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4513 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Simplification vis a vis de Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4355 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4134 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
lambda-abstraction inside a Cases. I had to make the term of the induction principle a bit less clean (more eta expansions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3817 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 19:12:48 +0000