aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
AgeCommit message (Collapse)Author
2006-03-14+ Debugging and cleaning functional principle generation tacticjforest
+ New functional induction now calls induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8627 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-12 -Debugging multiple induction, a bug appeared when having functioncourtieu
arguments to a principle (like in map_ind). -Added nbranches and npredicates to elim_scheme, and made the elimc field optional. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8622 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-10cleaning jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8620 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-07Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain ↵jforest
is_empty in those versions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8616 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-22Julien:bertot
+ Induction principle for general recursion + Bug correction in structural principles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8076 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17Julien:bertot
+ Compatibility with new induction + Induction principle for general recursion preparation still continuing + Cleaning dead code ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8055 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-17changed the decomposition of an induction schemecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8052 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-09very minor bug correction and cleanningbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8019 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08One can use a measure {mes f x} instead of a well-founded relation in ↵bertot
GenFixpoint. If the function takes only one argument, it can be deleted from the wf/mes part. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8013 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Julien:bertot
+ Recursive definition (repository contrib/recdef) can now be used with GenFixpoint syntax by just replacing the usual {struct x} annotation by {wf R x} where x is one of the function declared arguments and R is a expression well-typed in the x typing environment. + Bug correction in new functional induction + For now no induction principle for general recursive definition is generated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8012 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-03added mli 's for the nex functional induction (forgotten last time).coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7980 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-01New version of functional induction / inversion. By Julien Forest,coq
Benjamin Gregoire, Gilles Barthe. For the moment, it is as followed: If one uses GenFixpoint instead of Fixpoint, then induction principles are generated on the fly (respecting the match structure written by the user, with wildcards etc). These principles can be used directly or by tactics "new functional induction" and "functional inversion". We will soon make "new functional induction" become "functional induction", before release of V8.1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7972 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ↵herbelin
et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-08More exception handling in functional scheme.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7643 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-16changed the syntax categories of arguments of functional schemecoq
(constr --> ident). Transparent for the user. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7383 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-18code cleaning. No changes as far as tested.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7302 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Correction of a bug in functional scheme. It raised with mutualcoq
functions with imbricated recursive calls. Two bugs in one actually, one in the building of the set of recursive functions, and one with De Bruijn indices when looking for recursve calls. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7080 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Uniformisation de destApplication en destAppherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-10Hugo fixed a bug of refine, and it revealed a bug of functionalcoq
induction. Some metas were left in the type of metas of the term given to refine by functional induction. This commit fixes this bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6462 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6420 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6033 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-13"comments only" commit.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5744 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-10Correction of a bug in Functional Scheme discovered when porting thecoq
contrib QArith. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5313 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
more functions (higher order and polymorphic functions), the principle is a bit better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5310 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Obsolete, cf Funind.v dans test-suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5037 85f007b7-540e-0410-9357-904b9bb8a0f7
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-03-01 15:23:04 +0000