aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rbase.v
Commit message (Expand)AuthorAge
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...Gravatar herbelin2003-09-23
* Renommage de RealsB en RbaseGravatar desmettr2003-01-16
* Nouvelle interprétation des nombres réelsGravatar desmettr2003-01-15
* Réorganisation de la librairie des réelsGravatar desmettr2002-11-27
* *** empty log message ***Gravatar desmettr2002-06-20
* Ajout d'occurrences de Field (ne pas enlever)Gravatar delahaye2002-05-31
* Double Induction prend maintenant des noms d'hyppthèsesGravatar herbelin2002-05-29
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* OptimisationGravatar desmettr2002-04-02
* Intuition ne fait plus de Unfold des constantes (il faut les faireGravatar courant2002-03-21
* Intuition now takes an (optional) tactic as parameter. This tactic isGravatar courant2002-03-20
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* *** empty log message ***Gravatar desmettr2001-12-07
* *** empty log message ***Gravatar desmettr2001-12-07
* *** empty log message ***Gravatar desmettr2001-12-05
* *** empty log message ***Gravatar desmettr2001-12-05
* *** empty log message ***Gravatar desmettr2001-12-05
* Integration de nouveaux lemmesGravatar desmettr2001-11-30
* *** empty log message ***Gravatar desmettr2001-11-30
* Intégration de nouveaux lemmes.Gravatar desmettr2001-11-30
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* Oubli Save + je sais plusGravatar mayero2001-06-19
* Ajouts de lemmes (pour Float)Gravatar mayero2001-06-18
* Ajouts RealsGravatar mayero2001-04-23
* Minor layout adjustments for Library docGravatar coq2001-04-23
* Ajout tactics RealsGravatar mayero2001-04-20
* Library doc adjustments (until page 140)Gravatar coq2001-04-20
* Changement syntax pour RinvGravatar mayero2001-04-19
* Ajout de FieldGravatar delahaye2001-04-19
* entetesGravatar filliatr2001-03-15
* Renommage des variables dans les schémas d'inductionGravatar herbelin2001-02-14
* 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
* mise-a-jour, ajouts de quelques truc...Gravatar mayero2000-11-10
* Pour ne plus éviter temporairement le "Auto with zarith" !Gravatar herbelin2000-11-05
* Pour eviter temporairement le "Auto with zarith"Gravatar delahaye2000-10-30
* theories/RealsGravatar filliatr2000-06-21