index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
ring
/
Setoid_ring_theory.v
Commit message (
Expand
)
Author
Age
*
The statement of the compatibility theorem for addition and multiplication
sacerdot
2005-02-02
*
The "Add Setoid" command now has a new argument "as name" that is used
sacerdot
2004-10-01
*
Ported to the new implementation of setoid_*.
sacerdot
2004-09-03
*
Nouvelle en-tĂȘte
herbelin
2004-07-16
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
*
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
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Changement de la politique de V8only: V8only tout seul signifie
herbelin
2003-09-21
*
Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...
herbelin
2003-05-21
*
Mise en conformite de la precedence du '-' unaire avec celle de Notations
herbelin
2003-05-21
*
*** empty log message ***
barras
2003-03-12
*
Remplacement Grammar par Notation
herbelin
2002-12-02
*
Remplacement de Syntactic Definition par Notation
herbelin
2002-12-02
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Modification de l'emplacement des fichiers pour les setoides.
clrenard
2001-09-18
*
Passage au nouveau Destruct
herbelin
2001-08-07
*
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-08-05
*
Ajout des fichiers pour le Ring pour setoides
clrenard
2001-07-10