diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 2f106353d2..f72fdf7893 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -286,7 +286,7 @@ meta constant mk_mapp_core  : transparency → name → list (option expr) → t
    Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t).
    The tactic fails if the given expression is not a local constant. -/
 meta constant subst         : expr → tactic unit
-meta constant exact         : expr → tactic unit
+meta constant exact_core    : transparency → expr → tactic unit
 /- Elaborate the given quoted expression with respect to the current main goal.
    If the boolean argument is tt, then metavariables are tolerated and
    become new goals. -/
@@ -491,6 +491,12 @@ get_local n >>= infer_type
 meta def trace_result : tactic unit :=
 format_result >>= trace
 
+meta def exact : expr → tactic unit :=
+exact_core semireducible
+
+meta def rexact : expr → tactic unit :=
+exact_core reducible
+
 /- (find_same_type t es) tries to find in es an expression with type definitionally equal to t -/
 meta def find_same_type : expr → list expr → tactic expr
 | e []         := failed
diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp
index de58b1a08b..8ea87658cd 100644
--- a/src/library/tactic/exact_tactic.cpp
+++ b/src/library/tactic/exact_tactic.cpp
@@ -9,11 +9,12 @@ Author: Leonardo de Moura
 #include "library/tactic/app_builder_tactics.h"
 
 namespace lean {
-vm_obj exact(expr const & e, tactic_state const & s) {
+
+vm_obj exact_core(transparency_mode const & m, expr const & e, tactic_state const & s) {
     try {
         optional<metavar_decl> g = s.get_main_goal_decl();
         if (!g) return mk_no_goals_exception(s);
-        type_context ctx     = mk_type_context_for(s);
+        type_context ctx     = mk_type_context_for(s, m);
         expr e_type          = ctx.infer(e);
         if (!ctx.is_def_eq(g->get_type(), e_type)) {
             auto thunk = [=]() {
@@ -34,12 +35,12 @@ vm_obj exact(expr const & e, tactic_state const & s) {
     }
 }
 
-vm_obj tactic_exact(vm_obj const & e, vm_obj const & s) {
-    return exact(to_expr(e), to_tactic_state(s));
+vm_obj tactic_exact_core(vm_obj const & m, vm_obj const & e, vm_obj const & s) {
+    return exact_core(to_transparency_mode(m), to_expr(e), to_tactic_state(s));
 }
 
 void initialize_exact_tactic() {
-    DECLARE_VM_BUILTIN(name({"tactic", "exact"}), tactic_exact);
+    DECLARE_VM_BUILTIN(name({"tactic", "exact_core"}), tactic_exact_core);
 }
 
 void finalize_exact_tactic() {