Skip to content

Commit fa661f3

Browse files
committed
chore: remove leftover
1 parent cb405b5 commit fa661f3

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

src/Lean/Meta/Basic.lean

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -984,8 +984,7 @@ def _root_.Lean.MVarId.setUserName (mvarId : MVarId) (newUserName : Name) : Meta
984984
/--
985985
Throw an exception saying `fvarId` is not declared in the current local context.
986986
-/
987-
def _root_.Lean.FVarId.throwUnknown (fvarId : FVarId) : CoreM α := do
988-
unreachable!
987+
def _root_.Lean.FVarId.throwUnknown (fvarId : FVarId) : CoreM α :=
989988
throwError "unknown free variable `{mkFVar fvarId}`"
990989

991990
/--

0 commit comments

Comments
 (0)