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