aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Peano.v
Commit message (Collapse)AuthorAge
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some simplifications in NZDomainGravatar letouzey2011-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
* First release of Vector library.Gravatar pboutill2010-12-10
| | | | | | | | | | To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
| | | | | | | This allow for instance to remove the dependency of List.v toward Min.v To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
| | | | | | (shorter proof of O_S in trunk + typo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12271 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
| | | | | | | | | the number of conjunctions to split. - A few cleaning and uniformisation in auto.ml. - Removal of v62 hints already in core. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
* ugly comment erroneously left in the minus definitionGravatar letouzey2008-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing the definitions of pred and minus in the style of GGGravatar werner2008-06-12
| | | | | | | | in order for them to preserve the structural order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petites corrections diverses :Gravatar herbelin2008-06-02
| | | | | | | | | | | - bug d'installation (coq_config.cmo était installé une 2ème fois au lieu d'installer coq_config.cmx) - suite nettoyage configure, option reals - ajout d'une option "only parsing" oubliée dans Peano.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11035 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Modification de la déf de minus et pred conformément aux remarques deGravatar herbelin2008-05-28
| | | | | | | | | | | Assia et Benjamin W. de telle sorte qu'ils respectent le critère de décroissance structurelle lorsqu'utilisés dans un point-fixe. - Ajout des noms "standard" des lemmes de Peano et correction d'un nom de BinInt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11015 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 09:08:24 +0000