aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
maintenant écrire des fonctions récursives qui n'ont pas l'apparence d'être fonctionnelle. La sémantique reste toutefois différente. Par exemple, dans Ltac is := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. l'évaluation de i est paresseuse, alors que dans une version non récursive Ltac is := let i := match goal with |- ?A -> ?B => intro | _ => idtac end in i. l'évaluation de i est forte (et échoue sur le "match" qui n'est pas autorisé à retourner une tactique). (note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-31Debug implementation of dependent induction/dependent destruction and ↵msozeau
document it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Support for occurences and 'in' in class_setoid, work on corresponding ↵msozeau
tactics in SetoidClass git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10486 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Add occurence extra argmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10483 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ↵msozeau
wrapper around Ltac program_simpl ::= . !!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18bug in accessing n-th abstractionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10451 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ↵msozeau
Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-15Generalize instance declarations to any context, better name handling. Add ↵msozeau
hole kind info for topconstrs. Derive eta_expansion from functional extensionality axiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but ↵msozeau
implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Move Classes.Setoid to Classes.SetoidClass to avoid name clash.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10411 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
Variable, et plus de trucs useless qui traînaient par ma faute (y compris dans le noyau, la honte). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-07Adding the tactic "instantiate" (without argument), to force theglondu
instantiation of evars in tacticals (cf r9985, r10294). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10356 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
Au passage, un peu plus de standardisation des noms de fonctions de globalisation Principe de base : locate_foo : qualid -> foo (échoue avec Not_found) global : reference -> global_reference (échoue avec UserError) global_of_foo : foo -> global_reference (échoue avec UserError) f_with_alias : se comporte comme f mais prenant aussi en compte les notations de la forme "Notation id:=ref" Principale exception : locate, au lieu de locate_global locate_global_with_alias, qui prend en entrée un "qualid located" Restent beaucoup de fonctions qui pourraient utiliser global_with_alias au lieu de global, notamment dans contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-27Réparation d'une inefficacité bêtement introduite dans la révisionherbelin
10222: n'évaluer les std_ppcmds que si vraiment ils sont utilisés (en particulier, les [< ... >] sont paresseux comme on l'attend mais pas les ++). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10267 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-24Bugfix in abstract_generalizemsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10259 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-12- Préservation des appels récursifs de tête dans ltac (réponse au "wish"herbelin
implicite du rapport de bug #468); utilisation pour cela d'un mécanisme différent de localisation des échecs Ltac (mécanisme probablement à affiner). - Factorisation au passage des appels au débuggeur Ltac. - Trivialités en passant dans clenv.ml. - Tentative de documentation de l'infâme Reductionops.instance et essai de déplacement plus amont du test "s = []". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10222 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-12Uniformisation du comportement de rewrite et rewrite in : quand leherbelin
filtrage d'ordre 2 échoue à trouver un prédicat de réécriture qui n'est pas une K-abstraction, les deux rewrite essaie alors le filtrage d'ordre 1. Ce n'est pas le plus élégant mais c'est la solution uniforme permettant d'être conservatif. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10221 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-10Allowing setoid_reflexivity_in to work on quantified hypothesis (bug #1710) letouzey
(patch by J. Forest) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10212 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
decidability of the usual equality Major changes: * andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v * added 2 files: * toplevel/ind_tables.ml* : tables where the boolean eqs and the decidability proofs are stored * toplevel/auto_ind_decl.ml* : code of the schemes that are automatically generated from inductives types (currently boolean eq & decidability ) * improvement of injection: if the decidability have been correctly computed, injection can now break the equalities over dependant pair How to use: Set Equality Scheme. to set the automatic generation of the equality when you create a new inductive type Scheme Equality for I. tries to create the equality for the already declared type I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
Ajout de l'option with à (e)destruct et (e)induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-02Correcting error message when adding Setoid, Relation or morphism (bug #1626)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10162 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-30Suite de 10157herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10157 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
Printing Universes est active. Ajout de l'option "using" à la tactique non documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto decomp" avec des principes élémentaires tels que le dépliage de "iff". Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28On empêche "fresh" d'engendrer un mot-clé.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10154 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-27Découpage de Setoid.vnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10147 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
the latter is bound to a var which is not a quantified one - this led to remove a line marked "temporary compatibility" ... ; made a distinction between quantified hypothesis as for "intros until" and binding names as in "apply with"; in both cases, we now expect that a identifier not used as a variable, as in "apply f_equal with f:=g" where "f" is a true binder name in f_equal, must not be used as a variable elsewhere [see corresponding change in Ints/Tactic.v]) - Fixing bug 1643 (bug in the algorithm used to possibly reuse a global name in the recursive calls of a coinductive term) - Fixing bug 1699 (bug in contracting nested patterns at printing time when the return clause of the subpatterns is dependent) - Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic) - Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-17Raffinement de l'algorithme d'inférence de typeherbelin
----------------------------------------------- - Les fonctions evar_define et real_clean font un travail plus fin : - S'il y a plusieurs manières d'inverser l'instance d'une evar, on retarde le choix au lieu de faire un choix arbitraire. - Si l'instance contient une evar et que cette evar n'est pas inversible, on essaie aussi d'inverser ou de restreindre (un sous-terme) de l'evar qui était initialement à instancier. - Incidemment, real_clean est renommé en invert_instance, un nom qui reflète mieux la diversité du travail fait par ce fameux real_clean. - La fonction solve_refl garde les problèmes qui contiennent encore de l'information. - Changements secondaires : - Délégation de la gestion des variables modifiées et des problèmes à reconsidérer (get_conv_pbs) à Evd (qui s'en charge par effet de bord au moment du define) (incidemment get_conv_pbs devient extract_conv_pbs) - Essai d'un mécanisme différent de restriction des evars : pour éviter des contextes mal formés (comme do_restrict pouvait a priori le faire), on utilise maintenant un contexte bien formé doublé d'un filtre signalant les instances interdites. C'est a priori plus souple (par ex : si une variable du contexte a un type dépendant d'une evar, on peut attendre de connaître cette evar avec de déterminer si cette variable du contexte, qui peut-être dépend via cette evar d'une autre variable interdite, doit être finalement interdite ou pas) - Nettoyages divers. - Ce que evarutil ne fait toujours pas : - Utiliser l'inversion et/ou l'unification d'ordre supérieur (par exemple pour résoudre "?ev[S n]=n"); en particulier, la notion d'inversion unique ne prend pas en compte l'unification d'ordre supérieur et peut donc faire des choix irréversibles vis à vis de l'unif d'ordre supérieur. - Utiliser (systématiquement -- et précautionneusement) les types des solutions trouvées pour résoudre davantage de problèmes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10124 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-22Correction du bug #1634 + ajout de bugs dans la test-suitenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-16Correction du bug #1322notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-16Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;notin
modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Add a new tactic to generalize an instantiated inductive predicate adding ↵msozeau
equalities. Useful to do so-called "ford" induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10059 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
Cleaner code: the guardedness bug is now corrected. Added "trivial" to the automation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-18Raffinement de interp_ident pour que l'ident interprété soit au choixherbelin
frais (par exemple pour "intro") ou pas forcément (par exemple pour "fresh") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10021 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
utilities from Util. Some additions in Util, and simplifications in various files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
rename A into B, C into D, E into F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9952 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26killing some more non-exhaustive patternsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9912 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-20ajout de head0 et tail0 en natifbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
(cas d'un terme sans Rel libre), introduction au passage d'un nouveau type d'evar EvarGoal pour raffinement du message d'erreur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
métas permettant de savoir si une instance de méta vient d'un with-binding ou d'une unification, et si elle a déjà été typée ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28Retour à un message d'erreur d'apply qui montre un échec sans sans réduction herbelin
de la conclusion du lemme git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9865 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-23A fix for bug #1397: letouzey
setoid_reflexivity may discover it is doing plain Leibniz stuff (see exception Optimize in setoid_replace), and falls back to the usual reflexivity. Except that this one, due to the lack of delta-red, refuses to handle the job, and gives it back to setoid_reflexivity: a loop is born. quick fix for the moment: add some whd_betadeltaiota to reflexivity in the special situation where reflexivity is called back by setoid_reflexivity. Similar issue & fix for symmetry, transitivity. rewrite has potentially the same problem, but I can't manage to trigger a wild loop in practice. This code clearly deserves a closer look someday... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9852 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-12 10:31:41 +0000