aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/extraargs.mlg
diff options
context:
space:
mode:
authorMaxime Dénès2019-08-08 19:41:14 +0200
committerMaxime Dénès2019-08-08 19:41:14 +0200
commit9fdeb13166af29bfc6ec1e1930f1932ddc9f1cd4 (patch)
treeebe5ff5638efedfad980f0e81c6bb278e3547eb2 /plugins/ltac/extraargs.mlg
parent0d61500c7137f93942a63a356226276c26edfd99 (diff)
parent97d739835e98dcca038970a50e169a4e1127bd80 (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/extraargs.mlg')
-rw-r--r--plugins/ltac/extraargs.mlg2
1 files changed, 1 insertions, 1 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