aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
| | | | | | | | delta conversion when it should (setoid_rewrite bug reported by roconnor). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
| | | | | | | | | | in reasonable time), add (unfinished) documentation on type classes. Put some classes into Prop explicitely as singleton inductive types are no longer in Prop by default even if all the arguments are (is that really what we want? roconnor says no). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
| | | | | | | | now. Fix proof scripts that failed correspondingly. Should make many contribs compile again... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
| | | | | | | | | | | | | | | | | | | | | | (i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le principe de la hiérarchie d'univers est d'être cumulative -- et que Set en soit le niveau 0). Une solution aurait été de poser Prop <= Set mais on adopte une autre solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type et Prop <= Set, on garde la représentation de Prop au sein de la hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau sans aucune contrainte inférieure, appelons Type -1) et on adapte les fonctions de sous-typage et de typage pour qu'elle prenne en compte la règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets incidents dans Termops.refresh_universes et Univ.super). Petite uniformisation des noms d'univers et de sortes au passage (univ.ml, univ.mli, term.ml, term.mli et les autres fichiers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
| | | | | | | | | | | | | | | des types des with-bindings dans la 8.1 [ceux-ci étaient déjà utilisés et ce qui est vraiment nouveau est que l'unification est maintenant celle de evarconv alors que c'était avant un mélange d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je renonce à maintenir la compatibilité (on se retrouve donc avec un exemple qui fonctionne différement dans TermsConv.v de CoLoR). - Robustesse accrue pour la nouvelle facilité de syntaxe de binding avec paramètre pour pose/set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
| | | | | | | | | | | | | substitution. Makes unification succeed a bit more often, hence auto works better in some cases. - Backtrack the changes of auto using Hint Unfold to do more delta and add a new tactic "new auto" which does that, for compatibility. The first fix may have a big impact on the contribs, whereas the second should make them compile again... we'll see. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10855 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
| | | | | | | | | "pose as" de Program. - Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml. - Comportement de "simple apply" rendu plus proche de celui du apply 8.1 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debug implementation of failing tactics in Morphism to allow earlierGravatar msozeau2008-04-26
| | | | | | | | failures in proof search. Catch Refiner.FailError in typeclasses eauto to indicate that an extern tactic failed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
| | | | | | | | | | | des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
| | | | | | | | | | | | | | | | debugging and printing hint databases - Typeclasses unfold now correctly adds _global_ unfold hints. - New tactic autosimpl to do simplification using the declared unfold hints in given hint databases. - Work on auto-modulo-some-delta (the declared Unfold constants), actually used mostly if the goal contains evars, as Hint_db.map_auto does not work up-to any conversions (yet). - Fix GenMul which was using the old semantics of failing early because of variance checks, which is not possible in the new implementation. - Restrict when reflexive_morphism may be used using an extern tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | de l'argument donné contient des métavariables (souhait #1408). Beaucoup d'infrastructure autour des constantes pour cela mais qu'on devrait pouvoir récupérer pour analyser plus finement le comportement des constantes en général : 1- Pour insérer les coercions, on utilise une transformation (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml. 2- Pour la compatibilité, on s'interdit d'insérer une coercion entre classes flexibles parce que sinon l'insertion de coercion peut prendre précédence sur la résolution des evars ce qui peut changer les comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN). 3- Pour se souvenir rapidement de la nature flexible ou rigide du symbole de tête d'une constante vis à vis de l'évaluation, on met en place une table associant à chaque constante sa constante de tête (heads.ml) 4- Comme la table des constantes de tête a besoin de connaître l'opacité des variables de section, la partie tables de declare.ml va dans un nouveau decls.ml. Au passage, simplification de coercion.ml, correction de petits bugs (l'interface de Gset.fold n'était pas assez générale; specialize cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml]; whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml]) et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml, classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on change of flags for elim, otherwise rewrite goes underGravatar msozeau2008-04-23
| | | | | | | local variables... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change default eauto depth to 100 in setoid_rewrite, bump necessaryGravatar msozeau2008-04-23
| | | | | | | | | after introduction of the MorphismProxy indirection. Do local delta conversion in elim. Update CHANGES regarding level of ==> notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10834 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correct unification for the rewrite variant of setoid_rewrite,Gravatar msozeau2008-04-21
| | | | | | | | so that the example of bug #1425 is accepted. - Backtrack level of notations for morphism signatures to 55. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10825 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
| | | | | | | | | | | | | | | | term unification (for constant and variable delta unfolding) and one to parameterize closed-term conversion. Most of the time conversion uses full delta and unification does no delta. This fine-grain is used in rewrite/setoid_rewrite, where only closed-term delta on global constants is allowed. - Interpret Hint Unfold as a directive for delta conversion in auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints). - Remove ad-hoc support for this in typeclasses. Now setoid_rewrite works correctly w.r.t. the old version regarding local definitions. - Fix closed bugs which needed updating due to syntax modifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
| | | | | | | | | | lists of occurrences through tactics. Implement the "at" variants of setoid_replace correspondingly. Fix in class_tactics efor w_unify not checking types when unifying a meta with anything (problematic at top-level only). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug squashing day !Gravatar msozeau2008-04-17
| | | | | | | | | | | | | | | | | - Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to setoids. Add corresponding test files. - Add new modulo_zeta flag to control zeta during unification (e.g. not allowed for setoid_rewrite unification, but ok for almost everything else). - Various fixes in class_tactics with respect to evars and error messages. - Correct error message for NoOccurenceFound, distinguishing between a rewrite in the goal or an hypothesis. - Move notations for ==>, --> and ++> to level 90 as suggested by Russell O'Conor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
| | | | | | | | | | | | | | | - More meaningful argument name for resolve_typeclasses. - Try to remove unneeded instance declarations in Morphisms. - Allow the proofs of reflexivity arising from unchanged arguments in setoid_rewrite to be fullfiled by Morphism instances and not necessariy because the relation is reflexive (needed by higher-order morphisms). Use a new "MorphismProxy" class to implement that efficiently. - Fix a bug in abstract_generalize not delta-reducing a type where it should. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10807 85f007b7-540e-0410-9357-904b9bb8a0f7
* More renamings to avoid clashes (e.g. with CoRN).Gravatar msozeau2008-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
| | | | | | | | SetoidTactics and document it. Cleanup Classes.Equivalence. Minor fixes to the Program doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10799 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
| | | | | | | | | | | | semantics. - Add an Equivalence instance for pointwise equality from an Equivalence on the codomain of a function type, used by default when comparing functions with the Setoid's ===/equiv. - Partially fix the auto hint database "add" function where the exact same lemma could be added twice (happens when doing load for example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
| | | | | | | | | | | | | | | | - Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses corrections Gravatar herbelin2008-04-14
| | | | | | | | | | | | | | - gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev] - suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des quotations de tactiques pour simuler les métas des constr - quitte à devoir utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics] - utilisation de error en place d'un "print_string" d'échec dans fourier - améliorations espérées vis à vis de quelques "bizarreries" dans la gestion des Meta [pretyping] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamings to avoid clashes with definitions in Relation_Definitions, nowGravatar msozeau2008-04-14
| | | | | | | | | projections are of the form "equivalence_reflexive" and instance names too. As they are (almost) never used directly, it does not hurt to have long explicit names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
| | | | | | | | | | | | | | | | | | | | | | - vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
| | | | | | | | | | | | declarations. By default, print the list of implicitely generalized variables. Implement new commands Add Parametric Relation/Morphism for... parametric relations and morphisms. Now the Add * commands are strict about free vars and will fail if there remain some. Parametric just allows to give a variable context. Also, correct a bug in generalization of implicits that ordered the variables in the wrong order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10782 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
| | | | | | | | | | | Uses setoid_rewrite even if rewriting with leibniz if there are specified occurences, maybe a combination of pattern and rewrite could be done instead. Correct spelling of occurrences. Coq does not compile with this patch, the next one will make it compile again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitGravatar msozeau2008-04-09
| | | | | | | loading and exporting of Setoid to ROmega which uses it for iff. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Verify Setoid is loaded before doing anything.Gravatar msozeau2008-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix evar bugs in type classes:Gravatar msozeau2008-04-09
| | | | | | | | | | - disallow uninstantiated hypotheses (typically local variables with no assigned types) as solutions for typeclass instantiation. - Fix resolve_typeclasses call in pretyping that was not propagating found instances in the term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10772 85f007b7-540e-0410-9357-904b9bb8a0f7
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
| | | | | | | | | | | | | | | | | relf/sym/trans relations from morphisms on prop connectives and relations. - Add general order theory on predicates, instantiated for relations. Derives equivalence, implication, conjunction and disjunction as liftings from propositional connectives. Can be used for n-ary homogeneous predicates thanks to a bit of metaprogramming with lists of types. - Rebind Setoid_Theory to use the Equivalence record type instead of declaring an isomorphic one. One needs to do "red" after constructor to get the same statements when building objects of type Setoid_Theory, so scripts break. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
| | | | | | | | | | | | | | | | | | | | lemmes se terminant par False ou not sur n'importe quelle formule (cela crée trop d'incompatibilités dans les "try apply" etc.); de toutes façons, "contradict" joue presque ce rôle (à ceci près qu'il ne traverse pas les conjonctions) (tactics/tactics.ml). - Quelques corrections sur RIneq.v - le hint Rlt_not_eq avait été oublié dans la phase de restructuration, - davantage de noms canoniques (O -> 0, etc.), - nouvelle tentative de ramener "auto" vers Rle (avec Rle_ge) plutôt que vers Rge qui est moins souvent associé à des hints. - Utilisation du formateur deep_ft pour afficher les scripts de preuve afin d'éviter le besoin d'un "Set Printing Depth" (vernacentries.ml). - Suppression de certaines utilisations de l'Anomaly de meta_fvalue qui ne correspondaient pas à des comportements anormaux (reductionops.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes: Gravatar msozeau2008-04-05
| | | | | | | | | - Allow unicode superscripts characters. - Put Program notations in scopes. - Correct priority semantics in typeclasses eauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'une extension de apply pour que celui-ci sacheGravatar herbelin2008-04-04
| | | | | | | | traverser les conjonctions (par exemple, apply sur un "iff" cherchera à utiliser la première des 2 composantes qui s'applique). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10758 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Relâchement de la contrainte de bonne longueur des intropatternsGravatar herbelin2008-04-04
| | | | | | | | | | | | | lorsqu'en position terminale (en fait, l'idéal serait de pouvoir mettre des tactiques dans les branches, style "intros [H ; tac | ]") (cf un exemple QvMake.v) - Pas de delta du tout quand on fait de la recherche de sous-terme (même lorsqu'on vient de apply avec une conclusion ?P t) (cf un exemple dans Rocq/DEMOS/Sorting.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
| | | | | | | | | | | | | | | | | | - ajout de -> et <- pour substitution immédiate d'une égalité (comportement à la subst si variable, à la rewrite in * sinon) - ajout possibilité d'hypothèses avec paramètres - correction d'un comportement bizarre de l'utilisation des noms dans cas "[[|] H]" (cf CHANGES) Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])" pour décider de garder les noms, mais la syntaxe est assez moche. Peut-être un "intros H: <- H': [ | ]" ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandGravatar herbelin2008-04-04
| | | | | | | un lemme avec evars est utilisé localement avec auto ou eauto (clause using). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiGravatar herbelin2008-04-04
| | | | | | | n'était pas encore fait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
| | | | | | | | | | | alleviate some problems with delta. Better precedence in lambda notation. Temporarily deactivate notations for relation conjunction, equivalence and so on, while we search for a better syntax and maybe a generalization (fixes bug #1820). Better destruct_call in Program.Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
| | | | | | | | pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10738 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix for rewriting under dependent products.Gravatar msozeau2008-03-31
| | | | | | | | - Use support for abbreviations with params added by Hugo for inverse. - Standard priorities for operators on relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10733 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications diverses et variées :Gravatar herbelin2008-03-30
| | | | | | | | | | | | | - Nouvel essai de prise en compte unfold dans apply (unification.ml) - Correction bug commit précédent (constrintern.ml) - Correction bug d'explication des evars non résolues (evarutil.ml) - Fenêtre de query coqide plus large (command_windows.ml) - Orthographe tauto (tauto.ml4) - Crédits (ConstructiveEpsilon.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | Add definitions of relational algebra in Classes/RelationClasses including equivalence, inclusion, conjunction and disjunction. Add PartialOrder class and show that we have a partial order on relations. Change SubRelation to subrelation for consistency with the standard library. The caracterization of PartialOrder is a bit original: we require an equivalence and a preorder so that the equivalence relation is equivalent to the conjunction of the order relation and its inverse. We can derive antisymmetry and appropriate morphism instances from this. Also add a fully general heterogeneous definition of respectful from which we can build the non-dependent respectful combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
| | | | | | | | | | | | | | | | | | | - Better interface in constrintern w.r.t. evars used during typechecking - Add "unsatisfiable_constraints" exception which gives back the raw evar_map that was not satisfied during typeclass search (presentation could be improved). - Correctly infer the minimal sort for typeclasses declared as definitions (everything was in type before). - Really handle priorities in typeclass eauto: goals produced with higher priority (lowest number) instances are tried before other of lower priority goals, regardless of the number of subgoals. - Change inverse to a notation for flip, now that universe polymorphic definitions are handled correctly. - Add EquivalenceDec class similar to SetoidDec, declaring decision procedures for equivalences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
| | | | | | | | context [] pattern). May break some user contribs... Rename clsubstitute to substitute. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
| | | | | | | | | | | | | | types. Change (again) the semantics of bindings and the binding modifier ! in typeclasses. Inside [ ], implicit binding where only parameters need to be given is the default, use ! to use explicit binding, which is equivalent to regular bindings except for generalization of free variables. Outside brackets (e.g. on the right of instance declarations), explicit binding is the default, and implicit binding can be used by adding ! in front. This avoids almost every use of ! in the standard library and in other examples I have. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility fixes, backtrack on definitions of reflexive,Gravatar msozeau2008-03-22
| | | | | | | | | | | | | symmetric... classes for now, merging Relations with RelationClasses requires some non-trivial changes on implicits but also some definitions are different (e.g. antisymmetric in Classes is defined w.r.t an equivalence relation and not eq). Move back to Reflexive and so on. reflexivity-like tactics fail in the same way as before if Setoid was not imported. There is now a scope for morphism signatures, hence "==>", "++>" and "-->" can be given different interpretations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10708 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control rewriting under lambdas. Otherwise makes someGravatar msozeau2008-03-20
| | | | | | | | | | | | rewrite calls fail because an occurence is found under a lambda that was not found before and there are no adequate morphism declarations to make the rewrite succeed nor the possibility to give occurences to rewrite (yet). Only setoid_rewrite will try rewriting under lambda's for now. Example problem found in a port of the Random library. Also improved the required_library error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
| | | | | | | | | | | | | | | | | | | | | | | names, gives the ability to specify qualified classes in instance declarations. Use that in the class_tactics code. Refine the implementation of classes. For singleton classes the implementation of the class becomes a regular definition (into Type or Prop). The single method becomes a 'trivial' projection that allows to launch typeclass resolution. Each instance is just a definition as usual. Examples in theories/Classes/RelationClasses. This permits to define [Class reflexive A (R : relation A) := refl : forall x, R x x.]. The definition of [reflexive] that is generated is the same as the original one. We just need a way to declare arbitrary lemmas as instances of a particular class to retrofit existing reflexivity lemmas as typeclass instances of the [reflexive] class. Also debug rewriting under binders in setoid_rewrite to allow rewriting with lemmas which capture the bound variables when applied (works only with setoid_rewrite, as rewrite first matches the lemma with the entire, closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal [exists x, P (f x)]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10697 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 21:00:59 +0000