aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zmisc.v
AgeCommit message (Collapse)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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
This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5.
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- 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
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-27Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14241 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
All the functions about Z is now in a separated file BinIntDef, which is Included in BinInt.Z. This BinInt.Z directly implements ZAxiomsSig, and instantiates derived properties ZProp. Note that we refer to Z instead of t inside BinInt.Z, otherwise ring breaks later on @eq Z.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-18Some more revision of {P,N,Z}Arith + bitwise ops in Ndigitsletouzey
Initial plan was only to add shiftl/shiftr/land/... to N and other number type, this is only partly done, but this work has diverged into a big reorganisation and improvement session of PArith,NArith,ZArith. Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a) PArith/BinPos: - added a power function Ppow - iterator iter_pos moved from Zmisc to here + some lemmas - added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2 - more lemmas on Pcompare and succ/+/* and order, allow to simplify a lot some old proofs elsewhere. - new/revised results on Pminus (including some direct proof of stuff from Pnat) PArith/Pnat: - more direct proofs (limit the need of stuff about Pmult_nat). - provide nicer names for some lemmas (eg. Pplus_plus instead of nat_of_P_plus_morphism), compatibility notations provided. - kill some too-specific lemmas unused in stdlib + contribs NArith/BinNat: - N_of_nat, nat_of_N moved from Nnat to here. - a lemma relating Npred and Nminus - revised definitions and specification proofs of Npow and Nlog2 NArith/Nnat: - shorter proofs. - stuff about Z_of_N is moved to Znat. This way, NArith is entirely independent from ZArith. NArith/Ndigits: - added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr - revised proofs about Nxor, still using functional bit stream - use the same approach to prove properties of Nand Nor Ndiff ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N ZArith/Zmisc: almost empty new, only contain stuff about badly-named iter. Should be reformed more someday. ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes proofs and avoid slowdown due to adding 1 in Z instead of in positive Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt as long as I dont't know why it's slower on powers of two. Elsewhere: propagate new names + some nicer proofs NB: Impact on compatibility is probably non-zero, but should be really moderate. We'll see on contribs, but a few Require here and there might be necessary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- 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
2009-11-02Remove various useless {struct} annotationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-07adds a theorem to reason at the level of Zbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12119 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
- Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum ↵letouzey
part). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4973 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout lemmes; independance vis a vis noms variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, ↵herbelin
de la partie Omega dans contrib/omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Documentation/Structurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4702 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13suite changements ZArith en vu de librairie FSetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4149 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13quelques adaptations de Zarith en vu de la nouvelle librarie FSetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4148 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Ajout Open Scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3890 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-09Making the sumbool functions transparent, so that they can used tobertot
compute even inside Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2846 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-05nouveau module Zdivfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2614 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11Conformité des commentaires au format coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1951 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1914 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Library doc adjustments (until page 140)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19remplace Zarith par ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 17:52:01 +0000