diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index eb483c50c..93afb3d5a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -215,7 +215,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 casted_open_constr + bindings red_expr int_or_var open_constr simple_intropattern; int_or_var: @@ -236,9 +236,6 @@ GEXTEND Gram open_constr: [ [ c = constr -> ((),c) ] ] ; - casted_open_constr: - [ [ c = constr -> ((),c) ] ] - ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n | c = constr_with_bindings -> induction_arg_of_constr c |