Merge PR #11695: Refactor lookaheads

Reviewed-by: herbelin
Reviewed-by: ppedrot

1 files changed, 4 insertions, 12 deletions

diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 5835d75c79..f97c291c79 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -330,18 +330,10 @@ END
 {
 
 let local_test_lpar_id_colon =
-  let err () = raise Stream.Failure in
-  Pcoq.Entry.of_parser "lpar_id_colon"
-    (fun _ strm ->
-      match Util.stream_nth 0 strm with
-        | Tok.KEYWORD "(" ->
-            (match Util.stream_nth 1 strm with
-              | Tok.IDENT _ ->
-                  (match Util.stream_nth 2 strm with
-                    | Tok.KEYWORD ":" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lpar_id_colon" begin
+    lk_kw "(" >> lk_ident >> lk_kw ":"
+  end
 
 let pr_lpar_id_colon _ _ _ _ = mt ()