aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring/Ring_normalize.v
Commit message (Expand)AuthorAge
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* Encore des _sym au lieu de _commGravatar herbelin2006-11-13
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Ajout notations pour les expressions dans un anneauGravatar herbelin2003-10-28
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* 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-06 00:35:08 +0000