diff options
| author | Pierre-Marie Pédrot | 2019-06-06 16:52:23 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2019-07-29 14:18:01 +0000 |
| commit | 55400b02a70c540d6c6e8152affe1eae99760b91 (patch) | |
| tree | 72055f03180e1bbaad97e29c6287c51828c289bc /plugins/ltac | |
| parent | 807b1e18575914f9956569ab71bb5fe29716cbdf (diff) | |
Tentatively providing a localization function to ad-hoc camlp5 parsers.
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 ()) |