diff --git a/prelude/tactics.v b/prelude/tactics.v
index 970982061a39cc8707303d2cc27ffd1069ee18bd..a9c3458e680f0e8fdfff53f6410ebb41e433524e 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -56,7 +56,7 @@ Ltac done :=
     | contradiction
     | solve [apply not_symmetry; trivial]
     | split ]
-  | match goal with H : ¬_ |- _ => solve [destruct H; trivial] end ].
+  | match goal with H : ¬_ |- _ => solve [case H; trivial] end ].
 Tactic Notation "by" tactic(tac) :=
   tac; done.