| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
A sub-module N in BinNat now contains functions add (ex-Nplus),
mul (ex-Nmult), ... and properties.
In particular, this sub-module N directly instantiates NAxiomsSig
and includes all derived properties NProp.
Files Ndiv_def and co are now obsolete and kept only for compat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- we use a wrapper file big.ml to have short names about big_int
and specialized functions for extraction
- new files : ExtrOcamlZInt for Z==>int and N==>int,
ExtrOcamlZBigInt for Z==>big_int and N==>big_int
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
