diff --git a/theories/tactics.v b/theories/tactics.v
index 8391f697b471647c55d9d64386792250cc824041..5bea786c6c63aa9c3501ee17e5b8b71dd94d4de1 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -214,8 +214,8 @@ Tactic Notation "csimpl" "in" "*" :=
and injects equalities, and tries to contradict impossible inequalities. *)
Tactic Notation "simplify_eq" := repeat
match goal with
- | H : _ ≠ _ |- _ => by destruct H
- | H : _ = _ → False |- _ => by destruct H
+ | H : _ ≠ _ |- _ => by case H; clear H
+ | H : _ = _ → False |- _ => by case H; clear H
| H : ?x = _ |- _ => subst x
| H : _ = ?x |- _ => subst x
| H : _ = _ |- _ => discriminate H