coq/theories/Numbers/Integer/Binary, branch master

Update headers in the whole code base.

2020-03-18T11:15:43+00:00

Add headers to a few files which were missing them.

Update ml-style headers to new year.

2019-06-17T16:08:32+00:00

Update headers following #6543.

2018-02-27T16:57:50+00:00

Bump year in headers.

2017-07-04T12:20:57+00:00

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

Modularization of BinInt, related fixes in the stdlib

2011-05-05T15:12:59+00:00

 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

An automatic substitution of scope at functor application

2011-02-11T16:54:20+00:00

 For Argument Scope, we now record types (more precisely classes cl_typ)
 in addition to scope list. After substitution (e.g. at functor application),
 the new types are used to search for corresponding concrete scopes.

 Currently, this automatic scope substitution of argument scope takes
 precedence (if successful) over scope declared in the functor (even
 by the user). On the opposite, the manual scope substitution
 (cf last commit introducing annotation [scope foo to bar])
 is done _after_ the automatic scope substitution.

 TODO: if this behavior is satisfactory, document it ...

 Note that Classops.find_class_type lose its env args since it was
 actually unused, and is now used for Notation.find_class

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