aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Raxioms.v
Commit message (Expand)AuthorAge
* sumboolT, sumorT, sigTT, SigT redondantsGravatar herbelin2003-04-16
* Open Scope en LocalGravatar herbelin2003-04-12
* Remplacement Import par Open Scope en v8Gravatar herbelin2003-04-10
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementGravatar filliatr2002-06-21
* *** empty log message ***Gravatar desmettr2002-06-20
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Changement syntax pour RinvGravatar mayero2001-04-19
* entetesGravatar filliatr2001-03-15
* Modif de l'axiomatisation pour enlever les /\ de _neGravatar mayero2001-01-25
* Mise a jour RbaseGravatar mohring2001-01-11
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23
* correctionGravatar mayero2000-07-04
* ajoutsGravatar mayero2000-07-03
* theories/RealsGravatar filliatr2000-06-21