Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involving &

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: ggonthier
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: vbgl

19 files changed, 104 insertions, 59 deletions

diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst
new file mode 100644
index 0000000000..fba09f5e87
--- /dev/null
+++ b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst
@@ -0,0 +1,5 @@
+- White spaces are forbidden in the “&ident” syntax for ltac2 references
+  that are described in :ref:`ltac2_built-in-quotations`
+  (`#10324 <https://github.com/coq/coq/pull/10324>`_,
+  fixes `#10088 <https://github.com/coq/coq/issues/10088>`_,
+  authored by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index c545287fdd..045d028d02 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -427,6 +427,8 @@ In general, quotations can be introduced in terms using the following syntax, wh
 .. prodn::
    ltac2_term += @ident : ( @quotentry )
 
+.. _ltac2_built-in-quotations:
+
 Built-in quotations
 +++++++++++++++++++
 
@@ -439,10 +441,11 @@ The current implementation recognizes the following built-in quotations:
   holes at runtime (type ``Init.constr`` as well).
 - ``pattern``, which parses Coq patterns and produces a pattern used for term
   matching (type ``Init.pattern``).
-- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names
+- ``reference``, which parses either a :n:`@qualid` or :n:`&@ident`. Qualified names
   are globalized at internalization into the corresponding global reference,
   while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a
-  ``Std.reference``.
+  ``Std.reference``. There shall be no white space between the ampersand
+  symbol (``&``) and the identifier (:n:`@ident`).
 
 The following syntactic sugar is provided for two common cases.
 
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index f96cfebed5..f86cb0f6f2 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -23,7 +23,7 @@ module type S =
         val create : string -> 'a e
         val parse : 'a e -> parsable -> 'a
         val name : 'a e -> string
-        val of_parser : string -> (te Stream.t -> 'a) -> 'a e
+        val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a e
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
       end
@@ -112,7 +112,7 @@ type 'a ty_entry = {
 
 and 'a ty_desc =
 | Dlevels of 'a ty_level list
-| Dparser of 'a parser_t
+| Dparser of (Plexing.location_function -> 'a parser_t)
 
 and 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level
 
@@ -1449,7 +1449,7 @@ let start_parser_of_entry entry =
   match entry.edesc with
     Dlevels [] -> empty_entry entry.ename
   | Dlevels elev -> start_parser_of_levels entry 0 elev
-  | Dparser p -> fun levn strm -> p strm
+  | Dparser p -> fun levn strm -> p !floc strm
 
 (* Extend syntax *)
 
@@ -1549,9 +1549,9 @@ let clear_entry e =
         let parse_token_stream (e : 'a e) ts : 'a =
           e.estart 0 ts
         let name e = e.ename
-        let of_parser n (p : te Stream.t -> 'a) : 'a e =
+        let of_parser n (p : Plexing.location_function -> te Stream.t -> 'a) : 'a e =
           { ename = n;
-           estart = (fun _ -> p);
+           estart = (fun _ -> p !floc);
            econtinue =
              (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
            edesc = Dparser p}
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index ec4ec62409..658baf1de9 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -32,7 +32,7 @@ module type S =
         val create : string -> 'a e
         val parse : 'a e -> parsable -> 'a
         val name : 'a e -> string
-        val of_parser : string -> (te Stream.t -> 'a) -> 'a e
+        val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a e
         val parse_token_stream : 'a e -> te Stream.t -> 'a
         val print : Format.formatter -> 'a e -> unit
       end
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index a27d6450b7..de23f05a9e 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -785,12 +785,14 @@ let next_token ~diff_mode loc s =
 (* Location table system for creating tables associating a token count
    to its location in a char stream (the source) *)
 
-let locerr () = invalid_arg "Lexer: location function"
+let locerr i =
+  let m = "Lexer: location function called on token "^string_of_int i in
+  invalid_arg m
 
 let loct_create () = Hashtbl.create 207
 
 let loct_func loct i =
-  try Hashtbl.find loct i with Not_found -> locerr ()
+  try Hashtbl.find loct i with Not_found -> locerr i
 
 let loct_add loct i loc = Hashtbl.add loct i loc
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 8fdec7d1a8..78a12a2e7d 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -84,7 +84,7 @@ let err () = raise Stream.Failure
 (* admissible notation "(x t)" *)
 let lpar_id_coloneq =
   Pcoq.Entry.of_parser "test_lpar_id_coloneq"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
@@ -99,7 +99,7 @@ let lpar_id_coloneq =
 
 let impl_ident_head =
   Pcoq.Entry.of_parser "impl_ident_head"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
 	| KEYWORD "{" ->
 	    (match stream_nth 1 strm with
@@ -112,7 +112,7 @@ let impl_ident_head =
 
 let name_colon =
   Pcoq.Entry.of_parser "name_colon"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
 	| IDENT s ->
             (match stream_nth 1 strm with
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index c1f52c5b39..020501aedf 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -31,10 +31,35 @@ let my_int_of_string loc s =
   with Failure _ ->
     CErrors.user_err ~loc (Pp.str "This number is too large.")
 
-let check_nospace loc expected =
-  let (bp, ep) = Loc.unloc loc in
-  if ep = bp + String.length expected then () else
-  Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected"))
+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 ["|"; "}"]
+
 
 }
 
@@ -130,6 +155,6 @@ GRAMMAR EXTEND Gram
     [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
   bar_cbrace:
-    [ [ "|"; "}" -> { check_nospace loc "|}" } ] ]
+    [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;
 END
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cde867d2ef..7efeab6ba0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -29,7 +29,7 @@ module Entry : sig
   val create : string -> 'a t
   val parse : 'a t -> Parsable.t -> 'a
   val print : Format.formatter -> 'a t -> unit
-  val of_parser : string -> (Tok.t Stream.t -> 'a) -> 'a t
+  val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t
   val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a
   val name : 'a t -> string
 end
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 2654729652..e6e6e29d4f 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -332,7 +332,7 @@ END
 let local_test_lpar_id_colon =
   let err () = raise Stream.Failure in
   Pcoq.Entry.of_parser "lpar_id_colon"
-    (fun strm ->
+    (fun _ strm ->
       match Util.stream_nth 0 strm with
         | Tok.KEYWORD "(" ->
             (match Util.stream_nth 1 strm with
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5c84b35f1b..cab8ed0a55 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -64,7 +64,7 @@ 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 ->
+    (fun _ strm ->
       match stream_nth 0 strm with
         | KEYWORD "[" ->
             (match stream_nth 1 strm with
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 945a2dd613..7cd43cb5cd 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -40,7 +40,7 @@ let err () = raise Stream.Failure
 (* admissible notation "(x t)" *)
 let test_lpar_id_coloneq =
   Pcoq.Entry.of_parser "lpar_id_coloneq"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
@@ -54,7 +54,7 @@ let test_lpar_id_coloneq =
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
   Pcoq.Entry.of_parser "lpar_id_coloneq"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
@@ -68,7 +68,7 @@ let test_lpar_id_rpar =
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
   Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
@@ -85,7 +85,7 @@ open Extraargs
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
   Pcoq.Entry.of_parser "lpar_id_colon"
-    (fun strm ->
+    (fun _ strm ->
       let rec skip_to_rpar p n =
 	match List.last (Stream.npeek n strm) with
         | KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
@@ -109,7 +109,7 @@ let check_for_coloneq =
 
 let lookup_at_as_comma =
   Pcoq.Entry.of_parser "lookup_at_as_comma"
-    (fun strm ->
+    (fun _ strm ->
       match stream_nth 0 strm with
 	| KEYWORD (","|"at"|"as") -> ()
 	| _ -> err ())
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 962730d8dc..175a863ad8 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -235,7 +235,7 @@ let pr_ssrsimpl _ _ _ = pr_simpl
 
 let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
 
-let test_ssrslashnum b1 b2 strm =
+let test_ssrslashnum b1 b2 _ strm =
   match Util.stream_nth 0 strm with
   | Tok.KEYWORD "/" ->
       (match Util.stream_nth 1 strm with
@@ -276,8 +276,8 @@ let test_ssrslashnum11 = test_ssrslashnum true true
 let test_ssrslashnum01 = test_ssrslashnum false true
 let test_ssrslashnum00 = test_ssrslashnum false false
 
-let negate_parser f x =
-  let rc = try Some (f x) with Stream.Failure -> None in
+let negate_parser f tok x =
+  let rc = try Some (f tok x) with Stream.Failure -> None in
   match rc with
   | None -> ()
   | Some _ -> raise Stream.Failure 
@@ -474,7 +474,7 @@ END
 
 (* Old kinds of terms *)
 
-let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> xInParens
   | Tok.KEYWORD "@" -> xWithAt
   | _ -> xNoFlag
@@ -483,7 +483,7 @@ let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 (* New kinds of terms *)
 
-let input_term_annotation strm =
+let input_term_annotation _ strm =
   match Stream.npeek 2 strm with
   | Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
   | Tok.KEYWORD "(" :: _ -> `Parens
@@ -747,7 +747,7 @@ let pushIPatNoop = function
   | pats :: orpat -> (IPatNoop :: pats) :: orpat
   | [] -> []
 
-let test_ident_no_do strm =
+let test_ident_no_do _ strm =
   match Util.stream_nth 0 strm with
   | Tok.IDENT s when s <> "do" -> ()
   | _ -> raise Stream.Failure
@@ -825,7 +825,7 @@ END
 
 {
 
-let reject_ssrhid strm =
+let reject_ssrhid _ strm =
   match Util.stream_nth 0 strm with
   | Tok.KEYWORD "[" ->
       (match Util.stream_nth 1 strm with
@@ -835,13 +835,13 @@ let reject_ssrhid strm =
 
 let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
 
-let rec reject_binder crossed_paren k s =
+let rec reject_binder crossed_paren k tok s =
   match
     try Some (Util.stream_nth k s)
     with Stream.Failure -> None
   with
-  | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s
-  | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s
+  | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) tok s
+  | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) tok s
   | Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren ->
       raise Stream.Failure
   | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
@@ -1006,7 +1006,7 @@ END
 
 {
 
-let accept_ssrfwdid strm =
+let accept_ssrfwdid _ strm =
   match stream_nth 0 strm with
   | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
   | _ -> raise Stream.Failure
@@ -1590,7 +1590,7 @@ END
 let sq_brace_tacnames =
    ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
    (* "by" is a keyword *)
-let accept_ssrseqvar strm =
+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
@@ -1684,7 +1684,7 @@ let ssr_id_of_string loc s =
   ^ "Scripts with explicit references to anonymous variables are fragile."))
     end; Id.of_string s
 
-let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
 
 }
 
@@ -1987,7 +1987,7 @@ END
 
 {
 
-let accept_ssreqid strm =
+let accept_ssreqid _ strm =
   match Util.stream_nth 0 strm with
   | Tok.IDENT _ -> accept_before_syms [":"] strm
   | Tok.KEYWORD ":" -> ()
@@ -2406,7 +2406,7 @@ let lbrace = Char.chr 123
 (** Workaround to a limitation of coqpp *)
 
 let test_ssr_rw_syntax =
-  let test strm  =
+  let test _ strm  =
     if not !ssr_rw_syntax then raise Stream.Failure else
     if is_ssr_loaded () then () else
     match Util.stream_nth 0 strm with
@@ -2617,7 +2617,7 @@ END
 
 {
 
-let accept_idcomma strm =
+let accept_idcomma _ strm =
   match stream_nth 0 strm with
   | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
   | _ -> raise Stream.Failure
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index d920ea9a46..42b800b596 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -66,7 +66,7 @@ END
 
 {
 
-let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
diff --git a/test-suite/bugs/closed/bug_10088.v b/test-suite/bugs/closed/bug_10088.v
new file mode 100644
index 0000000000..3e17bfc12a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10088.v
@@ -0,0 +1,6 @@
+Require Import ssreflect.
+From Ltac2 Require Import Ltac2.
+
+Inductive nat_list :=
+  Nil
+| Cons of nat & nat_list.
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
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 23b5f4daef..adc1606016 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -23,31 +23,31 @@ open Ltac_plugin
 
 let err () = raise Stream.Failure
 
-type lookahead = int -> Tok.t Stream.t -> int option
+type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
 
 let entry_of_lookahead s (lk : lookahead) =
-  let run strm = match lk 0 strm with None -> err () | Some _ -> () in
+  let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
   Pcoq.Entry.of_parser s run
 
-let (>>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
+let (>>) (lk1 : lookahead) lk2 tok n strm = match lk1 tok n strm with
 | None -> None
-| Some n -> lk2 n strm
+| Some n -> lk2 tok n strm
 
-let (<+>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with
-| None -> lk2 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 n strm = Some n
+let lk_empty tok n strm = Some n
 
-let lk_kw kw n strm = match stream_nth n strm with
+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 n strm = match stream_nth n strm with
+let lk_ident tok n strm = match stream_nth n strm with
 | IDENT _ -> Some (n + 1)
 | _ -> None
 
-let lk_int n strm = match stream_nth n strm with
+let lk_int tok n strm = match stream_nth n strm with
 | NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
 | _ -> None
 
@@ -80,9 +80,13 @@ let test_lpar_id_rpar =
     lk_kw "(" >> lk_ident >> lk_kw ")"
   end
 
+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 test_ampersand_ident =
   entry_of_lookahead "test_ampersand_ident" begin
-    lk_kw "&" >> lk_ident
+    lk_kw "&" >> lk_ident >> check_no_space
   end
 
 let test_dollar_ident =
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index ad5d98669d..dcd1979a85 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -519,7 +519,7 @@ END
 
 let only_starredidentrefs =
   Pcoq.Entry.of_parser "test_only_starredidentrefs"
-    (fun strm ->
+    (fun _ strm ->
       let rec aux n =
       match Util.stream_nth n strm with
         | KEYWORD "." -> ()
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index da28e260b3..826e88cabf 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -67,7 +67,7 @@ module Vernac_ =
 
     let command_entry =
       Pcoq.Entry.of_parser "command_entry"
-        (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
+        (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
 
   end