diff options
| author | Vincent Laporte | 2020-12-02 16:57:04 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2020-12-02 16:57:04 +0100 |
| commit | 11730fa0ed2cb10da1ffc00f4f1140572134937e (patch) | |
| tree | 775a310bd094e5c9149ef353abc251e8e5d657cc /plugins | |
| parent | ad8cf0108e628710128e5a6e266b72895eed98b9 (diff) | |
| parent | 853b838681db635f51fc3c7ba3dfe26bc6712d72 (diff) | |
Merge PR #13275: Put all Int63 primitives in a separate file
Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/syntax/int63_syntax.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml index b14b02f3bb..110b26581f 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" |