deprecations

leanprover · Nov 4, 2024 · 91b2138 · 91b2138
1 parent 3ab759d
commit 91b2138
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
@@ -127,8 +127,8 @@ elab_rules : command
     let freshMsgs ← allNewMessages.toList.mapM fun m => do pure (m.severity, ← contents m)
     let .original leading startPos _ _ := allCommands[0]!.getHeadInfo
       | throwErrorAt allCommands[0]! "Failed to get source position"
-    let .original _ _ trailing stopPos := allCommands.back.getTailInfo
-      | throwErrorAt allCommands.back "Failed to get source position"
+    let .original _ _ trailing stopPos := allCommands.back!.getTailInfo
+      | throwErrorAt allCommands.back! "Failed to get source position"
     let text ← getFileMap
     let str := text.source.extract leading.startPos trailing.stopPos
     let mod ← getMainModule