aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring/Ring_normalize.v
AgeCommit message (Expand)Author
2002-05-15- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusbarras
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-07-10Ajout d'un Ring pour setoidesclrenard
2001-03-15entetesfilliatr
2001-03-01De bizarres SR_pus_assoc au lieu de SR_plus_assocherbelin
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
2000-11-28Elimination du 'delahaye
2000-11-21implicites manuelsfilliatr
2000-10-23Modifications pour implicites améliorésherbelin
2000-06-21 - $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)filliatr
2000-06-21Ringfilliatr