aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/extraargs.mlg
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/extraargs.mlg')
-rw-r--r--plugins/ltac/extraargs.mlg16
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 ()