diff options
| author | letouzey | 2010-11-02 14:44:08 +0000 |
|---|---|---|
| committer | letouzey | 2010-11-02 14:44:08 +0000 |
| commit | df7acfad0ce0270b62644a5e9f8709ed0e7936e6 (patch) | |
| tree | 746850496c47f6618219ad5d5560f021b7b8e56b /plugins | |
| parent | e5c4bc888c1f0516928a32f70529f95e36243c5d (diff) | |
Move stuff about positive into a distinct PArith subdir
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/nsatz/nsatz.ml4 | 6 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/z_syntax.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 5070f89ed7..b235b58214 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -189,9 +189,9 @@ 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 pxI = lazy(gen_constant "CC" ["NArith";"BinPos"] "xI") -let pxO = lazy(gen_constant "CC" ["NArith";"BinPos"] "xO") -let pxH = lazy(gen_constant "CC" ["NArith";"BinPos"] "xH") +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 nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0") let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos") diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index cd4a7d3b08..a520ce2d43 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -36,7 +36,7 @@ let l_true_equals_true = [|data_constant "bool";data_constant "true"|])) let pos_constant = - Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"] + Coqlib.gen_constant "refl_tauto" ["PArith";"BinPos"] let l_xI = lazy (pos_constant "xI") let l_xO = lazy (pos_constant "xO") diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 15d11eca2d..fb8de1f927 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -23,7 +23,7 @@ exception Non_closed_number open Libnames open Rawterm let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let positive_module = ["Coq";"NArith";"BinPos"] +let positive_module = ["Coq";"PArith";"BinPos"] let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) let positive_path = make_path positive_module "positive" |