summaryrefslogtreecommitdiff
path: root/parsing/g_tactic.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_tactic.ml4')
-rw-r--r--parsing/g_tactic.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b42b2c6d..69593f99 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -202,7 +202,7 @@ let merge_occurrences loc cl = function
GEXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
bindings red_expr int_or_var open_constr uconstr
- simple_intropattern clause_dft_concl;
+ simple_intropattern clause_dft_concl hypident;
int_or_var:
[ [ n = integer -> ArgArg n