aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring/Ring_normalize.v
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2008-05-09Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]herbelin
2008-04-29Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laherbelin
2006-11-13Encore des _sym au lieu de _commherbelin
2006-09-26commit de field + renommagesbarras
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2004-11-12Changement dans les boxed values .gregoire
2004-07-16Nouvelle en-têteherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-10-28Ajout notations pour les expressions dans un anneauherbelin
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2002-11-28Nettoyageherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:15:07 +0000