diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:09 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:09 +0000 |
| commit | f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 (patch) | |
| tree | 3808b3b5a9fc4a380307545e10845882300ef6aa /plugins/nsatz | |
| parent | 81d7335ba1a07a7a30e206ae3ffc4412f3a54f46 (diff) | |
Definitions of positive, N, Z moved in Numbers/BinNums.v
In the coming reorganisation, the name Z in BinInt will be a
module containing all code and properties about binary integers.
The inductive type Z hence cannot be at the same location.
Same for N and positive. Apart for this naming constraint, it
also have advantages : presenting the three types at once is
clearer, and we will be able to refer to N in BinPos (for instance
for output type of a predecessor function on positive).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/nsatz.ml4 | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 2b5a3e7c8..4b8b706d4 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -180,21 +180,24 @@ let ttmul = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEmul") let ttopp = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEopp") let ttpow = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEpow") -let tlist = lazy (gen_constant "CC" ["Lists";"List"] "list") -let lnil = lazy (gen_constant "CC" ["Lists";"List"] "nil") -let lcons = lazy (gen_constant "CC" ["Lists";"List"] "cons") +let datatypes = ["Init";"Datatypes"] +let binnums = ["Numbers";"BinNums"] -let tz = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z") -let z0 = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z0") -let zpos = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Zpos") -let zneg = lazy(gen_constant "CC" ["ZArith";"BinInt"] "Zneg") +let tlist = lazy (gen_constant "CC" datatypes "list") +let lnil = lazy (gen_constant "CC" datatypes "nil") +let lcons = lazy (gen_constant "CC" datatypes "cons") -let pxI = lazy(gen_constant "CC" ["PArith";"BinPos"] "xI") -let pxO = lazy(gen_constant "CC" ["PArith";"BinPos"] "xO") -let pxH = lazy(gen_constant "CC" ["PArith";"BinPos"] "xH") +let tz = lazy (gen_constant "CC" binnums "Z") +let z0 = lazy (gen_constant "CC" binnums "Z0") +let zpos = lazy (gen_constant "CC" binnums "Zpos") +let zneg = lazy(gen_constant "CC" binnums "Zneg") -let nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0") -let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos") +let pxI = lazy(gen_constant "CC" binnums "xI") +let pxO = lazy(gen_constant "CC" binnums "xO") +let pxH = lazy(gen_constant "CC" binnums "xH") + +let nN0 = lazy (gen_constant "CC" binnums "N0") +let nNpos = lazy(gen_constant "CC" binnums "Npos") let mkt_app name l = mkApp (Lazy.force name, Array.of_list l) |