diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e117f1dcb0..8fabb70536 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -27,6 +27,10 @@ open Recordops open Misctypes open Printer open Printmod +open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : mutual_inductive -> std_ppcmds; @@ -132,7 +136,6 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let open Context.Rel.Declaration in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in @@ -170,9 +173,8 @@ type opacity = | TransparentMaybeOpacified of Conv_oracle.level let opacity env = - let open Context.Named.Declaration in function - | VarRef v when is_local_def (Environ.lookup_named v env) -> + | VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -700,7 +702,7 @@ let read_sec_context r = let dir = try Nametab.locate_section qid with Not_found -> - user_err_loc (loc,"read_sec_context", str "Unknown section.") in + 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 @@ -733,11 +735,10 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let open Context.Named.Declaration in - str |> Global.lookup_named |> set_id str |> print_named_decl + str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl with Not_found -> - errorlabstrm - "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") + user_err + ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") let print_name = function | ByNotation (loc,ntn,sc) -> @@ -762,8 +763,7 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let open Context.Named.Declaration in - lookup_named id env |> set_id id |> print_named_decl + env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl let print_about_any loc k = match k with @@ -831,7 +831,7 @@ let index_of_class cl = try fst (class_info cl) with Not_found -> - errorlabstrm "index_of_class" + user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") let print_path_between cls clt = @@ -841,7 +841,7 @@ let print_path_between cls clt = try lookup_path_between_class (i,j) with Not_found -> - errorlabstrm "index_cl_of_id" + user_err ~hdr:"index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in |