index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
ring
Commit message (
Expand
)
Author
Age
*
Plug the new setoid implemtation in, leaving the original one commented
msozeau
2008-03-06
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Encore des _sym au lieu de _comm
herbelin
2006-11-13
*
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-09-26
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
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-03
*
The statement of the compatibility theorem for addition and multiplication
sacerdot
2005-02-02
*
setoid_rewrite t; [tac]
sacerdot
2005-02-02
*
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-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
The "Add Setoid" command now has a new argument "as name" that is used
sacerdot
2004-10-01
*
cutrewrite does not work with relations that are not Coq-like equalities.
sacerdot
2004-09-30
*
New syntax
sacerdot
2004-09-29
*
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-09-03
*
Setoid_replace.setoid_replace: last argument (that was supposed to be
sacerdot
2004-07-23
*
correction d'un bug de la tactique pour les semi setoid rings.
clrenard
2004-07-22
*
Nouvelle en-tête
herbelin
2004-07-16
*
eq and eqT are the same
barras
2004-06-25
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Ordre standard pour l'associativite
herbelin
2003-11-14
*
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
*
Noms/énoncés plus canoniques
herbelin
2003-11-12
*
Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...
herbelin
2003-11-05
*
Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...
herbelin
2003-11-01
*
Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...
herbelin
2003-10-30
*
Ajout notations pour les expressions dans un anneau
herbelin
2003-10-28
*
Simplification preuve
herbelin
2003-10-28
*
Ajout NArithRing
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
distinguer interp_cs et interp_setcs
letouzey
2003-10-06
*
Cacher les .v8
herbelin
2003-10-03
*
oups
letouzey
2003-09-28
*
2 pbs de plus réglés concernant Setoid Ring:
letouzey
2003-09-28
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
commit accidentel d'une bidouille
letouzey
2003-09-22
*
suite (et fin) reparation Setoid Ring
letouzey
2003-09-22
*
tentative de rafraichissement de Setoid Ring
letouzey
2003-09-22
[next]