aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-06-06 16:52:23 +0200
committerVincent Laporte2019-07-29 14:18:01 +0000
commit55400b02a70c540d6c6e8152affe1eae99760b91 (patch)
tree72055f03180e1bbaad97e29c6287c51828c289bc /toplevel
parent807b1e18575914f9956569ab71bb5fe29716cbdf (diff)
Tentatively providing a localization function to ad-hoc camlp5 parsers.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqloop.ml4
-rw-r--r--toplevel/g_toplevel.mlg2
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 2673995a86..f37feb24de 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -242,10 +242,10 @@ let set_prompt prompt =
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
- let rec dot st = match Stream.next st with
+ let rec dot tok st = match Stream.next st with
| Tok.KEYWORD ("."|"...") -> ()
| Tok.EOI -> ()
- | _ -> dot st
+ | _ -> dot tok st
in
Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 1a1537113e..e180d9e750 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -36,7 +36,7 @@ let err () = raise Stream.Failure
let test_show_goal =
Pcoq.Entry.of_parser "test_show_goal"
- (fun strm ->
+ (fun _ strm ->
match stream_nth 0 strm with
| IDENT "Show" ->
(match stream_nth 1 strm with