aboutsummaryrefslogtreecommitdiff
path: root/contrib/recdef
AgeCommit message (Collapse)Author
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
apply afin de reculer au plus tard les décisions irréversibles et en particulier de pouvoir typer les with-bindings modulo coercions : - l'unification des types des métas données en with-bindings est retardé à après l'unification (unify_0) de telle sorte que les instances trouvées par unify_0 soient prioritaires et que la décision d'insérer éventuellement des coercions autour des valeurs données en with-bindings se fasse au dernier moment; - toujours pour permettre d'insérer ultimement des coercions, l'instantiation des with-bindings ne se fait plus l'appel unify_0 (cf clenv_unique_resolver); - pour permettre ce retardement sans limiter le test de conversion que unify_0 fait sur les termes clos, on transmet à unify_0 les métas données en with-bindings (ainsi l'instantiation de ces métas peut être faite dynamiquement au moment du test de clôture); - parce que les métas données en with-bindings qui sont en position de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent simplifier le problème d'unification (et elles ne sont pas de toutes façons pas réinférables au premier ordre), on continue à les substituer avant l'appel à unify_0 (cf meta_reducible_instance); - pour l'unification du second-ordre, on continue d'instancier les with-bindings et d'unifier les types des with-bindings avant unification; - reste à régler un problème de compatibilité lorsque le résultat de l'unification des types des with-bindings est utilisé pour rendre un terme clos et pour permettre à unify_0 d'utiliser la conversion. + meilleure compatibilité de apply, split, left, right pour le code qui l'utilise avec des bindings clos + nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9850 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
de résoudre des buts comme celui-ci : Record nat_retract : Type := {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}. Goal nat_retract. exists (fun x => x) (fun x => x). - Nouvelle tentative d'utilisation des types des metas/evars pour inférer de nouvelles instances de metas/evars; permet par exemple d'utiliser f_equal sans option with, mais aussi, avec la modif précédente, de résoudre des buts tels que Goal exists f:bool->Prop, f true = True. exists (fun x => True). [Les expériences passées avaient montré qu'en prenant en compte les types dans l'unification, on peut unifier trop tôt une evars à une mauvaise sorte; à défaut de mécanisme de prise en compte des problème d'unification avec sous-typage, on s'est interdit ici d'unifier des types qui sont des arités.] - Tout les constr de tactic_expr deviennent des open_constr (même si seul with_bindings les accepte au final... c'est pas l'idéal). - Renommage env -> evd et templenv -> env dans clausenv. - Renommage closed_generic_argument -> typed_generic_argument. - Renommage closed_abstract_argument_type -> typed_abstract_argument_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-17correction de bug dans Function et augmentation de la classe des fonctions ↵jforest
supportees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9833 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-05Mise en place d'une nouvelle strategie plus efficace pour les preuves de ↵jforest
Function. => Changement d'ordre et de forme des obligations de preuve generees (pas de la semantique des obligations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9746 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-11correction du bug 1432jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9696 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-26Contounement d'un probleme avec la VM dans Function jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9538 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
(suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-19Gestion des arguments implicites dans les Functions bien fondeesjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9152 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-18correction of bug #1220jforest
adding a "using" optional argument to Function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9150 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-16Message modification in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9148 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-15Minor bug correction in well-founded Function.jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9143 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-25two minor bug corrections in General Recursive Functions jforest
and one un structural Functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9084 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la ↵jforest
generation des graphes de Function + Correction d'un petit bug dans les lemmes d'inversions de Function + Nettoyage d'hypotheses inutile dans les obligations de preuve de Function (wf et measure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9069 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-11Bug corrections in Function.jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9065 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-08In the old version, recursive functions cannot be declared inside a sectionbertot
when the termination argument is based on the fact that some relation is well-founded. The goal correspond to the proof that the relation is well-founded is cleared of all useless hypotheses and variables, including variables that maybe used in the intermediary lemma that gathers all the proofs that need to be done interactively. As a result, this intermediary lemma cannot be re-used to prove this goal. The message is: Error: No such section variable or assumption : A This message appears at the time the user send the Qed command. This is problem report #PR1202 submitted by X. Leroy. The correction is to use the list of input variables to the function as the list of variables that should be cleared from the context. The function tclUSER_if_not_mes needs to be modified. This function is also used in contrib/funind/functional_principles_proofs.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9064 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26removing a warningjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8862 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Error during last commit (coq didn't compile)jforest
Bug correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8851 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23cleanning code jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8847 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-22Correcting a bug in identifiers manipulation jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8842 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-09Correcting an old bug during generation of generale recursive functions.jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8798 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-07+ correcting a bug in general recursive function (match e with _ => match f ↵jforest
e with .... end end was not correctly treated) + cleaning dead code in functional_principles_proofs.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8797 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-03Fixing two minor bugs in recdef and graph of function generation. jforest
Fixing .depend (forgot to remove new_arg_principles dependencies in last commit ) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8786 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into ↵jforest
to files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8781 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28If function creates proof obligation, there are now printed once.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8769 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-10+ Changing a little functional schemes types jforest
+ New tactic to prove functions schemes + Add a command "Generate graph for <functionname>" to generate automatiquelly the graph associated to a function (usefull only when the function has not been defined by GenFixpoint). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8694 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default ↵msozeau
uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-17bug correctionbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8056 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-09securing intros (we now use h_intro)bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8018 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-09Minor bugs fixesbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8017 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Changing Set to Type for iter.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8014 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-03+ Adding an error message when the function cannot be definedbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7979 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-18Recursive Definition now supports functions with more than one argument.coq
Julien git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7887 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-12Changing well founded induction to fix on accessibility proof in orderbertot
to prepare the possibility to define function with more that one argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7856 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11removes several warnings in contrib/interfacebertot
Modifies the behavior of Recursive definition to produce goals instead of established theorems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7843 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-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-11-14avoids warnings about unused variablesbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7562 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-07Adds tools to help in defining new general recursive functionsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7527 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 17:06:41 +0000