aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-10-15Wish of Maggesi implemented: the type of the morphism compatibility lemmasacerdot
is now the one that is shown to the user (and not only convertible to it). In this way it is possible to register the lemma in the Hint database. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6217 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6216 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newsacerdot
existential variables it failed. Fixing by propagating the metavariable environment generated by the unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6215 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14Code clean-up.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6214 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14reflexivity, symmetry, symmetry ... in e transitivity now fall-backsacerdot
to their setoid_* counterparts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6212 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-13Compatibilité de Hint Rewrite avec Write Stateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6211 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6209 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12Desactivation de la construction 'lazy match' en attendant une autre solutionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6208 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs ↵herbelin
sont autorisés avant l'énoncé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6207 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ↵herbelin
mais utilisé !) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6206 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12Prise en compte dans cut_ident des idents de la form _23 qui sont ↵herbelin
officiellement autorisés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6205 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12option -no-hash-consing pour supprimmer le hash-consingfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6201 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6200 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵herbelin
evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11Suppression IsConjecture redondant avec Conjecturalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6198 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6197 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6196 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6195 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07setoid_symmetry in ... implemented.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6194 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07New commandssacerdot
setoid_reflexivity setoid_symmetry setoid_transitivity The command setoid_symmetry in ... is not implemented yet (it behaves just as symmetry in ... for now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6193 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07iff and impl are now declared as transitive relations.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6192 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07Now Print Setoids prints also the transitivity justification of transitivesacerdot
relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6191 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6190 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06* New syntactic sugar: Add Relation ... transitivity proved by ...sacerdot
now declares both the relation and the relation as a morphism, computing the appropriate signature (depending on the reflexivity of the relation). * New parameter "as ..." to Add Relation (to be able to compute the morphism name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6189 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06added transitivitybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6188 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06added transitivitybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6187 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06Add Setoid now accepts also quantified setoids.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6186 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06* code clean upsacerdot
* check for dependent functions reimplemented correctly (closing a long standing bug that was already in the original implementation by Clement Renard) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6185 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06Th unification procedure has been made a bit more complete by recording thesacerdot
number of quantifiers of a relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6184 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06Leibniz equality is now a quantified relation.sacerdot
This means that you can declare a morphism signature that has an argument (or its output type) that is just eq. E.g.: Add Morphism incl with signature incl --> eq ++> impl. is a correct signature for a morphism property of type forall A, list A -> list A -> Prop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6183 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6182 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6181 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05* code simplificationsacerdot
* error message improved * bug fixed: it was not checked whether the carrier of a relation of class Leibniz matched the expected type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6180 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05* [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whethersacerdot
there exists an i such that (c x1 ... xi) is a morphism. Previously only the case c was tried. * [ bug fixed ]: the term that must be replaced must not occur in c (i.e. in (c x1 ... xi)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6179 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-05* Bug fix: in case of non dependent implications the second argument wassacerdot
not correctly de-lifted. * [EXPERIMENTAL]: the Add Relation and Add Morphism commands now accept also quantified relations and quantified morphisms. [ Add Setoid doesn't do that yet. ] However, in case of quantified relations the matching between an argument type and the (quantified) carrier expected for it is quite weak and is complete only not modulus conversion. * Many bugs have probably been introduced by the experimental feature. However, the bugs should manifest only in the case of quantified relations. In particular Leibniz has a strange status and its management should be revised. * Open problem: should the data type for relations and morphisms be changed to explicitly show the quantifications? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6178 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6177 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-04Added "as ..." parameter to Add Morphism.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6176 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-04un paquet de corrections de bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6175 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6174 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6173 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01eq_constr replaced with a conversion test where possible.sacerdot
This is particular useful in case of modules (when it often happens to have two setoids that can be composed only up to convertibility of their input/output types). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6172 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-011. added new parameter "as ..." to Add Setoid. Used to synthesize the namesacerdot
of the morphism. Previously the name was automatically generated, but it was impossible to generate the same name in a module type and in a module. 2. behaviour of the relation/morphism tables w.r.t. module types and functors fixed. 3. relations/setoids/morphisms can now happear in a module type. Add Morphism in a module type declares an axiom instead of starting a new proof. Add Morphism/Add Relation/Add Setoid in a module now generate objects that match those generated by the same commands in a module type. 4. error messages improved/fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6171 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01add_setoid has a new parameter used to synthesize the morphism name.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6170 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01Added "as ..." parameters to "Add Setoid"sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6169 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01The "Add Setoid" command now has a new argument "as name" that is usedsacerdot
to generate the name of the morphism. Previously the name was automatically generated, but this behaviour was not compatible with module typing: it was not possible to generate the same identifier in the module type and in the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6167 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30New tacticsacerdot
setoid_replace ... with ... in ... [using relation ...] [generate side conditions ...] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6166 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30New tactic [setoid_]rewrite ... in ... [generate side conditions ...].sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30Proof term size optimization: setoid_rewrite H where H is an application ofsacerdot
Leibniz equality and no side conditions are imposed by the user simply calls the rewrite tactic. This was already done for setoid_replace/replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6164 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 03:34:04 +0000