aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Peano.v
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Some simplifications in NZDomainGravatar letouzey2011-06-20
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* First release of Vector library.Gravatar pboutill2010-12-10
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
* - 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