aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml4
Commit message (Collapse)AuthorAge
...
* Minor unification changes:Gravatar msozeau2009-05-18
| | | | | | | | | | | | | - Primitive setup for firing typeclass resolution on-demand: add a flag to control resolution of remaining evars (e.g. typeclasses) during unification. - Prevent canonical projection resolution when no delta is allowed during unification (fixes incompatibility found in ssreflect). - Correctly check types when the head is an evar _or_ a meta in w_unify. Move [isEvar_or_Meta] to kernel/term.ml, it's used in two places now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
| | | | | | | | | - Set implicit args on for Context decls - Move class_apply tactic to Init - Normalize evars before raising an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12127 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
| | | | | | | | | | | | | as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in typeclasses eauto and generalized rewriting:Gravatar msozeau2009-05-05
| | | | | | | | | | | | | - Decorate proof search with depth/subgoal number information - Add a tactic [autoapply foo using hints] to call the resolution tactic with the [transparent_state] associated with a hint db, giving better control over unfolding. - Fix a bug in the Lambda case in the new rewrite - More work on the [Proper] and [subrelation] hints to cut the search space while retaining completeness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for bugs in r12110:Gravatar msozeau2009-04-28
| | | | | | | | | | - [matches] is not parameterized by evars: normalize before calling conclPattern. - fix hints in Morphisms for subrelation and handling of signature normalization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup old eauto code.Gravatar msozeau2009-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12111 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
| | | | | | | | | | | and failure continuations, allowing to do safe cuts correctly. - Fix bug #2097 by suppressing useless nf_evars calls. - Improve the proof search strategy used by rewrite for subrelations and fix some hints. Up to 20% speed improvement in setoid-intensive files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
| | | | | | | | | | | | | | This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move setoid_rewrite to its own module and do some clean up inGravatar msozeau2009-04-07
| | | | | | | class_tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
| | | | | | | | | | | | | | now works correctly, "unfold foo at 4 in H at 3" now fails correctly, etc.). The terminology for clauses (though I don't find the term "clause" very intuitive after all) is mostly preserved except for "simple_clause" which becomes a light form of "clause" instead of being an atom of clause (what played the role of "simple_clause" is now called "goal_location" - better names are welcome). Main changes are in tacticals.ml and tactics.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11981 85f007b7-540e-0410-9357-904b9bb8a0f7
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | par Evd). Ça s'accompagne de quelques autres modifications de l'interface (certaines fonctions étaient des doublons, ou des conversions entre evar_map et evar_defs). J'ai modifié un peu la structure de evd.ml aussi, pour éviter des fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai introduit des sous-modules pour les différentes couches. Il y a à l'heure actuelle une pénalité en performance assez sévère (due principalement à la nouvelle mouture de Evd.merge, si mon diagnostique est correct). Mais fera l'objet de plusieurs optimisations dans les commits à venir. Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un appel de Decl_proof_instr.mark_as_done visiblement, je suis pour l'instant incapable de comprendre ce qui cause cette erreur. J'espère qu'on pourra le déterminer rapidement. Ce commit est le tout premier commit dans le trunk en rapport avec les évolution futures de la machine de preuve, en vue en particulier d'obtenir un "vrai refine". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
* pushed evar reduction in kernelGravatar barras2009-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2004 due to bad handling of evars in the unification for Gravatar msozeau2009-01-21
| | | | | | | the setoid_rewrite variant called by rewrite (bug traced by Hugo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various little fixes:Gravatar msozeau2009-01-18
| | | | | | | | | | | | - allow a new line after a (** printing *) directive in coqdoc so as not to output spurious new lines. - never directly unify the lemma with an evar in setoid_rewrite (they act as opaque constants). - Fix a useless dependency introduced by tauto which splits a record in SetoidList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
| | | | | | | | | | | | - Really unify with types of metas when they contain metas _or_ evars (why not always?) (fixes bug #2027). - Better handling of evars in rewrite lemmas when using setoid_rewrite through rewrite (reported by Ralf Hinze). - Use retyping with metas when possible (check?) and improve an obscure error message in retyping. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11776 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
| | | | | | | | | | splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
| | | | | | | | | | | | | | | | | | | | | | | inductive types was not taken into account). - Virtually extended tauto to - support arbitrary-length disjunctions and conjunctions, - support arbitrary complex forms of disjunctions and conjunctions when in the contravariant of an implicative hypothesis, - stick with the purely propositional fragment and not apply reflexivity. This is virtual in the sense that it is not activated since it breaks compatibility with the existing tauto. - Modified the notion of conjunction and unit type used in hipattern in a way that is closer to the intuitive meaning (forbid dependencies between parameters in conjunction; forbid indices in unit types). - Investigated how far "iff" could be turned into a direct inductive definition; modified tauto.ml4 so that it works with the current and the alternative definition. - Fixed a bug in the error message from lookup_eliminator. - Other minor changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
| | | | | | | | | the number of conjunctions to split. - A few cleaning and uniformisation in auto.ml. - Removal of v62 hints already in core. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
| | | | | | | | right unification flags for exact hints in eauto (may break a lot of things by succeeding much more often). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not catch _all_ exceptions in setoid unification.Gravatar msozeau2008-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11658 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] notGravatar msozeau2008-11-10
| | | | | | | reducing the type of the given lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11571 85f007b7-540e-0410-9357-904b9bb8a0f7
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
| | | | | | | | | | | | declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
| | | | | | | | introduced by the lemma remain in the subgoals (i.e. it's really [erewrite]). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11544 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
| | | | | | | | | s'est avéré ralentir la compilation des user-contribs au final, sans compter aussi le bug 1980 apparemment introduit par ce commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
| | | | | | | | | | | | | | | | | | | | | - New constr_expr construct [CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr] to generalize the free vars of the [constr_expr], binding these using [binding_kind] and making a lambda or a pi (or deciding from the scope) using [abstraction_kind option] (abstraction_kind = AbsLambda | AbsPi) - Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{ ... }" for implicit bindings (both "..(" and "_(" seem much more difficult to implement). Subject to discussion! A few examples added in a test-suite file. - Also add missing syntax for implicit/explicit combinations for _binders_: "{( )}" means implicit for the generalized (outer) vars, explicit for the (inner) variable itself. Subject to discussion as well :) - Factor much typeclass instance declaration code. We now just have to force generalization of the term after the : in instance declarations. One more step to using Instance for records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #1966, wrong handling of evars.Gravatar msozeau2008-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
| | | | | | | | | | abusivement sur les clauses. Nettoyage au passage de metamap qui était utilisé à la fois pour les substitutions de meta et pour les contextes de typage de meta. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial fix for bug #1948: recompute order of dependencies betweenGravatar msozeau2008-09-25
| | | | | | | | | evars at the end of unification as later evars can refer to previous ones. This removes the assumption that evars are already ordered in eterm's code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
| | | | | | | | | | | | [discriminated]] with a switch for using the more experimantal dnet impl for every hint. Also add [Hint Transparent/Opaque] which parameterize the dnet and the unification flags used by auto/eauto with a particular database. Document all this. Remove [Typeclasses unfold] directives that are no longer needed (everything is unfoldable by default) and move to [Typeclasses Transparent/Opaque] syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1936: uncaught exception due to undefinable exceptions.Gravatar msozeau2008-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1939: defined evars were not substituted in some typeclassesGravatar msozeau2008-09-14
| | | | | | | eauto goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11404 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove redefinition of id in Program.Basics, just add maximal implicits.Gravatar msozeau2008-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
| | | | | | | | | when one wants a particular type. Rewrite of the unification behind [Equations], much more robust but still buggy w.r.t. inaccessible patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug reintroduced in [setoid_reflexivity] etc...Gravatar msozeau2008-09-09
| | | | | | | | Go back to refine_hyp instead of specialize, because only the former handles open terms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11391 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
| | | | | | | | | | | | | | | This permits to create a database [relations] in [RelationClasses] with a single extern tactic in it that tries to apply [reflexivity] or [symmetry]. This is then automatically used in [auto with *] and repair backward compatibility. The previous commit broke some scripts which were using [intuition] to do (setoid) [reflexivity] or [symmetry]: this worked only by accident, because the hint database of typeclasses was used. Overrall, this also allows to put a bunch of always-applicable, related tactics in some database or to use [Hint Extern] but match only on hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
| | | | | | | | | | making the auto apply entry. Makes indexing better and avoid polution of [auto with *] with many abstract lemmas comming from [typeclass_instances]. Quite a nice speedup again, even Field_theory has dropped to 58s from 70s. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11381 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small fixes in "varify", a small tactic doing the first part ofGravatar msozeau2008-09-07
| | | | | | | reification: putting variables in a varmap. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve typeclasses eauto using the dnet for local assumptions too, and selectGravatar msozeau2008-09-04
| | | | | | | | | | only relevant hypotheses in it, slightly cutting the search space. Makes setoid_rewrite less sensitive to the number of hypothesis (~ 5% time improvment on the stdlib). This currently prevents resolution with constants which reduce to classes, hence the modifications in Setoids.Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11360 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anGravatar msozeau2008-09-04
| | | | | | | | | | evar, do unification between the evar type and the type of the instance to properly propagate information. Typical example: in context ?A : Type, ?R : relation ?A. When we instantiate ?R using a goal like x = y by @eq t, we need to instantiate A to t as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1935, reworking the reflexivity, symmetry... tactics to useGravatar msozeau2008-09-03
| | | | | | | | | the same typeclass method application tactic that's available to users. Modify a bit the _red tactics to accomodate the new setup and comment some dead code in setoid_replace. Next step is removing it completely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
| | | | | | | | | | | | | | | | | | | | | | equations. It is essentially an implementation of the "Eliminating Dependent Pattern-Matching" paper by Goguen, McBride and McKinna, relying on the new dependent eliminations tactics. The bulk is in contrib/subtac/equations.ml4. It implements a tree splitting on a set of clauses and the generation of a corresponding proof term along with some obligations at each splitting node. The obligations are solved by driving the dependent elimination tactic and you get a complete proof term at the end with the code given by the equations at the right spots, the rest of the cases being pruned automatically. Does not support recursion yet, a file with examples is in the test-suite. With recursion, it would be similar to Agda 2's pattern matching, except it won't reduce in Coq due to JMeq's/K. Incidentally, the simplification tactics after dependent elimination have been improved, resulting in a clearer and more space efficient implementation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major speed and space improvements in setoid rewrite:Gravatar msozeau2008-08-27
| | | | | | | | | | | | | | | | | | - Avoid using projections for singleton classes. Divides the size of proofs by 2 and simplifies the typechecking as well. - Switch to the new discrimination net implementation for classes, with the current convention that all constants are unfoldable. Users can add "Typeclasses Opaque" declarations make the dnet discriminate more, otherwise it should be entirely backward-compatible. - Fix bug introduced in r11333 in "transitivity" tactic in presence of coercions. Up to 15% gains on setoid-intensive files like Ring_polynom and Field_theory. More importantly, performance should not decrease significantly by adding new Morphism/Setoid declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11337 85f007b7-540e-0410-9357-904b9bb8a0f7
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
| | | | | | | | | | | | | | | syntax yet. Doesn't change the auto/eauto behavior either. - Typeclass resolution now considers everything transparent by default and does it consistently for "open" and closed terms. - Correctly declare singleton classes definition as opaque for proof search. - Add a few initial declarations to make iff, id, compose... opaque - Add definition of dependent signatures for dependent function types and remove corresponding exception code in class_tactics. The instance requires higher-order unification and is not really usable yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11333 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
| | | | | | | class constraints of the form Π x1 ... xn, Class args. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11278 85f007b7-540e-0410-9357-904b9bb8a0f7
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
| | | | | | | | | | | | | | | Now there is a class "SetoidRelation" for registering relations that should always be considered as setoids and never unfolded. Every "Add Relation" command adds an instance and impl,iff are there by default. Now the test is: if there is a SetoidRelation instance, use it ; otherwise, allow unfolding to find an eq or fallback on setoid_rewrite. To avoid searching for SetoidRelation instances repeateadly we check that it is really needed first by unfolding the hyp. Only two scripts relied on the now-forbidden semantics of rewriting by an @eq inside a setoid relation, in Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
* A (safe) implementation of prolog's cut in the typeclasses eauto to avoidGravatar msozeau2008-07-24
| | | | | | | | | redoing proofs for nothing, i.e, do not backtrack on proofs whose evars are disjoint from the evars of the rest of the goals. Fixes the example in bug #1911, needs some more testing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11258 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
| | | | | | | | | | terms and [head_of_constr id] to put the head of a constr in some new hypothesis. Both are used in a new tactic to deal with partial applications in setoid_rewrite. Also fix bug #1905 by using [subrelation] to take care of [Morphism (R ==> R') id] constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11244 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
| | | | | | | | | | majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop using the discrimination net in typeclasses/setoid rewrite, which wasGravatar msozeau2008-07-02
| | | | | | | | considering every definition opaque by default, until a better fix is found. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11202 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 03:01:47 +0000