coq/theories/PArith/vo.itarget, branch master

drop vo.itarget files and compute the corresponding the corresponding values automatically instead

2017-06-01T15:33:19+00:00

BinPosDef: a module with all code about positive, later Included in BinPos

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

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

Modularization of BinPos + fixes in Stdlib

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

 BinPos now contain a sub-module Pos, in which are placed functions
 like add (ex-Pplus), mul (ex-Pmult), ... and properties like
 add_comm, add_assoc, ...

 In addition to the name changes, the organisation is changed quite
 a lot, to try to take advantage more of the orders < and <= instead
 of speaking only of the comparison function.

 The main source of incompatibilities in scripts concerns this compare:
 Pos.compare is now a binary operation, expressed in terms of the
 ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
 this ternary version being called now Pos.compare_cont. As for everything
 else, compatibility notations (only parsing) are provided. But notations
 "_ ?= _" on positive will have to be edited, since they now point to
 Pos.compare.

 We also make the sub-module Pos to be directly an OrderedType,
 and include results about min and max.

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

Numbers: axiomatization, properties and implementations of gcd

2010-11-05T18:27:39+00:00

 - For nat, we create a brand-new gcd function, structural in
   the sense of Coq, even if it's Euclid algorithm. Cool...
 - We re-organize the Zgcd that was in Znumtheory, create out of it
   files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised
   in order to be much simpler (no omega, no advanced lemmas of
   Znumtheory, etc).
 - Abstract Properties NZGcd / ZGcd / NGcd could still be completed,
   for the moment they contain up to Gauss thm. We could add stuff
   about (relative) primality, relationship between gcd and div,mod,
   or stuff about parity, etc etc.
 - Znumtheory remains as it was, apart for Zgcd and correctness proofs
   gone elsewhere. We could later take advantage of ZGcd in it.
   Someday, we'll have to switch from the current Zdivide inductive,
   to Zdivide' via exists. To be continued...

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

Move stuff about positive into a distinct PArith subdir

2010-11-02T14:44:08+00:00

 Beware! after this, a ./configure must be done. It might also
 be a good idea to chase any phantom .vo remaining after a make clean

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