diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | printing/prettyp.ml | 9 |
2 files changed, 3 insertions, 10 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e38da45b95..418e13759b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -295,7 +295,7 @@ let tag_var = tag Tag.variable | CPatOr pl -> hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator - | CPatNotation ("( _ )",([p],[]),[]) -> + | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (s,(l,ll),args) -> @@ -665,7 +665,7 @@ let tag_var = tag Tag.variable | CastCoerce -> str ":>"), lcast ) - | CNotation ("( _ )",([t],[],[],[])) -> + | CNotation ((_,"( _ )"),([t],[],[],[])) -> return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) | CNotation (s,env) -> pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 7258bb9b72..1810cc6588 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -657,14 +657,10 @@ let gallina_print_library_entry env sigma with_values ent = gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> - Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { obj_dir; _ }) -> Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> - Some (str " >>>>>>> Closed Module " ++ pr_name oname) let gallina_print_context env sigma with_values = let rec prec n = function @@ -793,9 +789,6 @@ let read_sec_context qid = let rec get_cxt in_cxt = function | (_,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. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in @@ -909,7 +902,7 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) +let print_coercion_value env sigma v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in |