aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring/Ring_abstract.v
AgeCommit message (Expand)Author
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-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-05-15- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusbarras
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-05-14réparation Ring (simplifications)filliatr
2001-03-15entetesfilliatr
2001-01-09Meta Definition -> Tactic Definitiondelahaye
2001-01-09Tactic Definition -> Meta Definitiondelahaye
2000-11-07Correction sur commit errone de la version 1.3herbelin
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
2000-10-24Syntaxe des tactiquesherbelin
2000-06-21Ringfilliatr