diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 11:16:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-04 14:52:53 +0100 |
| commit | d5656a6c28f79d59590d4fde60c5158a649d1b65 (patch) | |
| tree | eac22126e5577742b22d731e53e9b49e81d40095 /parsing/g_ltac.ml4 | |
| parent | 143bb68613bcb314e2feffd643f539fba9cd3912 (diff) | |
Making parentheses mandatory in tactic scopes.
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 45d2a09e7..b76f5dda2 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -146,11 +146,11 @@ GEXTEND Gram ; (* Can be used as argument and at toplevel in tactic expressions. *) tactic_top_or_arg: - [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c - | IDENT "constr"; ":"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) - | IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a - | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n) - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> + [ [ IDENT "uconstr"; ":"; "("; c = Constr.lconstr; ")" -> UConstr c + | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> ConstrMayEval (ConstrTerm c) + | IDENT "ltac"; ":"; "("; a = tactic_expr LEVEL "5"; ")" -> arg_of_expr a + | IDENT "ltac"; ":"; "("; n = natural; ")" -> TacGeneric (genarg_of_int n) + | IDENT "ipattern"; ":"; "("; ipat = simple_intropattern; ")" -> TacGeneric (genarg_of_ipattern ipat) | c = constr_eval -> ConstrMayEval c | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l |