aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index cdbe444e5b..e933f08735 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -256,7 +256,7 @@ let rec discard_to_dot () =
try
Pcoq.Entry.parse parse_to_dot top_buffer.tokens
with
- | Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot ()
+ | CLexer.Error.E _ -> discard_to_dot ()
| e when CErrors.noncritical e -> ()
let read_sentence ~state input =