aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Setoids
Commit message (Collapse)AuthorAge
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
| | | | | | | | | | | sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Duplication du fichier FSetProperties pour les ensembles Weak. Gravatar letouzey2006-05-11
| | | | | | | | | | Du coup, factorisation d'une partie dans SetoidList. Ajout de lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface concernant elements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minimum pour documentation TeX de la biblioGravatar herbelin2006-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Copy of the definition of prodT (already in the standard library) removed.Gravatar sacerdot2004-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6306 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof term size reduction (again).Gravatar sacerdot2004-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Code simplification and clean-up. In particular there is no more codeGravatar sacerdot2004-10-18
| | | | | | | | | | | | | | | duplicated between add_relation and add_setoid. * Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v * Term size reduction (first part): when a relation is registered, we add to the environment a definition that gives back either the relation as an argument or as a relation class. The definition is used to reduce the term size. [ Note: we could save a bit more by defining two definitions in place of one. However, we suppose that the lambda term fragments generated can be shared quite effectively. Thus we would recive almost no benefit by sharing in terms of size. What about proof checking time? ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7
* iff and impl are now declared as transitive relations.Gravatar sacerdot2004-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6192 85f007b7-540e-0410-9357-904b9bb8a0f7
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
| | | | | | | | | | 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
* added transitivityGravatar barras2004-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6188 85f007b7-540e-0410-9357-904b9bb8a0f7
* impl is a reflexive relation (it used to be areflexive).Gravatar sacerdot2004-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6154 85f007b7-540e-0410-9357-904b9bb8a0f7
* impl relation and impl/and/or/not morphisms over impl declared.Gravatar sacerdot2004-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6153 85f007b7-540e-0410-9357-904b9bb8a0f7
* * cleaning/renamingGravatar sacerdot2004-09-08
| | | | | | | * reuse of definitions already given in the standard library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6083 85f007b7-540e-0410-9357-904b9bb8a0f7
* The Coq part of the reflexive tactic is now able to handle alsoGravatar sacerdot2004-09-08
| | | | | | | | | | | irreflexive relations (in particular partial setoids, also called typoids). This feature was asked by Marco Maggesi. The Coq part of the tactic has now reached the planned expressive power. However, the ML part does not exploit yet the full expressiveness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6079 85f007b7-540e-0410-9357-904b9bb8a0f7
* * The Coq part of the reflexive tactic setoid_rewrite is generalized toGravatar sacerdot2004-09-07
| | | | | | | | | | | asymmetric relations thanks to the introduction of morphisms that are covariant or contravariant in their arguments. * The ML part of the tactic is updated only for backward compatibility: it is still not possible to benefit from the asymmetric relations and relative morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6070 85f007b7-540e-0410-9357-904b9bb8a0f7
* New reflexive implementation of setoid_rewrite. The new implementationGravatar sacerdot2004-09-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | introduces a few backward incompatibilities: 1. setoid_replace used to try to close the new goal using full_trivial. The new implementation does not try to close the goal. To fix the script it is sufficient to add a "; [ idtac | trivial ]." after every application of setoid_replace that used to generate just one goal. 2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation only replaces c1 with c2. To fix the script it is sufficient to replace (setoid_replace c1 with c2) with (setoid_replace c1 with c2) || (setoid_replace c2 with c1) in those cases where it is unknown what should be substituted with what. 3. the goal generated by the "Add Morphism" command has the hypothesis permutated w.r.t. the old implementation. I.e. the old implementation used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ... whereas the new implementation generates forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ... Fixing the script is usually trivial. 4. the "Add Morphism P" command used to generate a non-standard goal in the case of P being a predicate (i.e. a function whose codomain is Prop). In that case the goal ended with an implication (instead of ending with a coimplication). The new implementation generates a standard goal that ends with a coimplication. To fix the script you can add the following line at the very beginning: cut <<old_goal>>; intro Hold; split; apply Hold; assumption || (symmetry;assumption). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cacher les .v8Gravatar herbelin2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2731 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des setoides.Gravatar clrenard2001-09-19
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 16:19:27 +0000