diff options
| author | Maxime Dénès | 2019-08-08 19:41:14 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-08-08 19:41:14 +0200 |
| commit | 9fdeb13166af29bfc6ec1e1930f1932ddc9f1cd4 (patch) | |
| tree | ebe5ff5638efedfad980f0e81c6bb278e3547eb2 /plugins/ltac | |
| parent | 0d61500c7137f93942a63a356226276c26edfd99 (diff) | |
| parent | 97d739835e98dcca038970a50e169a4e1127bd80 (diff) | |
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
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extraargs.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 10 |
3 files changed, 7 insertions, 7 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 ()) |