diff --git a/theories/tactics.v b/theories/tactics.v
index 67045a6d8b4cb41bd17d58664a6cb723b94b52ef..0e0adb0e0571f433f1c22549ff06e4b8ab6539f8 100644
--- a/theories/tactics.v
+++ b/theories/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.