aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring
Commit message (Expand)AuthorAge
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Implemented a test for "Add [Semi] Setoid Ring" to check that the givenGravatar sacerdot2005-02-03
* Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "||"Gravatar sacerdot2005-02-03
* The statement of the compatibility theorem for addition and multiplicationGravatar sacerdot2005-02-02
* setoid_rewrite t; [tac]Gravatar sacerdot2005-02-02
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* The "Add Setoid" command now has a new argument "as name" that is usedGravatar sacerdot2004-10-01
* cutrewrite does not work with relations that are not Coq-like equalities.Gravatar sacerdot2004-09-30
* New syntaxGravatar sacerdot2004-09-29
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Ported to the new implementation of setoid_*.Gravatar sacerdot2004-09-03
* The old implementation of (setoid_replace c1 with c2) used to replaceGravatar sacerdot2004-09-03
* Setoid_replace.setoid_replace: last argument (that was supposed to beGravatar sacerdot2004-07-23
* correction d'un bug de la tactique pour les semi setoid rings.Gravatar clrenard2004-07-22
* Nouvelle en-têteGravatar herbelin2004-07-16
* eq and eqT are the sameGravatar barras2004-06-25
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Ordre standard pour l'associativiteGravatar herbelin2003-11-14
* moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...Gravatar barras2003-11-13
* Noms/énoncés plus canoniquesGravatar herbelin2003-11-12
* Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...Gravatar herbelin2003-11-05
* Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...Gravatar herbelin2003-11-01
* Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...Gravatar herbelin2003-10-30
* Ajout notations pour les expressions dans un anneauGravatar herbelin2003-10-28
* Simplification preuveGravatar herbelin2003-10-28
* Ajout NArithRingGravatar herbelin2003-10-22
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* distinguer interp_cs et interp_setcsGravatar letouzey2003-10-06
* Cacher les .v8Gravatar herbelin2003-10-03
* oupsGravatar letouzey2003-09-28
* 2 pbs de plus réglés concernant Setoid Ring:Gravatar letouzey2003-09-28
* Un peu plus de souplesse dans la globalisation des noms utilises par les tact...Gravatar herbelin2003-09-26
* commit accidentel d'une bidouilleGravatar letouzey2003-09-22
* suite (et fin) reparation Setoid RingGravatar letouzey2003-09-22
* tentative de rafraichissement de Setoid RingGravatar letouzey2003-09-22
* Changement de la politique de V8only: V8only tout seul signifieGravatar herbelin2003-09-21
* Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...Gravatar herbelin2003-05-21
* Mise en conformite de la precedence du '-' unaire avec celle de NotationsGravatar herbelin2003-05-21
* Mise en conformite de la precedence du '-' unaire avec celle de NotationsGravatar herbelin2003-05-21
* Concentration des notations officielles dans Init/Notations; restructuration ...Gravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Notations arithmetiquesGravatar herbelin2003-05-13
* Alignement du comportement des implicites d'inductif en sortie de section sur...Gravatar herbelin2003-04-09
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07