diff options
| author | Pierre Roux | 2020-10-26 14:43:05 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-12-02 09:26:53 +0100 |
| commit | 853b838681db635f51fc3c7ba3dfe26bc6712d72 (patch) | |
| tree | 0b23386f296313f4fae2a0db293e1f441834f7e4 /plugins/syntax/int63_syntax.ml | |
| parent | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff) | |
Put all Int63 primitives in a separate file
Following a request from Pierre-Marie Pédrot in #13258
Diffstat (limited to 'plugins/syntax/int63_syntax.ml')
| -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 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" |