diff options
| author | Maxime Dénès | 2017-11-27 16:50:27 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-27 16:50:27 +0100 |
| commit | 2fcbfcfe8066bcf7ee40830bb9043b0cfd754e63 (patch) | |
| tree | 0d3b52ef87e745ca91671ee37d686b0134344a53 | |
| parent | 4bf305af7e4688b96ec6f407b2a6f4e7e9d7a4a5 (diff) | |
| parent | de9b47e22811cd61316484bc8fd4ef89138ccda6 (diff) | |
Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.
| -rw-r--r-- | grammar/vernacextend.mlp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 5bc8f15047..f6f46710c2 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -170,11 +170,11 @@ EXTEND [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun ~atts ~st -> ( let () = $e$ in st ) >> in + let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun ~atts ~st -> ( let () = $e$ in st ) >> in + let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; |