diff --git a/prelude/tactics.v b/prelude/tactics.v
index 775393eae31f3ad3708205157f8f5010d8f06879..20006310255fae0abd6942310730d3d87fa34d52 100644
--- a/prelude/tactics.v
+++ b/prelude/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