diff options
Diffstat (limited to 'parsing/g_tacticnew.ml4')
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 40a292ca1..c45dc332f 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -234,7 +234,7 @@ GEXTEND Gram [ [ "using"; el = constr_with_bindings -> el ] ] ; with_names: - [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids + [ [ "as"; "["; ids = LIST1 (LIST0 simple_intropattern) SEP "|"; "]" -> ids | -> [] ] ] ; simple_tactic: |