diff --git a/main.ml b/main.ml
index 1910132..f875cfd 100644
--- a/main.ml
+++ b/main.ml
@@ -58,8 +58,10 @@ let rec interactive ((g, gs) : proof) : proof =
     Goal ty -> fresh_proof ty |> interactive
     | Tact t ->
       begin match t with
-        Exact e ->
-          tact_exact (g, gs) e |> interactive
+        Exact_term e ->
+          tact_exact_term (g, gs) e |> interactive
+        | Exact_proof s ->
+            tact_exact_proof (g, gs) s |> interactive
         | Assumption ->
           tact_assumption (g, gs) |> interactive
         | Intro ->
diff --git a/parser.mly b/parser.mly
index 59d1440..c44037d 100644
--- a/parser.mly
+++ b/parser.mly
@@ -33,7 +33,8 @@ tactic:
 
 command:
   | GOAL t=ty             { Goal t }
-  | EXACT e=expression    { Tact (Exact e) }
+  | EXACT e=expression    { Tact (Exact_term e) }
+  | EXACT s=TYID          { Tact (Exact_proof s) }
   | ASSUMPTION            { Tact (Assumption) }
   | INTRO                 { Tact (Intro) }
   | CUT t=ty              { Tact (Cut t) }