aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Peano.v
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-08-25Modify Init/Peano.v to compile with -mangle-names.Jasper Hugunin
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-08-31Numeral Notation for natPierre Letouzey
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2018-01-03Fix core hint database issue #6521Anton Trunov
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2012-12-21nat_iter n f x -> nat_rect _ x (fun _ => f) npboutill
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-06-20Some simplifications in NZDomainletouzey
2011-05-05Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)letouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-10First release of Vector library.pboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-17Arith's min and max placed in Peano (+basic specs max_l and co)letouzey
2009-11-02Remove various useless {struct} annotationsletouzey
2009-08-11Fixed extra space in printing notation { x & P } + minor other thingsherbelin
2008-12-26- Optimized "auto decomp" which had a (presumably) exponential inherbelin
2008-10-14ugly comment erroneously left in the minus definitionletouzey
2008-06-12Changing the definitions of pred and minus in the style of GGwerner
2008-06-02Petites corrections diverses :herbelin
2008-05-28- Modification de la déf de minus et pred conformément aux remarques deherbelin
2006-10-17Mise en forme des theoriesnotin
2006-03-17Modification des propriétés (svn:executable)notin
2005-05-19Documentationherbelin
2005-02-04Essai d'utilisation de 'where' pour les notationsherbelin
2004-11-12Changement dans les boxed values .gregoire
2004-07-16Nouvelle en-têteherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-14Backtrack sur Peanoherbelin
2003-11-12Lemmes dans un sens plus naturelherbelin
2003-10-10nat_scope ouvert par defautherbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:16:53 +0000