diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 6dc6a28..f9ebb66 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -154,33 +154,31 @@ the draft tactic instead.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
-  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
   assert! !sorrys.isEmpty
-  withEnv env do
-    let goalsM := sorrys.mapM λ i => do
-      match i.info with
-      | .ofTermInfo termInfo  => do
-        let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+  let goalsM := sorrys.mapM λ i => do
+    match i.info with
+    | .ofTermInfo termInfo  => do
+      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+      if (← mvarId.getType).hasSorry then
+        throwError s!"Coupling is not allowed in drafting"
+      return [(mvarId, stxByteRange termInfo.stx)]
+    | .ofTacticInfo tacticInfo => do
+      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      for mvarId in mvarIds do
         if (← mvarId.getType).hasSorry then
           throwError s!"Coupling is not allowed in drafting"
-        return [(mvarId, stxByteRange termInfo.stx)]
-      | .ofTacticInfo tacticInfo => do
-        let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-        for mvarId in mvarIds do
-          if (← mvarId.getType).hasSorry then
-            throwError s!"Coupling is not allowed in drafting"
-        let range := stxByteRange tacticInfo.stx
-        return mvarIds.map (·, range)
-      | _ => panic! "Invalid info"
-    let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
-    let goals := annotatedGoals.map Prod.fst
-    let srcBoundaries := annotatedGoals.map Prod.snd
-    let root := match goals with
-      | [] => panic! "No MVars generated"
-      | [g] => g
-      | _ => { name := .anonymous }
-    let state ← GoalState.createFromMVars goals root
-    return { state, srcBoundaries }
+      let range := stxByteRange tacticInfo.stx
+      return mvarIds.map (·, range)
+    | _ => panic! "Invalid info"
+  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
+  let goals := annotatedGoals.map Prod.fst
+  let srcBoundaries := annotatedGoals.map Prod.snd
+  let root := match goals with
+    | [] => panic! "No MVars generated"
+    | [g] => g
+    | _ => { name := .anonymous }
+  let state ← GoalState.createFromMVars goals root
+  return { state, srcBoundaries }
 
 
 @[export pantograph_frontend_collect_new_defined_constants_m]
diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean
index 8067d17..3d2829b 100644
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@@ -118,6 +118,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
 
 partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
   if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
+    trace[Pantograph.Frontend.MetaTranslate] "Existing mvar id {srcMVarId.name} → {mvarId'.name}"
     return mvarId'
   let mvarId' ← Meta.withLCtx .empty #[] do
     let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
@@ -134,6 +135,7 @@ partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
           let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
           assignDelayedMVar mvarId' fvars' mvarIdPending'
         pure mvarId'
+  trace[Pantograph.Frontend.MetaTranslate] "Translated {srcMVarId.name} → {mvarId'.name}"
   addTranslatedMVar srcMVarId mvarId'
   return mvarId'
 end
@@ -148,6 +150,7 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
     let lctx' ← translateLCtx
     let mvar ← Meta.withLCtx lctx' #[] do
       let type' ← translateExpr type
+      trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
       Meta.mkFreshExprSyntheticOpaqueMVar type'
     return mvar.mvarId!
 
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 7f135f5..21d6dc1 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -113,11 +113,14 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
   }
 
 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume_parent]
+@[export pantograph_goal_state_immediate_resume]
 protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
   -- Prune parents solved goals
   let mctx := state.mctx
-  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
+  let parentGoals := parent.goals.filter λ goal =>
+    let isDuplicate := state.goals.contains goal
+    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
+    (¬ isDuplicate) && (¬ isSolved)
   {
     state with
     savedState := {
@@ -127,25 +130,25 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
   }
 
 /--
-Brings into scope a list of goals
+Brings into scope a list of goals. User must ensure `goals` is distinct.
 -/
 @[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
   if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
     let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
     .error s!"Goals {invalid_goals} are not in scope"
-  else
-    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-    let unassigned := goals.filter (λ goal =>
-      let mctx := state.mctx
-      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
-    .ok {
-      state with
-      savedState := {
-        term := state.savedState.term,
-        tactic := { goals := unassigned },
-      },
-    }
+  -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+  let unassigned := goals.filter λ goal =>
+    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
+    let isDuplicate := state.goals.contains goal
+    (¬ isDuplicate) && (¬ isSolved)
+  return {
+    state with
+    savedState := {
+      term := state.savedState.term,
+      tactic := { goals := unassigned },
+    },
+  }
 /--
 Brings into scope all goals from `branch`
 -/
@@ -238,23 +241,20 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
 /-- Response for executing a tactic -/
 inductive TacticResult where
   -- Goes to next state
-  | success (state: GoalState)
+  | success (state : GoalState) (messages : Array String)
   -- Tactic failed with messages
-  | failure (messages: Array String)
+  | failure (messages : Array String)
   -- Could not parse tactic
-  | parseError (message: String)
+  | parseError (message : String)
   -- The given action cannot be executed in the state
-  | invalidAction (message: String)
+  | invalidAction (message : String)
 
-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
-  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
-    |>.filterMapM λ m => do
-      if m.severity == .error then
-        return .some $ ← m.toString
-      else
-        return .none
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
+  let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
+  let hasErrors := newMessages.any (·.severity == .error)
+  let newMessages ← newMessages.mapM λ m => m.toString
   Core.resetMessageLog
-  return newMessages.toArray
+  return (hasErrors, newMessages.toArray)
 
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM
@@ -266,13 +266,16 @@ protected def GoalState.tryTacticM
     let nextState ← state.step goal tacticM guardMVarErrors
 
     -- Check if error messages have been generated in the core.
-    let newMessages ← dumpMessageLog prevMessageLength
-    if ¬ newMessages.isEmpty then
+    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
+    if hasError then
       return .failure newMessages
-    return .success nextState
+    else
+      return .success nextState newMessages
   catch exception =>
     match exception with
-    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
+    | .internal _ =>
+      let (_, messages) ← dumpMessageLog prevMessageLength
+      return .failure messages
     | _ => return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
@@ -341,7 +344,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
       parentMVar? := .some goal,
       convMVar? := .some (convRhs, goal, otherGoals),
       calcPrevRhs? := .none
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
@@ -378,7 +381,7 @@ protected def GoalState.convExit (state: GoalState):
       parentMVar? := .some convGoal,
       convMVar? := .none
       calcPrevRhs? := .none
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
@@ -456,7 +459,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
       },
       parentMVar? := .some goal,
       calcPrevRhs?
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 9371662..07f68e6 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -268,14 +268,14 @@ structure GoalTactic where
 structure GoalTacticResult where
   -- The next goal state id. Existence of this field shows success
   nextStateId?: Option Nat          := .none
-  -- If the array is empty, it shows the goals have been fully resolved.
-  goals?: Option (Array Goal)          := .none
+  -- If the array is empty, it shows the goals have been fully resolved. If this
+  -- is .none, there has been a tactic error.
+  goals?: Option (Array Goal)       := .none
 
-  -- Existence of this field shows tactic execution failure
-  tacticErrors?: Option (Array String) := .none
+  messages? : Option (Array String) := .some #[]
 
   -- Existence of this field shows the tactic parsing has failed
-  parseError?: Option String := .none
+  parseError? : Option String       := .none
   deriving Lean.ToJson
 structure GoalContinue where
   -- State from which the continuation acquires the context
diff --git a/Repl.lean b/Repl.lean
index a735c88..a9193d3 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -5,6 +5,8 @@ namespace Pantograph.Repl
 
 open Lean
 
+set_option trace.Pantograph.Frontend.MetaTranslate true
+
 structure Context where
   coreContext : Core.Context
 
@@ -61,6 +63,10 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
     catch ex =>
       let desc ← ex.toMessageData.toString
       return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
+    finally
+      for {msg, ..} in (← getTraceState).traces do
+        IO.eprintln (← msg.format.toIO)
+      resetTraceState
   if let .some token := cancelTk? then
     runCancelTokenWithTimeout token (timeout := .ofBitVec options.timeout)
   let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with
@@ -81,6 +87,7 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
     : EMainM α := do
   let scope := (← get).scope
   let context := {
+    errToSorry := false,
     isNoncomputableSection := scope.isNoncomputable,
   }
   let state := {
@@ -148,7 +155,7 @@ def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.Fro
         .some $ step.newConstants.toArray.map λ name => name.toString
       else
         .none
-    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
+    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then
         pure (.none, .none, .none)
       else do
         let ({ state, srcBoundaries }, goals) ← liftMetaM do
@@ -318,12 +325,10 @@ def execute (command: Protocol.Command): MainM Json := do
         pure $ .error error
     match nextGoalState? with
     | .error error => Protocol.throw error
-    | .ok (.success nextGoalState) => do
+    | .ok (.success nextGoalState messages) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
-          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
-            Protocol.throw $ errorIO "Resuming known goals"
-          pure result
+          pure $ nextGoalState.immediateResume goalState
         | true, .some true => pure nextGoalState
         | true, .some false => do
           let .some (_, _, dormantGoals) := goalState.convMVar? |
@@ -337,13 +342,14 @@ def execute (command: Protocol.Command): MainM Json := do
       return {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
+        messages? := .some messages,
       }
     | .ok (.parseError message) =>
-      return { parseError? := .some message }
+      return { messages? := .none, parseError? := .some message }
     | .ok (.invalidAction message) =>
       Protocol.throw $ errorI "invalid" message
     | .ok (.failure messages) =>
-      return { tacticErrors? := .some messages }
+      return { messages? := .some messages }
   goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
     let state ← getMainState
     let .some target := state.goalStates[args.target]? |
diff --git a/Test/Common.lean b/Test/Common.lean
index c8ffa5d..8a0623e 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -71,7 +71,7 @@ def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
 def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
 
 def TacticResult.toString : TacticResult → String
-  | .success state => s!".success ({state.goals.length} goals)"
+  | .success state _messages => s!".success ({state.goals.length} goals)"
   | .failure messages =>
     let messages := "\n".intercalate messages.toList
     s!".failure {messages}"
diff --git a/Test/Integration.lean b/Test/Integration.lean
index d80c072..510753e 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -88,7 +88,7 @@ def test_tactic : Test :=
     step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
     step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
-     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
+     ({ messages? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
       Protocol.GoalTacticResult)
   ]
 example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
@@ -302,6 +302,34 @@ def test_import_open : Test :=
      ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
   ]
 
+/-- Ensure there cannot be circular references -/
+def test_frontend_process_circular : Test :=
+  let withSorry := "theorem mystery : 1 + 2 = 2 + 3 := sorry"
+  [
+    let goal1: Protocol.Goal := {
+      name := "_uniq.2",
+      target := { pp? := .some "1 + 2 = 2 + 3" },
+      vars := #[],
+    }
+    step "frontend.process"
+      ({
+        file? := .some withSorry,
+        sorrys := true,
+      }: Protocol.FrontendProcess)
+     ({
+       units := [{
+         boundary := (0, withSorry.utf8ByteSize),
+         goalStateId? := .some 0,
+         goals? := .some #[goal1],
+         goalSrcBoundaries? := .some #[(35, 40)],
+         messages := #["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],
+       }],
+     }: Protocol.FrontendProcessResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "exact?" }: Protocol.GoalTactic)
+     ({ messages? := .some #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."] }
+     : Protocol.GoalTacticResult),
+  ]
+
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
   let coreContext ← createCoreContext #[]
@@ -322,6 +350,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),
     ("frontend.process import", test_import_open),
+    ("frontend.process circular", test_frontend_process_circular),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 
diff --git a/Test/Main.lean b/Test/Main.lean
index 8d9a87d..2a8e890 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -55,6 +55,7 @@ def main (args: List String) := do
     ("Serial", Serial.suite env_default),
     ("Tactic/Assign", Tactic.Assign.suite env_default),
     ("Tactic/Prograde", Tactic.Prograde.suite env_default),
+    ("Tactic/Special", Tactic.Special.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
   LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 421ea01..8f355b8 100644
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@@ -79,7 +79,7 @@ def test_m_couple: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -88,7 +88,7 @@ def test_m_couple: TestM Unit := do
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   -- Set m to 3
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -111,7 +111,7 @@ def test_m_couple_simp: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -122,7 +122,7 @@ def test_m_couple_simp: TestM Unit := do
     #[#["_uniq.38"], #["_uniq.38"], #[]])
 
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -136,7 +136,7 @@ def test_m_couple_simp: TestM Unit := do
     #[.some "2 ≤ 2", .some "2 ≤ 5"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
   let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -146,7 +146,7 @@ def test_m_couple_simp: TestM Unit := do
       return ()
     | .ok state => pure state
   let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -173,7 +173,7 @@ def test_proposition_generation: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -187,7 +187,7 @@ def test_proposition_generation: TestM Unit := do
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
 
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -197,7 +197,7 @@ def test_proposition_generation: TestM Unit := do
 
   let assign := "Eq.refl x"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -216,7 +216,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -224,7 +224,7 @@ def test_partial_continuation: TestM Unit := do
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
 
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index ceb8690..178d8d2 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -89,7 +89,7 @@ def test_identity: TestM Unit := do
 
   let tactic := "intro p h"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -116,7 +116,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn 0 "intro n m" with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -130,7 +130,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
     addTest $ assertUnreachable $ other.toString
 
   let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -148,14 +148,14 @@ def test_delta_variable: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
     #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -187,14 +187,14 @@ def test_arith: TestM Unit := do
 
   let tactic := "intros"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check tactic (state1.goals.length = 1)
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -202,7 +202,7 @@ def test_arith: TestM Unit := do
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
   let tactic := "assumption"
   let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -237,7 +237,7 @@ def test_or_comm: TestM Unit := do
 
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -265,7 +265,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -291,7 +291,7 @@ def test_or_comm: TestM Unit := do
     s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
 
   let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -301,7 +301,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -310,13 +310,13 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
   let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
   let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -330,13 +330,13 @@ def test_or_comm: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals[0]!])
   let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -375,7 +375,7 @@ def test_conv: TestM Unit := do
 
   let tactic := "intro a b c1 c2 h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -383,7 +383,7 @@ def test_conv: TestM Unit := do
     #[interiorGoal [] "a + b + c1 = b + a + c2"])
 
   let state2 ← match ← state1.conv (state1.get! 0) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -392,7 +392,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rhs"
   let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -401,7 +401,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "lhs"
   let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -410,7 +410,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "congr"
   let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -422,7 +422,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rw [Nat.add_comm]"
   let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -431,7 +431,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rfl"
   let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -446,7 +446,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rfl"
   let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -454,14 +454,14 @@ def test_conv: TestM Unit := do
     #[])
 
   let state1_1 ← match ← state6.convExit with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
 
   let tactic := "exact h"
   let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -488,7 +488,7 @@ def test_calc: TestM Unit := do
       return ()
   let tactic := "intro a b c d h1 h2"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -496,7 +496,7 @@ def test_calc: TestM Unit := do
     #[interiorGoal [] "a + b = c + d"])
   let pred := "a + b = b + c"
   let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -510,7 +510,7 @@ def test_calc: TestM Unit := do
 
   let tactic := "apply h1"
   let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -521,7 +521,7 @@ def test_calc: TestM Unit := do
       return ()
   let pred := "_ = c + d"
   let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -532,7 +532,7 @@ def test_calc: TestM Unit := do
   addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
   let tactic := "apply h2"
   let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -553,7 +553,7 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
 
   let tactic := "intro p"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -572,7 +572,7 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
 
   let tactic := "intro p q r h"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -604,7 +604,7 @@ def test_deconstruct : TestM Unit := do
 
   let tactic := "intro p q ⟨hp, hq⟩"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       fail other.toString
       return ()
diff --git a/Test/Tactic.lean b/Test/Tactic.lean
index 217edb6..ea77e98 100644
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@@ -1,2 +1,3 @@
 import Test.Tactic.Assign
 import Test.Tactic.Prograde
+import Test.Tactic.Special
diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean
index 63bc525..6a806ce 100644
--- a/Test/Tactic/Prograde.lean
+++ b/Test/Tactic/Prograde.lean
@@ -56,7 +56,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -65,7 +65,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl (Or.inl h)"
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -75,7 +75,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   let evalBind := "y"
   let evalExpr := "Or.inl h"
   let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -95,7 +95,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl y"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -112,22 +112,22 @@ def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
 def test_define_root_expr : TestT Elab.TermElabM Unit := do
   --let rootExpr ← parseSentence "Nat"
   --let state0 ← GoalState.create rootExpr
-  --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
+  --let .success state1 _ ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
   --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
   --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
   let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p x"
-  let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state1 _ ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let binderName := `binder
   let value := "x.fst"
   let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
   let tacticM := Tactic.evalDefine binderName expr
-  let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
+  let .success state2 _ ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
   let tactic := s!"apply {binderName}"
-  let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state3 _ ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let tactic := s!"exact 5"
-  let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state4 _ ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
   addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
 
@@ -140,7 +140,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -149,7 +149,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl (Or.inl h)"
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -159,7 +159,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
   let haveBind := "y"
   let haveType := "p ∨ q"
   let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -171,7 +171,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl h"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -185,7 +185,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
       return ()
   let expr := "Or.inl y"
   let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -200,7 +200,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro a p h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -216,7 +216,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
     | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
     | false => state1.tryAssign (state1.get! 0) (expr := expr)
   let state2 ← match result2 with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -241,7 +241,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
 
   let tactic := "exact 1"
   let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -274,7 +274,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
 
   let tactic := "exact Or.inl (Or.inl h)"
   let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
diff --git a/Test/Tactic/Special.lean b/Test/Tactic/Special.lean
new file mode 100644
index 0000000..2342b3f
--- /dev/null
+++ b/Test/Tactic/Special.lean
@@ -0,0 +1,23 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Special
+
+def test_exact_q : TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "1 + 2 = 2 + 3"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "exact?"
+  let state1? ← state0.tacticOn (goalId := 0) (tactic := tactic)
+  let .failure messages := state1? | fail "Must fail"
+  checkEq "messages" messages #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."]
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("exact?", test_exact_q),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Special
diff --git a/doc/repl.md b/doc/repl.md
index b0fe972..7217139 100644
--- a/doc/repl.md
+++ b/doc/repl.md
@@ -39,6 +39,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
     exit, the goal id is ignored.
   - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
+  If the `goals` field does not exist, the tactic execution has failed. Read
+  `messages` to find the reason.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
   Execute continuation/resumption
   - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.