diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 02d2663361..b1e9f257f2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -100,8 +100,7 @@ GEXTEND Gram ; tactic_mode: [ [ gln = OPT[n=natural; ":" -> n]; - tac = subgoal_command -> tac gln - | tac = subgoal_command -> tac None ] ] + tac = subgoal_command -> tac gln ] ] ; subprf: |