aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Peano.v
Commit message (Expand)AuthorAge
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* ugly comment erroneously left in the minus definitionGravatar letouzey2008-10-14
* Changing the definitions of pred and minus in the style of GGGravatar werner2008-06-12
* Petites corrections diverses :Gravatar herbelin2008-06-02
* - Modification de la déf de minus et pred conformément aux remarques deGravatar herbelin2008-05-28
* Mise en forme des theoriesGravatar notin2006-10-17
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* DocumentationGravatar herbelin2005-05-19
* Essai d'utilisation de 'where' pour les notationsGravatar herbelin2005-02-04
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Backtrack sur PeanoGravatar herbelin2003-11-14
* Lemmes dans un sens plus naturelGravatar herbelin2003-11-12
* nat_scope ouvert par defautGravatar herbelin2003-10-10
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...Gravatar herbelin2003-09-23
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
* Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...Gravatar herbelin2003-09-21
* Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...Gravatar herbelin2003-09-19
* Bind et Delimit pour natGravatar herbelin2003-09-12
* Concentration des notations officielles dans Init/Notations; restructuration ...Gravatar herbelin2003-05-21
* BlancsGravatar herbelin2003-04-29
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
* Déplacement de minus dans PeanoGravatar herbelin2003-03-29
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Modifs incongrues dans le précédent commitGravatar herbelin2002-01-10
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
* Suppression d'Export redondantsGravatar herbelin2001-11-14
* documentation automatique de la bibliothèque standardGravatar filliatr2001-04-11
* entetesGravatar filliatr2001-03-15
* - méthode load sur les HintsGravatar filliatr1999-12-13
* fichiers prelude CoqGravatar filliatr1999-12-13