diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 73718c629..ae9fc2aed 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -255,9 +255,7 @@ GEXTEND Gram [ [ "using"; el = constr_with_bindings -> el ] ] ; with_names: - [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids - | "as"; "("; ids = LIST1 simple_intropattern SEP ","; ")" -> [ids] - | -> [] ] ] + [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ] ; simple_tactic: [ [ |