aboutsummaryrefslogtreecommitdiff
path: root/theories/Arith/Div2.v
AgeCommit message (Expand)Author
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
2003-03-31Ajout double_plusherbelin
2003-03-29Implicit Variables Typeherbelin
2003-03-12*** empty log message ***barras
2002-02-14option -dump-glob pour coqdocfilliatr
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-04-19Remplacement Euclid_def Euclid_proof par Euclidmohring
2001-03-15entetesfilliatr
2000-12-20Oublié de supprimer du code mortherbelin
2000-12-20Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...herbelin
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
2000-05-22Changement nommage des hypothèses; parenthèses pour les tactiquesherbelin
2000-05-18parethèses de tactiquesherbelin
2000-03-10mise sous CVS du repertoire theories/Arithfilliatr