diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 2f94fc38f3..22a53d8c3a 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -849,5 +849,9 @@ tactic.by_contradiction >> return ()
 meta def by_contra : tactic unit :=
 tactic.by_contradiction >> return ()
 
+/-- Fail if there are unsolved goals. -/
+meta def done : tactic unit :=
+tactic.done
+
 end interactive
 end tactic