aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index a80599cd5..ab5104c78 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -146,7 +146,6 @@ let print_highlight_location ib loc =
highlight_lines
let valid_buffer_loc ib loc =
- not (Loc.is_ghost loc) &&
let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
(* Toplevel error explanation. *)