| Age | Commit message (Expand) | Author |
|---|
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-03-14 | Makefile: ml dependencies of contribs are moved to .mllib files | letouzey |
| 2009-01-18 | Getting rid of the previous implementation of setoid_rewrite which was | msozeau |
| 2009-01-01 | Switched to "standardized" names for the properties of eq and | herbelin |
| 2008-12-16 | Take advantage of natdynlink when available: almost all contribs become loada... | letouzey |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-05-09 | Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ] | herbelin |
| 2008-04-29 | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin |
| 2008-04-14 | Diverses corrections | herbelin |
| 2008-04-12 | Adding 'at' to rewrite, as it is already implemented in setoid_rewrite. | msozeau |
| 2008-04-01 | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2007-12-06 | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2006-11-13 | Encore des _sym au lieu de _comm | herbelin |
| 2006-09-26 | petits pbs de dependances | barras |
| 2006-09-26 | Compilation newring | notin |
| 2006-09-26 | commit de field + renommages | barras |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2006-04-28 | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-02-06 | Nettoyage et documentation de Library | herbelin |
| 2005-02-03 | Implemented a test for "Add [Semi] Setoid Ring" to check that the given | sacerdot |
| 2005-02-03 | Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "||" | sacerdot |
| 2005-02-02 | The statement of the compatibility theorem for addition and multiplication | sacerdot |
| 2005-02-02 | setoid_rewrite t; [tac] | sacerdot |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-11-12 | Changement dans les boxed values . | gregoire |
| 2004-10-01 | The "Add Setoid" command now has a new argument "as name" that is used | sacerdot |
| 2004-09-30 | cutrewrite does not work with relations that are not Coq-like equalities. | sacerdot |
| 2004-09-29 | New syntax | sacerdot |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
| 2004-09-03 | Ported to the new implementation of setoid_*. | sacerdot |
| 2004-09-03 | The old implementation of (setoid_replace c1 with c2) used to replace | sacerdot |
| 2004-07-23 | Setoid_replace.setoid_replace: last argument (that was supposed to be | sacerdot |
| 2004-07-22 | correction d'un bug de la tactique pour les semi setoid rings. | clrenard |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-06-25 | eq and eqT are the same | barras |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-14 | Ordre standard pour l'associativite | herbelin |
| 2003-11-13 | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras |
| 2003-11-12 | Noms/énoncés plus canoniques | herbelin |
| 2003-11-05 | Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif... | herbelin |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |
| 2003-10-30 | Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ... | herbelin |
| 2003-10-28 | Ajout notations pour les expressions dans un anneau | herbelin |
| 2003-10-28 | Simplification preuve | herbelin |
