aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Peano.v
Commit message (Collapse)AuthorAge
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
* DocumentationGravatar herbelin2005-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai d'utilisation de 'where' pour les notationsGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur PeanoGravatar herbelin2003-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lemmes dans un sens plus naturelGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4881 85f007b7-540e-0410-9357-904b9bb8a0f7
* nat_scope ouvert par defautGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵Gravatar herbelin2003-09-23
| | | | | | TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
| | | | | | | extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵Gravatar herbelin2003-09-21
| | | | | | aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵Gravatar herbelin2003-09-19
| | | | | | meme si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bind et Delimit pour natGravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Concentration des notations officielles dans Init/Notations; restructuration ↵Gravatar herbelin2003-05-21
| | | | | | de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
* BlancsGravatar herbelin2003-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de minus dans PeanoGravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3810 85f007b7-540e-0410-9357-904b9bb8a0f7
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2672 85f007b7-540e-0410-9357-904b9bb8a0f7
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2671 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifs incongrues dans le précédent commitGravatar herbelin2002-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2385 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'Export redondantsGravatar herbelin2001-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2190 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation automatique de la bibliothèque standardGravatar filliatr2001-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* - méthode load sur les HintsGravatar filliatr1999-12-13
| | | | | | | | - CAST pris en compte dans Astterm - Coercin.lookup_path_to_sort_from protégé par un try/with git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@248 85f007b7-540e-0410-9357-904b9bb8a0f7
* fichiers prelude CoqGravatar filliatr1999-12-13
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@243 85f007b7-540e-0410-9357-904b9bb8a0f7