diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 32 |
1 files changed, 15 insertions, 17 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 602b7a4965..647111bbe1 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -360,10 +360,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 @@ -410,7 +410,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 @@ -649,8 +649,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 _) -> @@ -779,8 +779,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. *) @@ -811,7 +811,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(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 @@ -903,18 +903,16 @@ let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path ((i,j),p) = - let sigma, env = Pfedit.get_current_context () in +let print_path env sigma ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j -(* XXX: This is suspicious!!! *) let _ = Classops.install_path_printer print_path -let print_graph () = - prlist_with_sep fnl print_path (inheritance_graph()) +let print_graph env sigma = + prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) @@ -929,7 +927,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between env sigma cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -940,7 +938,7 @@ let print_path_between cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path env sigma ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl |