diff options
| author | Emilio Jesus Gallego Arias | 2018-10-31 09:39:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-31 12:58:02 +0100 |
| commit | 0adc2073cf3e7bd3b2d9ee2cdf75e16e3a243c44 (patch) | |
| tree | 5d7212f3462f7e650238906768a4bfd199ec9091 /printing/prettyp.ml | |
| parent | e29dc5ab5e85eb5f740de83f9f0b97b233651a3e (diff) | |
[nametab] Move global_dir_reference to Nametab
This type is "private" to the Nametab, which manages it. It thus makes
sense IMHO to live there.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 4619e049e0..96720e84d6 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -326,7 +326,7 @@ type locatable = Locatable : 'a locatable_info -> locatable type logical_name = | Term of GlobRef.t - | Dir of global_dir_reference + | Dir of Nametab.GlobDirRef.t | Syntactic of KerName.t | ModuleType of ModPath.t | Other : 'a * 'a locatable_info -> logical_name @@ -367,7 +367,7 @@ let pr_located_qualid = function | Syntactic kn -> str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) | Dir dir -> - let s,dir = match dir with + let s,dir = let open Nametab.GlobDirRef in match dir with | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir @@ -416,7 +416,7 @@ let locate_term qid = let locate_module qid = let all = Nametab.locate_extended_all_dir qid in - let map dir = match dir with + let map dir = let open Nametab.GlobDirRef in match dir with | DirModule { obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp) | DirOpenModule _ -> Some (Dir dir, qid) | _ -> None @@ -429,7 +429,7 @@ let locate_modtype qid = let modtypes = List.map map all in (** Don't forget the opened module types: they are not part of the same name tab. *) let all = Nametab.locate_extended_all_dir qid in - let map dir = match dir with + let map dir = let open Nametab.GlobDirRef in match dir with | DirOpenModtype _ -> Some (Dir dir, qid) | _ -> None in @@ -788,7 +788,7 @@ let print_any_name env sigma na udecl = | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn - | Dir (DirModule { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp + | Dir (Nametab.GlobDirRef.DirModule { obj_dir; obj_mp; _ } ) -> print_module (printable_body obj_dir) obj_mp | Dir _ -> mt () | ModuleType mp -> print_modtype mp | Other (obj, info) -> info.print obj |