diff options
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 5070f89ed..b235b5821 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 cd4a7d3b0..a520ce2d4 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 15d11eca2..fb8de1f92 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" |