diff options
| author | Pierre-Marie Pédrot | 2016-03-03 23:52:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-04 11:13:29 +0100 |
| commit | 143bb68613bcb314e2feffd643f539fba9cd3912 (patch) | |
| tree | 380802541066fa50298a57a7fde44fd18198eb45 /parsing/g_constr.ml4 | |
| parent | ebaa67508ec9f59f95e5b68bfece6228e2024ce5 (diff) | |
Uniformizing the parsing of argument scopes in Ltac.
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0fe0ac42b1..6eeae925a3 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -215,7 +215,7 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> + | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] |