aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Rdefinitions.v
AgeCommit message (Expand)Author
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-02-27Restructuration des hints pour qu'Auto fasse moins de détours et lesherbelin
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
2002-02-14option -dump-glob pour coqdocfilliatr
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19Mise de (*i autour CVS infomohring
2001-03-15entetesfilliatr
2000-11-23Ajout d'une syntaxe pour Reals.mayero