diff options
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) |