Pantograph/Goal.lean

@@ -34,7 +34,6 @@ structure GoalState where
   -- Existence of this field shows that we are currently in `conv` mode.
   convMVar?: Option (MVarId × MVarId) := .none
   -- Previous RHS for calc, so we don't have to repeat it every time
-  -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
   calcPrevRhs?: Option Expr := .none
 
 protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
@@ -140,7 +139,6 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
       savedState := nextSavedState
       newMVars := newMVarSet prevMCtx nextMCtx,
       parentMVar? := .some goal,
-      calcPrevRhs? := .none,
     }
 
 /-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
@@ -406,7 +404,6 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
       state.savedState with
       tactic := { goals := [goal] },
     },
-    calcPrevRhs? := .none,
   }
 
 /--
@@ -426,7 +423,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
         term := state.savedState.term,
         tactic := { goals := unassigned },
       },
-      calcPrevRhs? := .none,
     }
 /--
 Brings into scope all goals from `branch`

Pantograph/Library.lean

@@ -178,10 +178,6 @@ def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
 def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
   runTermElabM <| state.convExit
 
-@[export pantograph_goal_calc_m]
-def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult :=
-  runTermElabM <| state.tryCalc goalId pred
-
 @[export pantograph_goal_focus]
 def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
   state.focus goalId