aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Rdefinitions.v
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
2008-04-04- Amélioration de la présentation de RIneq, même si un nettoyage desherbelin
2006-12-11Changement dans le kernel : bgregoir
2006-10-17Mise en forme des theoriesnotin
2004-07-16Nouvelle en-têteherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-19Restauration compatibilite 7.4 pour le Hint Unfold Rgtherbelin
2003-10-20R passe dans Set !herbelin
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