aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
...
* Fixes in dependent induction tactic, putting things in better order forGravatar msozeau2008-09-11
| | | | | | | simplifications (homogeneous equations first). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11398 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
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
| | | | | | | overriding the default tactic when adding a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11373 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
* Little cleanup in auto.Gravatar msozeau2008-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11336 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
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
| | | | | | | | intro-patterns and avoid useless generalizations on inductive parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de bugs:Gravatar herbelin2008-08-05
| | | | | | | | | | | | | - evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un terme applicatif au moment de tester f u1 .. un = g v1 .. vn au premier ordre : on revient sur l'algo tel qu'il était avant le commit 11187. - Bug #1887 (format récursif cassé à cause de la vérification des idents). - Nouveau choix de formattage du message "Tactic Failure". - Nettoyage vocabulaire "match context" -> "match goal" au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 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
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
| | | | | | | generalized variables himself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix wrong environment bug in test for setoid_rewrite or rewrite.Gravatar msozeau2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11279 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 better test for relations being setoids or not: do leibniz rewrite iffGravatar msozeau2008-07-25
| | | | | | | the applied relation is an abbreviation for @eq. Fixes bug #1915. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11264 85f007b7-540e-0410-9357-904b9bb8a0f7
* More compatibility fixes, revert the tauto fix that preventedGravatar msozeau2008-07-25
| | | | | | | destruction of records as a lot of scripts currently rely on it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11263 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
| | | | | | | after all... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11259 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
* Suite commit 11236Gravatar notin2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation de l'information "strict" (càd à toplevel ou en train deGravatar herbelin2008-07-24
| | | | | | | | | | définir une ltac) dans l'interprétation des identificateurs isolés en position de tactiques, comme dans "let x:=y in t" (résoud l'incompatibilité #1906). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11250 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
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
| | | | | | | | | | | It breaks tauto as [?X _ _] matches much more terms. It is mostly fixed by not destructing objects of record types. The new [intuition] was also pulling an unneeded dependency in Field_theory which can be cleared easily. Zis_gcd_bezout is also considered a conjunction now, which seems correct(?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11243 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
| | | | | | | | effacé dans un intro-pattern (suggéré par ssreflect). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 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
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
| | | | | | | | | | | | | | | | | - Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas où c'est le n-ième sous-termes qui finalement réussit (passage à une complexité en n plutôt que n^2, via l'utilisation de continuations). - Sémantique du filtrage: suppression dans sub_match de la recherche dans le type des let (puisque ce n'est pas cencé être une information utilisateur) mais rajout de la recherche dans le champ cast qui lui est utilisateur. - Nouvelle fonctionnalité: récupération des noms des variables liantes filtrées (dans matches/sub_match) et utilisation de ces noms dans ltac (utile pour récupérer x dans "exists x, P x"); git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix implicit arguments in sections bug and check for resolution of evars whenGravatar msozeau2008-07-07
| | | | | | | | | defining records. Fix test-suite script because of new implicit argument setting for DefaultRelation. Fix regression in auto, changing the order of tried lemmas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11213 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
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
| | | | | | | | | | | | | | | | | goals containing existentials and use transparency information on constants (optionally). Only used by the typeclasses eauto engine for now, but could be used for other hint bases easily (just switch a boolean). Had to add a new "creation" hint to be able to set said boolean upon creation of the typeclass_instances hint db. Improve the proof-search algorithm for Morphism, up to 10 seconds gained in e.g. Field_theory, Ring_polynom. Added a morphism declaration for [compose]. One needs to declare more constants as being unfoldable using the [Typeclasses unfold] command so that discrimination is done correctly, but that amounts to only 6 declarations in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵Gravatar notin2008-06-25
| | | | | | globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction petit bug sur révision 11159 (res_pf fait un effet de bordGravatar herbelin2008-06-21
| | | | | | | sur le sigma, utilisation de refine à la place). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11162 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptées. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiées (au lieu de traiter seulement les buts t1<>t2). --This line, and those below, will be ignored-- M doc/refman/RefMan-tac.tex M CHANGES M pretyping/evd.ml M pretyping/termops.ml M pretyping/termops.mli M pretyping/clenv.ml M tactics/extratactics.ml4 M tactics/inv.ml M tactics/equality.ml M tactics/tactics.mli M tactics/equality.mli M tactics/tacticals.ml M tactics/eqdecide.ml4 M tactics/tacinterp.ml M tactics/tactics.ml M tactics/extratactics.mli M toplevel/auto_ind_decl.ml M contrib/funind/invfun.ml M test-suite/success/Discriminate.v M test-suite/success/Injection.v M proofs/clenvtac.mli M proofs/clenvtac.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little fixes: print unbound variable in error message (patch by SamuelGravatar msozeau2008-06-19
| | | | | | | | Bronson), some keywords in coqdoc, and test well-typedness of predicate in subtac_cases after abstraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11153 85f007b7-540e-0410-9357-904b9bb8a0f7
* incomplete bugfix for infoGravatar corbinea2008-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11149 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
| | | | | | | | (résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in implementation of splitting of class constraints.Gravatar msozeau2008-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility fixes (Add Setoid bug and accidental introduction of aGravatar msozeau2008-06-18
| | | | | | | tactic named "app"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11139 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes w.r.t. let binders in class contexts and Add ParametricGravatar msozeau2008-06-17
| | | | | | | Morphism/Relation bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
| | | | | | | | unsatisfiable constraints. Add a resolution call in tacinterp before trying the default tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
| | | | | | | | | | | | | | disambiguate syntax: [ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x : nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will not parse. Add applicative contexts in tactics match, to be able to match arbitrary partial applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end will bind C to [ ∙ 1 2 ] and x to 0. Minor improvements in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
| | | | | | | | components and resolving them separately, reporting more precise failures. Improve error messages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11105 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
| | | | | | | | | | | | | | | - Changement au passage de la convention "at -n1 ... -n2" en "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut pas mélanger des positifs et des négatifs. - Au passage: - simplification de gclause avec fusion de onconcl et concl_occs, - généralisation de l'utilisation de la désignation des occurrences par la négative aux cas de setoid_rewrite, clrewrite et rewrite at, - correction d'un bug de "rewrite in at" qui utilisait le at de la conclusion dans les hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correct handling of DependentMorphism error, using tclFAIL instead ofGravatar msozeau2008-06-10
| | | | | | | | | | | | letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:31:17 +0000