diff options
| author | letouzey | 2011-05-05 15:12:09 +0000 |
|---|---|---|
| committer | letouzey | 2011-05-05 15:12:09 +0000 |
| commit | f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 (patch) | |
| tree | 3808b3b5a9fc4a380307545e10845882300ef6aa /interp | |
| 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 'interp')
| -rw-r--r-- | interp/coqlib.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index ac1aa1879c..0f3d1bab2a 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -91,12 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s let arith_dir = ["Coq";"Arith"] let arith_modules = [arith_dir] +let numbers_dir = [ "Coq";"Numbers"] let parith_dir = ["Coq";"PArith"] - let narith_dir = ["Coq";"NArith"] - let zarith_dir = ["Coq";"ZArith"] -let zarith_base_modules = [parith_dir;narith_dir;zarith_dir] + +let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir] let init_dir = ["Coq";"Init"] let init_modules = [ |