aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b930c4eec..07a398903 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -290,7 +290,10 @@ let rec discard_to_dot () =
let read_sentence () =
try Vernac.parse_sentence (top_buffer.tokens, None)
- with reraise -> discard_to_dot (); raise reraise
+ with reraise ->
+ let reraise = Errors.push reraise in
+ discard_to_dot ();
+ raise reraise
(** [do_vernac] reads and executes a toplevel phrase, and print error
messages when an exception is raised, except for the following: