aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring/ring.ml
Commit message (Expand)AuthorAge
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* 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
* 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
* cutrewrite does not work with relations that are not Coq-like equalities.Gravatar sacerdot2004-09-30
* New syntaxGravatar sacerdot2004-09-29
* 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
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* distinguer interp_cs et interp_setcsGravatar letouzey2003-10-06
* 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
* suite (et fin) reparation Setoid RingGravatar letouzey2003-09-22
* tentative de rafraichissement de Setoid RingGravatar letouzey2003-09-22
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Reparation de ring pour les setoidesGravatar clrenard2002-06-19
* Protection des tactiques contre l'utilisation sans le bon contexte de thoriesGravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Suppression de l'application de f_equal2 pour "mult" (non inversible);Gravatar herbelin2002-04-05
* reparation semi setoid ringGravatar clrenard2002-03-14
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* ParsingGravatar herbelin2001-08-10
* Ajout d'un Ring pour setoidesGravatar clrenard2001-07-10
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* patch ClaudioGravatar filliatr2001-05-28
* réparation Ring (simplifications)Gravatar filliatr2001-05-14
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* rétablissement patch ClaudioGravatar filliatr2001-02-05
* retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...Gravatar filliatr2001-02-02
* Comment fixedGravatar sacerdot2001-01-12