diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/ptactic.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 14 |
3 files changed, 9 insertions, 9 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index 950ef30b53..e53043fb19 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -98,7 +98,7 @@ open Equality let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0) let lt = ConstRef (coq_constant ["Init";"Peano"] "lt") let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded") -let z = IndRef (coq_constant ["Zarith";"fast_integer"] "Z", 0) +let z = IndRef (coq_constant ["ZArith";"fast_integer"] "Z", 0) let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0) let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 0d15dc58e7..355abd135a 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -42,7 +42,7 @@ Hashtbl.add type_table "Coq.Init.Datatypes.prod" Hashtbl.add type_table "Coq.Init.Datatypes.nat" [|[|"";"O"; "S"|]|];; -Hashtbl.add type_table "Coq.Zarith.fast_integer.Z" +Hashtbl.add type_table "Coq.ZArith.fast_integer.Z" [|[|"";"ZERO";"POS";"NEG"|]|];; Hashtbl.add type_table "Coq.Zarith.fast_integer.positive" diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 16bbd614f1..e17336a71a 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -229,7 +229,7 @@ let constant dir s = (Nametab.string_of_qualid (Nametab.make_qualid dir id))) let arith_constant dir = constant ("Arith"::dir) -let zarith_constant dir = constant ("Zarith"::dir) +let zarith_constant dir = constant ("ZArith"::dir) let logic_constant dir = constant ("Logic"::dir) (* fast_integer *) @@ -398,12 +398,12 @@ let make_coq_path dir s = (Nametab.string_of_qualid (Nametab.make_qualid dir id))^ " is not a constant") -let sp_Zs = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zs") -let sp_Zminus = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zminus") -let sp_Zle = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zle") -let sp_Zgt = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zgt") -let sp_Zge = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zge") -let sp_Zlt = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zlt") +let sp_Zs = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zs") +let sp_Zminus = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zminus") +let sp_Zle = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zle") +let sp_Zgt = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zgt") +let sp_Zge = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zge") +let sp_Zlt = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zlt") let sp_not = lazy (make_coq_path ["Init";"Logic"] "not") let mk_var v = mkVar (id_of_string v) |