diff --git a/library/init/meta/fun_info.lean b/library/init/meta/fun_info.lean
index dd8f1f85ca..e8a3833261 100644
--- a/library/init/meta/fun_info.lean
+++ b/library/init/meta/fun_info.lean
@@ -78,10 +78,10 @@ meta_definition fun_info.has_to_format [instance] : has_to_format fun_info :=
 has_to_format.mk fun_info.to_format
 
 namespace tactic
-meta_constant get_fun_info       : expr → tactic fun_info
+meta_constant get_fun_info_core   : expr → transparency → tactic fun_info
 /- (get_fun_info fn n) return information assuming the function has only n arguments.
    The tactic fail if n > length (params (get_fun_info fn)) -/
-meta_constant get_fun_info_n     : expr → nat → tactic fun_info
+meta_constant get_fun_info_n_core : expr → nat → transparency → tactic fun_info
 /- (get_spec_func_info t) return information for the function application t of the form
    (f a_1 ... a_n).
    This tactic is more precise than (get_fun_info f) and (get_fun_info_n f)
@@ -99,6 +99,18 @@ meta_constant get_fun_info_n     : expr → nat → tactic fun_info
 
     Remark: get_fun_info and get_spec_func_info return the same result for all but
     is_prop and is_subsingleton. -/
-meta_constant get_spec_fun_info   : expr → tactic fun_info
-meta_constant get_spec_prefix_size : expr → nat → tactic nat
+meta_constant get_spec_fun_info_core   : expr → transparency → tactic fun_info
+meta_constant get_spec_prefix_size_core : expr → nat → transparency → tactic nat
+
+meta_definition get_fun_info (e : expr) : tactic fun_info :=
+get_fun_info_core e transparency.semireducible
+
+meta_definition get_fun_info_n (e : expr) (n : nat) : tactic fun_info :=
+get_fun_info_n_core e n transparency.semireducible
+
+meta_definition get_spec_fun_info (e : expr) : tactic fun_info :=
+get_spec_fun_info_core e transparency.semireducible
+
+meta_definition get_spec_prefix_size (e : expr) (n : nat) : tactic nat :=
+get_spec_prefix_size_core e n transparency.semireducible
 end tactic
diff --git a/src/library/tactic/fun_info_tactics.cpp b/src/library/tactic/fun_info_tactics.cpp
index bc0d366829..f77309523e 100644
--- a/src/library/tactic/fun_info_tactics.cpp
+++ b/src/library/tactic/fun_info_tactics.cpp
@@ -42,29 +42,6 @@ vm_obj to_obj(fun_info const & info) {
     return mk_vm_constructor(0, to_obj(info.get_params_info()), to_obj(info.get_result_deps()));
 }
 
-fun_info get_fun_info(type_context & ctx, expr const & fn);
-/** \brief Return information assuming the function has only nargs.
-    \pre nargs <= get_fun_info(ctx, fn).get_arity() */
-fun_info get_fun_info(type_context & ctx, expr const & fn, unsigned nargs);
-/** \brief Return information for the function application.
-    This is more precise than \c get methods for dependent functions.
-
-    Example: given (f : Pi (A : Type), A -> A), \c get_specialized_fun_info for
-
-    f unit b
-
-    returns a \c fun_info with two param_info
-    1) m_specialized = true, m_is_dep = true
-    2) m_subsingleton = true, m_deps = {0}
-
-    The second argument is marked as subsingleton only because the resulting information
-    is taking into account the first argument.
-
-    \remark \c get and \c get_specialization return the same result for all but
-    is_prop and is_subsingleton. */
-fun_info get_specialized_fun_info(type_context & ctx, expr const & app);
-unsigned get_specialization_prefix_size(type_context & ctx, expr const & fn, unsigned nargs);
-
 #define TRY   LEAN_TACTIC_TRY
 #define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s))
 
@@ -72,40 +49,40 @@ static vm_obj mk_result(fun_info const & info, vm_obj const & s) {
     return mk_tactic_success(to_obj(info), to_tactic_state(s));
 }
 
-vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & s) {
+vm_obj tactic_get_fun_info(vm_obj const & fn, vm_obj const & m, vm_obj const & s) {
     TRY;
-    type_context_scope ctx(s);
+    type_context_scope ctx(s, m);
     return mk_result(get_fun_info(ctx, to_expr(fn)), s);
     CATCH;
 }
 
-vm_obj tactic_get_fun_info_n(vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
+vm_obj tactic_get_fun_info_n(vm_obj const & fn, vm_obj const & n, vm_obj const & m, vm_obj const & s) {
     TRY;
-    type_context_scope ctx(s);
+    type_context_scope ctx(s, m);
     return mk_result(get_fun_info(ctx, to_expr(fn), force_to_unsigned(n, 0)), s);
     CATCH;
 }
 
-vm_obj tactic_get_spec_fun_info(vm_obj const & app, vm_obj const & s) {
+vm_obj tactic_get_spec_fun_info(vm_obj const & app, vm_obj const & m, vm_obj const & s) {
     TRY;
-    type_context_scope ctx(s);
+    type_context_scope ctx(s, m);
     return mk_result(get_specialized_fun_info(ctx, to_expr(app)), s);
     CATCH;
 }
 
-vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & s) {
+vm_obj tactic_get_spec_prefix_size(vm_obj const & fn, vm_obj const & n, vm_obj const & m, vm_obj const & s) {
     TRY;
-    type_context_scope ctx(s);
+    type_context_scope ctx(s, m);
     return mk_tactic_success(mk_vm_nat(get_specialization_prefix_size(ctx, to_expr(fn), force_to_unsigned(n, 0))),
                              to_tactic_state(s));
     CATCH;
 }
 
 void initialize_fun_info_tactics() {
-    DECLARE_VM_BUILTIN(name({"tactic", "get_fun_info"}),           tactic_get_fun_info);
-    DECLARE_VM_BUILTIN(name({"tactic", "get_fun_info_n"}),         tactic_get_fun_info_n);
-    DECLARE_VM_BUILTIN(name({"tactic", "get_spec_fun_info"}),      tactic_get_spec_fun_info);
-    DECLARE_VM_BUILTIN(name({"tactic", "get_spec_prefix_size"}),   tactic_get_spec_prefix_size);
+    DECLARE_VM_BUILTIN(name({"tactic", "get_fun_info_core"}),           tactic_get_fun_info);
+    DECLARE_VM_BUILTIN(name({"tactic", "get_fun_info_n_core"}),         tactic_get_fun_info_n);
+    DECLARE_VM_BUILTIN(name({"tactic", "get_spec_fun_info_core"}),      tactic_get_spec_fun_info);
+    DECLARE_VM_BUILTIN(name({"tactic", "get_spec_prefix_size_core"}),   tactic_get_spec_prefix_size);
 }
 
 void finalize_fun_info_tactics() {
diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h
index e2473b1428..b8d3fe7e8a 100644
--- a/src/library/tactic/tactic_state.h
+++ b/src/library/tactic/tactic_state.h
@@ -130,6 +130,8 @@ struct type_context_scope {
         m_mctx(s.mctx()), m_ctx(mk_type_context_for(s, m_mctx, m)) {}
     type_context_scope(vm_obj const & s, transparency_mode m = transparency_mode::Semireducible):
         type_context_scope(to_tactic_state(s), m) {}
+    type_context_scope(vm_obj const & s, vm_obj const & m):
+        type_context_scope(to_tactic_state(s), to_transparency_mode(m)) {}
     operator type_context &() { return m_ctx; }
 };