aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/int63_syntax.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index 5f4db8e800..494500ca25 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -20,14 +20,14 @@ open Libnames
(*** Constants for locating int63 constructors ***)
-let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.int"
-let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.id_int"
+let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int"
+let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.id_int"
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
(* int63 stuff *)
-let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "Int63"]
+let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"]
let int63_path = make_path int63_module "int"
let int63_scope = "int63_scope"