aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/ArithProp.v
AgeCommit message (Collapse)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26commit de field + renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout et MAJ commandes de scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4375 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-12Open Scope en Localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3917 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Remplacement Import par Open Scope en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21MAJ ArithPropdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Renommage de RealsB en Rbasedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Réorganisation de la librairie des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7