Merge PR #11695: Refactor lookaheads

Reviewed-by: herbelin
Reviewed-by: ppedrot

1 files changed, 4 insertions, 13 deletions

diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 56fda58a25..d3768eb1e3 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -11,8 +11,6 @@
 {
 open Pcoq
 open Pcoq.Prim
-open Tok
-open Util
 open Vernacexpr
 
 (* Vernaculars specific to the toplevel *)
@@ -36,17 +34,10 @@ open Toplevel_
 let err () = raise Stream.Failure
 
 let test_show_goal =
-  Pcoq.Entry.of_parser "test_show_goal"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-      | IDENT "Show" ->
-          (match stream_nth 1 strm with
-          | IDENT "Goal" ->
-            (match stream_nth 2 strm with
-              | NUMERAL _ -> ()
-              | _ -> err ())
-          | _ -> err ())
-      | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "test_show_goal" begin
+   lk_kw "Show" >> lk_kw "Goal" >> lk_nat
+  end
 
 }