diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 151949c3c6..85b9d6a08f 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -752,11 +752,14 @@ let case_eq_intros_rewrite x = end } let rec find_a_destructable_match t = + let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in + let cl = [cl, (None, None), None], None in + let dest = TacAtom (Loc.ghost, TacInductionDestruct(false, false, cl)) in match kind_of_term t with | Case (_,_,x,_) when closed0 x -> if isVar x then (* TODO check there is no rel n. *) - raise (Found (Tacinterp.eval_tactic(<:tactic<destruct x>>))) + raise (Found (Tacinterp.eval_tactic dest)) else (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *) raise (Found (case_eq_intros_rewrite x)) |