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

5 files changed, 24 insertions, 24 deletions

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 "@" -> '@'
   | _ -> ' '