coq/theories/Numbers/Natural/SpecViaZ, branch master

BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)

2017-06-13T08:30:29+00:00

 See now https://github.com/coq/bignums
 Int31 is still in the stdlib.
 Some proofs there has be adapted to avoid the need for BigNumPrelude.

Update copyright headers.

2016-01-20T16:33:09+00:00

Update headers.

2015-01-12T13:24:46+00:00

Updating headers.

2012-08-08T18:56:15+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7

ZArith + other : favor the use of modern names instead of compat notations

2012-07-05T16:56:16+00:00

 - 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

theories/, plugins/ and test-suite/ ported to the Arguments vernacular

2011-11-21T17:03:52+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7

Cleanup of files related with power over Z.

2011-07-01T17:38:17+00:00

 - Zpow_def, Zpower, Zpow_facts shortened thanks to stuff in BinInt.Z

 - The alternative Zpower_alt is now in a separate file Zpow_alt.v,
   not loaded by default.

 - Some more injection lemmas in Znat (pow, div, mod, quot, rem)

 - Btw, added a "square" function in Z, N, Pos, ... (instead of
   Zpow_facts.Zsquare).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14253 85f007b7-540e-0410-9357-904b9bb8a0f7

Cleanup in SpecViaZ

2011-06-30T14:40:52+00:00

 Note that in NSig (and hence NMake and BigN), to_N is now
 Z.to_N (to_Z ...) instead of Z.abs_N (to_Z ...). This doesn't
 change the result (since to_Z create non-negative integers),
 but some proofs may have to be adapted

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14250 85f007b7-540e-0410-9357-904b9bb8a0f7

Cleanup of Ndigits

2011-06-30T14:40:50+00:00

 - No need for compatibility notations for stuff introduced strictly
   after branching of 8.3, for instance Nor, Nand, etc.
 - Properties for N.lor, N.lxor, etc are now in BinNat.N, no need to
   duplicate them in Ndigits, apart from the few compatibility results
   about xor.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14249 85f007b7-540e-0410-9357-904b9bb8a0f7

Deletion of useless Zdigits_def

2011-06-28T23:30:32+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7