aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring/Ring_normalize.v
Commit message (Expand)AuthorAge
* NettoyageGravatar herbelin2002-11-28
* - abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusGravatar barras2002-05-15
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* Ajout d'un Ring pour setoidesGravatar clrenard2001-07-10
* entetesGravatar filliatr2001-03-15
* De bizarres SR_pus_assoc au lieu de SR_plus_assocGravatar herbelin2001-03-01
* Renommage des variables dans les schémas d'inductionGravatar herbelin2001-02-14
* Elimination du 'Gravatar delahaye2000-11-28
* implicites manuelsGravatar filliatr2000-11-21
* Modifications pour implicites améliorésGravatar herbelin2000-10-23
* - $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)Gravatar filliatr2000-06-21
* RingGravatar filliatr2000-06-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-12 12:47:24 +0000