diff options
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 7d82fa715..1cc0c0297 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -60,6 +60,10 @@ end open Prelude +let arg_of_expr = function + TacArg a -> a + | e -> Tacexp e + (* Tactics grammar rules *) GEXTEND Gram @@ -220,8 +224,8 @@ GEXTEND Gram | ta = tactic_arg0 -> ta ] ] ; tactic_arg0: - [ [ "("; a = tactic_expr; ")" -> Tacexp a - | "()" -> TacVoid + [ [ "("; a = tactic_expr; ")" -> arg_of_expr a + | "()" -> Integer 0 | r = reference -> Reference r | n = integer -> Integer n | id = METAIDENT -> MetaIdArg (loc,id) |