diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 8cf1e531dd..a7d95c5e89 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -65,8 +65,8 @@ TACTIC EXTEND replace_term END let induction_arg_of_quantified_hyp = function - | AnonHyp n -> ElimOnAnonHyp n - | NamedHyp id -> ElimOnIdent (Loc.ghost,id) + | AnonHyp n -> None,ElimOnAnonHyp n + | NamedHyp id -> None,ElimOnIdent (Loc.ghost,id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a @@ -74,7 +74,7 @@ let induction_arg_of_quantified_hyp = function let elimOnConstrWithHoles tac with_evars c = Tacticals.New.tclWITHHOLES with_evars (tac with_evars) - c.sigma (Some (ElimOnConstr c.it)) + c.sigma (Some (None,ElimOnConstr c.it)) TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> |