diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6074acea4..023835af7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -80,7 +80,7 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; @@ -457,7 +457,7 @@ let print_pure_constr csr = print_string (Printexc.to_string e);print_flush (); raise e -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" @@ -514,7 +514,7 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (Errors.print e) + e -> Feedback.msg_notice (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; @@ -530,7 +530,7 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (Errors.print e) + e -> Feedback.msg_notice (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; |