From a26827f58bb1991e1313d19a7ea1fac6dedd07c1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 May 2022 11:57:21 -0700
Subject: [PATCH] chore: remove `Context.main`

---
 src/Lean/Elab/Tactic/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 9add88f68e..5699c7ff14 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -36,7 +36,6 @@ def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit :=
 namespace Tactic
 
 structure Context where
-  main       : MVarId
   /-- Declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree -/
   elaborator : Name
   /--
@@ -94,7 +93,7 @@ def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) :=
        else
          throw ex
    try
-     aux.runCore' { main := mvarId, elaborator := Name.anonymous } { goals := [mvarId] }
+     aux.runCore' { elaborator := Name.anonymous } { goals := [mvarId] }
    finally
      modify fun s => { s with syntheticMVars := savedSyntheticMVars }