From c408e819ce39b27f0842c84b1b24c585ac5b6086 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 01:14:50 +0100 Subject: [lib] [api] Introduce record for `object_prefix` This is a minor cleanup adding a record in a try to structure the state living in `Lib`. --- printing/prettyp.ml | 20 ++++++++++---------- printing/printmod.ml | 6 +++--- 2 files changed, 13 insertions(+), 13 deletions(-) (limited to 'printing') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8fc00ed96..8b21ff761 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -359,10 +359,10 @@ let pr_located_qualid = function str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) | Dir dir -> let s,dir = match dir with - | DirOpenModule (dir,_) -> "Open Module", dir - | DirOpenModtype (dir,_) -> "Open Module Type", dir - | DirOpenSection (dir,_) -> "Open Section", dir - | DirModule (dir,_) -> "Module", dir + | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir + | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir + | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir + | DirModule { obj_dir ; _ } -> "Module", obj_dir | DirClosedSection dir -> "Closed Section", dir in str s ++ spc () ++ DirPath.print dir @@ -409,7 +409,7 @@ let locate_term qid = let locate_module qid = let all = Nametab.locate_extended_all_dir qid in let map dir = match dir with - | DirModule (_, (mp, _)) -> Some (Dir dir, Nametab.shortest_qualid_of_module mp) + | DirModule { obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp) | DirOpenModule _ -> Some (Dir dir, qid) | _ -> None in @@ -645,8 +645,8 @@ let gallina_print_library_entry env sigma with_values ent = Some (str " >>>>>>> Section " ++ pr_name oname) | (oname,Lib.ClosedSection _) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) - | (_,Lib.CompilingLibrary (dir,_)) -> - Some (str " >>>>>>> Library " ++ DirPath.print dir) + | (_,Lib.CompilingLibrary { obj_dir; _ }) -> + Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) | (oname,Lib.ClosedModule _) -> @@ -775,8 +775,8 @@ let read_sec_context r = with Not_found -> user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function - | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> - if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest + | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> + if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | (_,Lib.ClosedSection _)::rest -> user_err Pp.(str "Cannot print the contents of a closed section.") (* LEM: Actually, we could if we wanted to. *) @@ -798,7 +798,7 @@ let print_any_name env sigma = function | Term (ConstructRef ((sp,_),_)) -> print_inductive sp | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn - | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp + | Dir (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 diff --git a/printing/printmod.ml b/printing/printmod.ml index 13a03e9b4..dd2e99d58 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -237,10 +237,10 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn -let nametab_register_dir mp = +let nametab_register_dir obj_mp = let id = mk_fake_top () in - let dir = DirPath.make [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))) + let obj_dir = DirPath.make [id] in + Nametab.push_dir (Nametab.Until 1) obj_dir (DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty }) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here -- cgit v1.2.3