aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-08 03:22:22 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-07 02:55:41 +0200
commit1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (patch)
tree24b4e369c4acbe2bb9c9ca79b84fc7ddff34e2d8 /toplevel/coqloop.ml
parentfee2365f13900b4d4f4b88c986cbbf94403eeefa (diff)
[camlpX] Remove camlp4 compat layer.
We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
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 8e6f9ffb5..2282932d4 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -255,7 +255,7 @@ let set_prompt prompt =
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
- let rec dot st = match Compat.get_tok (Stream.next st) with
+ let rec dot st = match Stream.next st with
| Tok.KEYWORD ("."|"...") -> ()
| Tok.EOI -> raise End_of_input
| _ -> dot st
@@ -270,7 +270,7 @@ let rec discard_to_dot () =
try
Gram.entry_parse parse_to_dot top_buffer.tokens
with
- | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
+ | Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
| End_of_input -> raise End_of_input
| e when CErrors.noncritical e -> ()