aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Setoids
Commit message (Expand)AuthorAge
* Minimum pour documentation TeX de la biblioGravatar herbelin2006-02-22
* Copy of the definition of prodT (already in the standard library) removed.Gravatar sacerdot2004-11-16
* Proof term size reduction (again).Gravatar sacerdot2004-10-19
* * Code simplification and clean-up. In particular there is no more codeGravatar sacerdot2004-10-18
* iff and impl are now declared as transitive relations.Gravatar sacerdot2004-10-07
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
* added transitivityGravatar barras2004-10-06
* impl is a reflexive relation (it used to be areflexive).Gravatar sacerdot2004-09-29
* impl relation and impl/and/or/not morphisms over impl declared.Gravatar sacerdot2004-09-29
* * cleaning/renamingGravatar sacerdot2004-09-08
* The Coq part of the reflexive tactic is now able to handle alsoGravatar sacerdot2004-09-08
* * The Coq part of the reflexive tactic setoid_rewrite is generalized toGravatar sacerdot2004-09-07
* New reflexive implementation of setoid_rewrite. The new implementationGravatar sacerdot2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Cacher les .v8Gravatar herbelin2003-10-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
* Deplacement des setoides.Gravatar clrenard2001-09-19