diff options
Diffstat (limited to 'plugins/ltac/g_tactic.mlg')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 89a14c7c12..43957bbde5 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -190,7 +190,7 @@ open Pvernac.Vernac_ GRAMMAR EXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis - bindings red_expr int_or_var open_constr uconstr + bindings red_expr int_or_var nat_or_var open_constr uconstr simple_intropattern in_clause clause_dft_concl hypident destruction_arg; int_or_var: |