refactor: doc comment and remove redundant instance

leanprover · Jan 19, 2024 · 7946ee3 · 7946ee3
1 parent 2f6d2be
commit 7946ee3
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean
@@ -44,6 +44,11 @@ node is always contained within a `commandCtx` node.
 -/
 inductive PartialContextInfo where
   | commandCtx (info : CommandContextInfo)
+  /--
+  Context for the name of the declaration that surrounds nodes contained within this `context` node.
+  For example, this makes the name of the surrounding declaration available in `InfoTree` nodes
+  corresponding to the terms within the declaration.
+  -/
   | parentDeclCtx (parentDecl : Name)
   -- TODO: More constructors for the different kinds of scopes `commandCtx` is currently
   -- used for (e.g. eliminating `Info.updateContext?` would be nice!).

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
@@ -51,9 +51,6 @@ instance : Monad TacticM :=
   let i := inferInstanceAs (Monad TacticM);
   { pure := i.pure, bind := i.bind }
 
-instance : MonadParentDecl TacticM where
-  getParentDeclName? := Term.getDeclName?
-
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals