diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 547ccc017c..84eff7e5e6 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -27,6 +27,9 @@ end tactic_state
 meta instance : has_to_format tactic_state :=
 ⟨tactic_state.to_format⟩
 
+meta instance : has_to_string tactic_state :=
+⟨λ s, (to_fmt s)^.to_string s^.get_options⟩
+
 @[reducible] meta def tactic := interaction_monad tactic_state
 @[reducible] meta def tactic_result := interaction_monad.result tactic_state