aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring/Setoid_ring_normalize.v
Commit message (Expand)AuthorAge
* distinguer interp_cs et interp_setcsGravatar letouzey2003-10-06
* Alignement du comportement des implicites d'inductif en sortie de section sur...Gravatar herbelin2003-04-09
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* NettoyageGravatar herbelin2002-11-28
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* MAJ vis à vis de la nouvelle non-localité des Remark/FactGravatar herbelin2001-09-14
* ParsingGravatar herbelin2001-08-10
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* Setoid_rewrite -> RewriteGravatar clrenard2001-07-10
* Ajout des fichiers pour le Ring pour setoidesGravatar clrenard2001-07-10