index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Init
/
Peano.v
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove v62 from stdlib.
Théo Zimmermann
2016-10-24
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Update headers.
Maxime Dénès
2015-01-12
*
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2014-07-09
*
nat_iter n f x -> nat_rect _ x (fun _ => f) n
pboutill
2012-12-21
*
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-26
*
Updating headers.
herbelin
2012-08-08
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Some simplifications in NZDomain
letouzey
2011-06-20
*
Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)
letouzey
2011-05-05
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
First release of Vector library.
pboutill
2010-12-10
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Arith's min and max placed in Peano (+basic specs max_l and co)
letouzey
2010-02-17
*
Remove various useless {struct} annotations
letouzey
2009-11-02
*
Fixed extra space in printing notation { x & P } + minor other things
herbelin
2009-08-11
*
- Optimized "auto decomp" which had a (presumably) exponential in
herbelin
2008-12-26
*
ugly comment erroneously left in the minus definition
letouzey
2008-10-14
*
Changing the definitions of pred and minus in the style of GG
werner
2008-06-12
*
Petites corrections diverses :
herbelin
2008-06-02
*
- Modification de la déf de minus et pred conformément aux remarques de
herbelin
2008-05-28
*
Mise en forme des theories
notin
2006-10-17
*
Modification des propriétés (svn:executable)
notin
2006-03-17
*
Documentation
herbelin
2005-05-19
*
Essai d'utilisation de 'where' pour les notations
herbelin
2005-02-04
*
Changement dans les boxed values .
gregoire
2004-11-12
*
Nouvelle en-tête
herbelin
2004-07-16
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Backtrack sur Peano
herbelin
2003-11-14
*
Lemmes dans un sens plus naturel
herbelin
2003-11-12
*
nat_scope ouvert par defaut
herbelin
2003-10-10
*
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-09-23
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...
herbelin
2003-09-21
*
Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...
herbelin
2003-09-19
*
Bind et Delimit pour nat
herbelin
2003-09-12
*
Concentration des notations officielles dans Init/Notations; restructuration ...
herbelin
2003-05-21
*
Blancs
herbelin
2003-04-29
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
Déplacement de minus dans Peano
herbelin
2003-03-29
*
lemmes plus_O_n et plus_Sn_m (pour Yves)
filliatr
2002-05-07
*
lemmes plus_O_n et plus_Sn_m (pour Yves)
filliatr
2002-05-07
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
Modifs incongrues dans le précédent commit
herbelin
2002-01-10
*
MAJ des Id pour coqweb
herbelin
2002-01-09
*
Suppression d'Export redondants
herbelin
2001-11-14
*
documentation automatique de la bibliothèque standard
filliatr
2001-04-11
[next]