aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 5c1b27c33..aade101a4 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -312,7 +312,7 @@ let do_vernac ~time doc sid =
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."); doc, sid)
+ else (Feedback.msg_warning (str "There is no ML toplevel."); doc, sid)
(* Exception printing should be done by the feedback listener,
however this is not yet ready so we rely on the exception for
now. *)
@@ -353,7 +353,7 @@ let rec loop ~time doc =
| CErrors.Drop -> doc
| CErrors.Quit -> exit 0
| any ->
- Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++
+ top_stderr (str "Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++
fnl() ++
str"Please report" ++