diff options
Diffstat (limited to 'plugins/ltac/extratactics.mlg')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4a2c298caa..90c366ed63 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -774,7 +774,7 @@ let rec find_a_destructable_match sigma t = let cl = [cl, (None, None), None], None in let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in match EConstr.kind sigma t with - | Case (_,_,_,x,_) when closed0 sigma x -> + | Case (_,_,_,_,_,x,_) when closed0 sigma x -> if isVar sigma x then (* TODO check there is no rel n. *) raise (Found (Tacinterp.eval_tactic dest)) |