From 2f48cfbc19fbb564db02baf6a775ab16a390afb6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 8 Apr 2024 12:45:03 -0700
Subject: [PATCH] doc: Remove outdated comments

---
 Pantograph/Goal.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index ed181a3..07a432b 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -263,11 +263,8 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
   let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
     state.restoreTacticM goal
 
-    -- TODO: Fail if this is already in conv
-
     -- See Lean.Elab.Tactic.Conv.convTarget
     let convMVar ← Elab.Tactic.withMainContext do
-      -- TODO: Memorize this `rhs` as a conv resultant goal
       let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
       Elab.Tactic.setGoals [newGoal.mvarId!]
       pure rhs.mvarId!