diff --git a/prelude/tactics.v b/prelude/tactics.v
index 843644e83e1f9d389feb8585c3b9593197b03de2..e12aef1be0850345cf6cfc352c9e6968945b483f 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -44,6 +44,7 @@ Ltac done :=
   [ repeat first
     [ solve [trivial]
     | solve [symmetry; trivial]
+    | eassumption
     | reflexivity
     | discriminate
     | contradiction