aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rdefinitions.v
Commit message (Expand)AuthorAge
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Library doc adjustments (until page 140)Gravatar coq2001-04-20
* Mise de (*i autour CVS infoGravatar mohring2001-04-19
* entetesGravatar filliatr2001-03-15
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23