diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index 433b9dfed7..3d9b7cd569 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/trace.h"
 #include "library/util.h"
+#include "library/cache_helper.h"
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_exceptional.h"
 #include "library/vm/vm_format.h"
@@ -460,6 +461,13 @@ vm_obj tactic_mk_fresh_name(vm_obj const & s) {
     return mk_tactic_success(to_obj(mk_fresh_name()), to_tactic_state(s));
 }
 
+typedef transparencyless_cache_compatibility_helper<vm_state> vm_state_cache_helper;
+MK_THREAD_LOCAL_GET_DEF(vm_state_cache_helper, get_vmsc);
+
+vm_state & get_tactic_vm_state(environment const & env) {
+    return get_vmsc().get_cache_for(env);
+}
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),           tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}),   tactic_state_format_expr);
diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h
index b8d3fe7e8a..5a0ab7ece4 100644
--- a/src/library/tactic/tactic_state.h
+++ b/src/library/tactic/tactic_state.h
@@ -138,6 +138,8 @@ struct type_context_scope {
 #define LEAN_TACTIC_TRY try {
 #define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return mk_tactic_exception(ex, S); }
 
+vm_state & get_tactic_vm_state(environment const & env);
+
 void initialize_tactic_state();
 void finalize_tactic_state();
 }