Merge PR #11695: Refactor lookaheads

Reviewed-by: herbelin
Reviewed-by: ppedrot

11 files changed, 176 insertions, 258 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index d6c6c365cb..48e6f1f213 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -17,7 +17,6 @@ open Glob_term
 open Constrexpr
 open Constrexpr_ops
 open Util
-open Tok
 open Namegen
 
 open Pcoq
@@ -54,48 +53,25 @@ let err () = raise Stream.Failure
 
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
-let lpar_id_coloneq =
-  Pcoq.Entry.of_parser "test_lpar_id_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT s ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":=" ->
-                        stream_njunk 3 strm;
-                        Names.Id.of_string s
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+let test_lpar_id_coloneq =
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_id_coloneq" begin
+    lk_kw "(" >> lk_ident >> lk_kw ":="
+  end
 
 let ensure_fixannot =
-  Pcoq.Entry.of_parser "check_fixannot"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "{" ->
-            (match stream_nth 1 strm with
-              | IDENT ("wf"|"struct"|"measure") -> ()
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "check_fixannot" begin
+    lk_kw "{" >> lk_kws ["wf"; "struct"; "measure"]
+  end
 
-let name_colon =
-  Pcoq.Entry.of_parser "name_colon"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | IDENT s ->
-            (match stream_nth 1 strm with
-              | KEYWORD ":" ->
-                  stream_njunk 2 strm;
-                  Name (Names.Id.of_string s)
-              | _ -> err ())
-        | KEYWORD "_" ->
-          (match stream_nth 1 strm with
-              | KEYWORD ":" ->
-                  stream_njunk 2 strm;
-                  Anonymous
-              | _ -> err ())
-        | _ -> err ())
+let lk_name = Pcoq.Lookahead.(lk_ident <+> lk_kw "_")
+
+let test_name_colon =
+  let open Pcoq.Lookahead in
+  to_entry "test_name_colon" begin
+    lk_name >> lk_kw ":"
+  end
 
 let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
 
@@ -266,7 +242,7 @@ GRAMMAR EXTEND Gram
       | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ]
   ;
   appl_arg:
-    [ [ id = lpar_id_coloneq; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) }
+    [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) }
       | c=operconstr LEVEL "9" -> { (c,None) } ] ]
   ;
   atomic_constr:
@@ -464,8 +440,8 @@ GRAMMAR EXTEND Gram
     [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
       | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
           { id, expl, c }
-      | iid = name_colon ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
-          { (CAst.make ~loc iid), expl, c }
+      | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+          { iid, expl, c }
       | c = operconstr LEVEL "200" ->
           { (CAst.make ~loc Anonymous), false, c } ] ]
   ;
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 020501aedf..5f61b9a047 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -31,35 +31,11 @@ let my_int_of_string loc s =
   with Failure _ ->
     CErrors.user_err ~loc (Pp.str "This number is too large.")
 
-let rec contiguous tok n m =
-    n == m
-  ||
-    let (_, ep) = Loc.unloc (tok n) in
-    let (bp, _) = Loc.unloc (tok (n + 1)) in
-    Int.equal ep bp && contiguous tok (succ n) m
-
-let rec lookahead_kwds strm n = function
-  | [] -> ()
-  | x :: xs ->
-      let toks = Stream.npeek (n+1) strm in
-      match List.nth toks n with
-      | Tok.KEYWORD y ->
-          if String.equal x y then lookahead_kwds strm (succ n) xs
-          else raise Stream.Failure
-      | _ -> raise Stream.Failure
-      | exception (Failure _) -> raise Stream.Failure
-
-(* [test_nospace m] fails if the next m tokens are not contiguous keywords *)
-let test_nospace m = assert(m <> []); Pcoq.Entry.of_parser "test_nospace"
-   (fun tok strm ->
-      let n = Stream.count strm in
-      lookahead_kwds strm 0 m;
-      if contiguous tok n (n + List.length m - 1) then ()
-      else raise Stream.Failure)
-
-let test_nospace_pipe_closedcurly =
-  test_nospace ["|"; "}"]
-
+let test_pipe_closedcurly =
+  let open Pcoq.Lookahead in
+  to_entry "test_pipe_closedcurly" begin
+    lk_kw "|" >> lk_kw "}" >> check_no_space
+  end
 
 }
 
@@ -155,6 +131,6 @@ GRAMMAR EXTEND Gram
     [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
   bar_cbrace:
-    [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ]
+    [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;
 END
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 92c3b7c6e8..d1a6e0eda2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -118,6 +118,64 @@ struct
 
 end
 
+module Lookahead =
+struct
+
+  let err () = raise Stream.Failure
+
+  type t = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
+
+  let rec contiguous tok n m =
+    n == m ||
+    let (_, ep) = Loc.unloc (tok n) in
+    let (bp, _) = Loc.unloc (tok (n + 1)) in
+    Int.equal ep bp && contiguous tok (succ n) m
+
+  let check_no_space tok m strm =
+    let n = Stream.count strm in
+    if contiguous tok n (n+m-1) then Some m else None
+
+  let to_entry s (lk : t) =
+    let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
+    Entry.of_parser s run
+
+  let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
+  | None -> None
+  | Some n -> lk2 tok n strm
+
+  let (<+>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
+  | None -> lk2 tok n strm
+  | Some n -> Some n
+
+  let lk_empty tok n strm = Some n
+
+  let lk_kw kw tok n strm = match stream_nth n strm with
+  | Tok.KEYWORD kw' | Tok.IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
+  | _ -> None
+
+  let lk_kws kws tok n strm = match stream_nth n strm with
+  | Tok.KEYWORD kw | Tok.IDENT kw -> if List.mem_f String.equal kw kws then Some (n + 1) else None
+  | _ -> None
+
+  let lk_ident tok n strm = match stream_nth n strm with
+  | Tok.IDENT _ -> Some (n + 1)
+  | _ -> None
+
+  let lk_ident_except idents tok n strm = match stream_nth n strm with
+  | Tok.IDENT ident when not (List.mem_f String.equal ident idents) -> Some (n + 1)
+  | _ -> None
+
+  let lk_nat tok n strm = match stream_nth n strm with
+  | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
+  | _ -> None
+
+  let rec lk_list lk_elem n strm =
+    ((lk_elem >> lk_list lk_elem) <+> lk_empty) n strm
+
+  let lk_ident_list = lk_list lk_ident
+
+end
+
 (** Grammar extensions *)
 
 (** NB: [extend_statement =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f2fc007a7b..6543a69b50 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -34,6 +34,21 @@ module Entry : sig
   val name : 'a t -> string
 end
 
+module Lookahead : sig
+  type t
+  val to_entry : string -> t -> unit Entry.t
+  val (>>) : t -> t -> t
+  val (<+>) : t -> t -> t
+  val lk_list : t -> t
+  val check_no_space : t
+  val lk_kw : string -> t
+  val lk_kws : string list -> t
+  val lk_nat : t
+  val lk_ident : t
+  val lk_ident_except : string list -> t
+  val lk_ident_list : t
+end
+
 (** The parser of Coq is built from three kinds of rule declarations:
 
    - dynamic rules declared at the evaluation of Coq files (using
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 ()
 
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7ea843ca69..c163438718 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -20,7 +20,6 @@ open Tacexpr
 open Namegen
 open Genarg
 open Genredexpr
-open Tok (* necessary for camlp5 *)
 open Names
 open Attributes
 
@@ -63,14 +62,10 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
 
 (* Hack to parse "[ id" without dropping [ *)
 let test_bracket_ident =
-  Pcoq.Entry.of_parser "test_bracket_ident"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "[" ->
-            (match stream_nth 1 strm with
-              | IDENT _ -> ()
-              | _ -> raise Stream.Failure)
-        | _ -> raise Stream.Failure)
+  let open Pcoq.Lookahead in
+  to_entry "test_bracket_ident" begin
+    lk_kw "[" >> lk_ident
+  end
 
 (* Tactics grammar rules *)
 
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index f0d6258cd1..3e4c7ba782 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -38,45 +38,24 @@ let err () = raise Stream.Failure
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let test_lpar_id_coloneq =
-  Pcoq.Entry.of_parser "lpar_id_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":=" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lpar_id_coloneq" begin
+    lk_kw "(" >> lk_ident >> lk_kw ":="
+  end
 
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
-  Pcoq.Entry.of_parser "lpar_id_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ")" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lpar_id_coloneq" begin
+    lk_kw "(" >> lk_ident >> lk_kw ")"
+  end
 
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
-  Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD "(" ->
-            (match stream_nth 1 strm with
-              | IDENT _ | NUMERAL _ ->
-                  (match stream_nth 2 strm with
-                    | KEYWORD ":=" -> ()
-                    | _ -> err ())
-              | _ -> err ())
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_idnum_coloneq" begin
+    lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":="
+  end
 
 (* idem for (x:t) *)
 open Extraargs
@@ -107,11 +86,10 @@ let check_for_coloneq =
       | _ -> err ())
 
 let lookup_at_as_comma =
-  Pcoq.Entry.of_parser "lookup_at_as_comma"
-    (fun _ strm ->
-      match stream_nth 0 strm with
-        | KEYWORD (","|"at"|"as") -> ()
-        | _ -> err ())
+  let open Pcoq.Lookahead in
+  to_entry "lookup_at_as_comma" begin
+    lk_kws [",";"at";"as"]
+  end
 
 open Constr
 open Prim
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 3f67d55e73..cd7c7d660e 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -142,25 +142,6 @@ let add_genarg tag pr =
   Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
   wit
 
-(** Primitive parsing to avoid syntax conflicts with basic tactics. *)
-
-let accept_before_syms syms strm =
-  match Util.stream_nth 1 strm with
-  | Tok.KEYWORD sym when List.mem sym syms -> ()
-  | _ -> raise Stream.Failure
-
-let accept_before_syms_or_any_id syms strm =
-  match Util.stream_nth 1 strm with
-  | Tok.KEYWORD sym when List.mem sym syms -> ()
-  | Tok.IDENT _ -> ()
-  | _ -> raise Stream.Failure
-
-let accept_before_syms_or_ids syms ids strm =
-  match Util.stream_nth 1 strm with
-  | Tok.KEYWORD sym when List.mem sym syms -> ()
-  | Tok.IDENT id when List.mem id ids -> ()
-  | _ -> raise Stream.Failure
-
 open Ssrast
 let pr_id = Ppconstr.pr_id
 let pr_name = function Name id -> pr_id id | Anonymous -> str "_"
@@ -746,13 +727,11 @@ let pushIPatNoop = function
   | pats :: orpat -> (IPatNoop :: pats) :: orpat
   | [] -> []
 
-let test_ident_no_do _ strm =
-  match Util.stream_nth 0 strm with
-  | Tok.IDENT s when s <> "do" -> ()
-  | _ -> raise Stream.Failure
-
 let test_ident_no_do =
-  Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do
+  let open Pcoq.Lookahead in
+  to_entry "test_ident_no_do" begin
+    lk_ident_except ["do"]
+  end
 
 }
 
@@ -1005,12 +984,11 @@ END
 
 {
 
-let accept_ssrfwdid _ strm =
-  match stream_nth 0 strm with
-  | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
-  | _ -> raise Stream.Failure
-
-let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
+let test_ssrfwdid =
+  let open Pcoq.Lookahead in
+  to_entry "test_ssrfwdid" begin
+    lk_ident >> (lk_ident <+> lk_kws [":"; ":="; "("])
+  end
 
 }
 
@@ -1589,13 +1567,12 @@ END
 let sq_brace_tacnames =
    ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
    (* "by" is a keyword *)
-let accept_ssrseqvar _ strm =
-  match stream_nth 0 strm with
-  | Tok.IDENT id when not (List.mem id sq_brace_tacnames) ->
-     accept_before_syms_or_ids ["["] ["first";"last"] strm
-  | _ -> raise Stream.Failure
 
-let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
+let test_ssrseqvar =
+  let open Pcoq.Lookahead in
+  to_entry "test_ssrseqvar" begin
+    lk_ident_except sq_brace_tacnames >> (lk_kws ["[";"first";"last"])
+  end
 
 let swaptacarg (loc, b) = (b, []), Some (TacId [])
 
@@ -1985,15 +1962,11 @@ END
 
 {
 
-let accept_ssreqid _ strm =
-  match Util.stream_nth 0 strm with
-  | Tok.IDENT _ -> accept_before_syms [":"] strm
-  | Tok.KEYWORD ":" -> ()
-  | Tok.KEYWORD pat when List.mem pat ["_"; "?"; "->"; "<-"] ->
-                      accept_before_syms [":"] strm
-  | _ -> raise Stream.Failure
-
-let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid
+let test_ssreqid =
+  let open Pcoq.Lookahead in
+  to_entry "test_ssreqid" begin
+    ((lk_ident <+> lk_kws ["_"; "?"; "->"; "<-"]) >> lk_kw ":") <+> lk_kw ":"
+  end
 
 }
 
@@ -2614,12 +2587,11 @@ END
 
 {
 
-let accept_idcomma _ strm =
-  match stream_nth 0 strm with
-  | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
-  | _ -> raise Stream.Failure
-
-let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma
+let test_idcomma =
+  let open Pcoq.Lookahead in
+  to_entry "test_idcomma" begin
+    (lk_ident <+> lk_kw "_") >> lk_kw ","
+  end
 
 }
 
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
 
 }
 
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index e95ac3b02b..a0984aa2a9 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -13,7 +13,6 @@
 open Pp
 open Util
 open Names
-open Tok
 open Pcoq
 open Attributes
 open Constrexpr
@@ -21,81 +20,52 @@ open Tac2expr
 open Tac2qexpr
 open Ltac_plugin
 
-let err () = raise Stream.Failure
-
-type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
-
-let check_no_space tok m strm =
-  let n = Stream.count strm in
-  if G_prim.contiguous tok n (n+m-1) then Some m else None
-
-let entry_of_lookahead s (lk : lookahead) =
-  let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
-  Pcoq.Entry.of_parser s run
-
-let (>>) (lk1 : lookahead) lk2 tok n strm = match lk1 tok n strm with
-| None -> None
-| Some n -> lk2 tok n strm
-
-let (<+>) (lk1 : lookahead) lk2 tok n strm = match lk1 tok n strm with
-| None -> lk2 tok n strm
-| Some n -> Some n
-
-let lk_empty tok n strm = Some n
-
-let lk_kw kw tok n strm = match stream_nth n strm with
-| KEYWORD kw' | IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None
-| _ -> None
-
-let lk_ident tok n strm = match stream_nth n strm with
-| IDENT _ -> Some (n + 1)
-| _ -> None
-
-let lk_int tok n strm = match stream_nth n strm with
-| NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
-| _ -> None
-
-let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space)
-
-let rec lk_ident_list n strm =
-  ((lk_ident >> lk_ident_list) <+> lk_empty) n strm
+let lk_ident_or_anti =
+  Pcoq.Lookahead.(lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space))
 
 (* lookahead for (x:=t), (?x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
-  entry_of_lookahead "test_lpar_idnum_coloneq" begin
-    lk_kw "(" >> (lk_ident_or_anti <+> lk_int) >> lk_kw ":="
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_idnum_coloneq" begin
+    lk_kw "(" >> (lk_ident_or_anti <+> lk_nat) >> lk_kw ":="
   end
 
 (* lookahead for (x:t), (?x:t) *)
 let test_lpar_id_colon =
-  entry_of_lookahead "test_lpar_id_colon" begin
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_id_colon" begin
     lk_kw "(" >> lk_ident_or_anti >> lk_kw ":"
   end
 
 (* Hack to recognize "(x := t)" and "($x := t)" *)
 let test_lpar_id_coloneq =
-  entry_of_lookahead "test_lpar_id_coloneq" begin
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_id_coloneq" begin
     lk_kw "(" >> lk_ident_or_anti >> lk_kw ":="
   end
 
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
-  entry_of_lookahead "test_lpar_id_rpar" begin
+  let open Pcoq.Lookahead in
+  to_entry "test_lpar_id_rpar" begin
     lk_kw "(" >> lk_ident >> lk_kw ")"
   end
 
 let test_ampersand_ident =
-  entry_of_lookahead "test_ampersand_ident" begin
+  let open Pcoq.Lookahead in
+  to_entry "test_ampersand_ident" begin
     lk_kw "&" >> lk_ident >> check_no_space
   end
 
 let test_dollar_ident =
-  entry_of_lookahead "test_dollar_ident" begin
+  let open Pcoq.Lookahead in
+  to_entry "test_dollar_ident" begin
     lk_kw "$" >> lk_ident >> check_no_space
   end
 
 let test_ltac1_env =
-  entry_of_lookahead "test_ltac1_env" begin
+  let open Pcoq.Lookahead in
+  to_entry "test_ltac1_env" begin
     lk_ident_list >> lk_kw "|-"
   end
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index def4ed942a..8486de3aed 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -22,7 +22,6 @@ open Extend
 open Decls
 open Declaremods
 open Namegen
-open Tok (* necessary for camlp5 *)
 
 open Pcoq
 open Pcoq.Prim
@@ -531,16 +530,12 @@ END
 
 {
 
-let only_starredidentrefs =
-  Pcoq.Entry.of_parser "test_only_starredidentrefs"
-    (fun _ strm ->
-      let rec aux n =
-      match Util.stream_nth n strm with
-        | KEYWORD "." -> ()
-        | KEYWORD ")" -> ()
-        | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
-        | _ -> raise Stream.Failure in
-      aux 0)
+let test_only_starredidentrefs =
+  let open Pcoq.Lookahead in
+  to_entry "test_only_starredidentrefs" begin
+    lk_list (lk_ident <+> lk_kws ["Type"; "*"]) >> (lk_kws [".";")"])
+  end
+
 let starredidentreflist_to_expr l =
   match l with
   | [] -> SsEmpty
@@ -670,7 +665,7 @@ GRAMMAR EXTEND Gram
   ;
   (* Proof using *)
   section_subset_expr:
-    [ [ only_starredidentrefs; l = LIST0 starredidentref ->
+    [ [ test_only_starredidentrefs; l = LIST0 starredidentref ->
           { starredidentreflist_to_expr l }
       | e = ssexpr -> { e } ]]
   ;
@@ -688,9 +683,9 @@ GRAMMAR EXTEND Gram
       | e1 = ssexpr; "+"; e2 = ssexpr-> { SsUnion(e1,e2) } ]
     | "0"
       [ i = starredidentref -> { i }
-      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"->
+      | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"->
           { starredidentreflist_to_expr l }
-      | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
+      | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
           { SsFwdClose(starredidentreflist_to_expr l) }
       | "("; e = ssexpr; ")"-> { e }
       | "("; e = ssexpr; ")"; "*" -> { SsFwdClose e } ] ]