diff --git a/prelude/tactics.v b/prelude/tactics.v
index 7ca9b524a148ede613bda213d22c21c3d99afe1f..775393eae31f3ad3708205157f8f5010d8f06879 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -66,7 +66,7 @@ Ltac done :=
     | discriminate
     | contradiction
     | split
-    | match goal with H : ¬_ |- _ => case H; clear H; done end
+    | match goal with H : ¬_ |- _ => case H; clear H; fast_done end
     ]
   ].
 Tactic Notation "by" tactic(tac) :=