aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml22
1 files changed, 11 insertions, 11 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 67a5472d5..0d4807e16 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Flags
open Vernac
@@ -251,7 +251,7 @@ let print_toplevel_error (e, info) =
else mt ()
else print_location_in_file loc
in
- locmsg ++ Errors.iprint (e, info)
+ locmsg ++ CErrors.iprint (e, info)
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
@@ -272,14 +272,14 @@ let rec discard_to_dot () =
with
| Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
| End_of_input -> raise End_of_input
- | e when Errors.noncritical e -> ()
+ | e when CErrors.noncritical e -> ()
let read_sentence () =
try
let (loc, _ as r) = Vernac.parse_sentence (top_buffer.tokens, None) in
CWarnings.set_current_loc loc; r
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
discard_to_dot ();
iraise reraise
@@ -300,13 +300,13 @@ let do_vernac () =
try
Vernac.eval_expr (read_sentence ())
with
- | End_of_input | Errors.Quit ->
- top_stderr (fnl ()); raise Errors.Quit
- | Errors.Drop -> (* Last chance *)
- if Mltop.is_ocaml_top() then raise Errors.Drop
+ | End_of_input | CErrors.Quit ->
+ top_stderr (fnl ()); raise CErrors.Quit
+ | CErrors.Drop -> (* Last chance *)
+ if Mltop.is_ocaml_top() then raise CErrors.Drop
else Feedback.msg_error (str"There is no ML toplevel.")
| any ->
- let any = Errors.push any in
+ let any = CErrors.push any in
Format.set_formatter_out_channel stdout;
let msg = print_toplevel_error any ++ fnl () in
pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
@@ -343,8 +343,8 @@ let rec loop () =
reset_input_buffer stdin top_buffer;
while true do do_vernac(); loop_flush_all () done
with
- | Errors.Drop -> ()
- | Errors.Quit -> exit 0
+ | CErrors.Drop -> ()
+ | CErrors.Quit -> exit 0
| any ->
Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++