diff options
Diffstat (limited to 'tactics/eqdecide.ml')
| -rw-r--r-- | tactics/eqdecide.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index be4b13597..7c821ddcb 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -123,7 +123,7 @@ let diseqCase hyps eqonleft = (tclTHEN (intro_using diseq) (tclTHEN (choose_noteq eqonleft) (tclTHEN (rewrite_and_clear (List.rev hyps)) - (tclTHEN (Proofview.V82.tactic red_in_concl) + (tclTHEN (red_in_concl) (tclTHEN (intro_using absurd) (tclTHEN (Simple.apply (mkVar diseq)) (tclTHEN (Extratactics.injHyp absurd) |