diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index e15855ef26..9b4998c671 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -37,7 +37,7 @@ Feedback Segmenttree Unicodetable Unicode -Errors +CErrors CWarnings Bigint CUnix diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6074acea46..7c010e6a48 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -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"; |