Fix typo

This PR ensures that the infotree recognizes `Classical.propDecidable` as an instance, when below a `classical` tactic.

The `classical` tactic modifies the environment that the subsequent sequence of tactics runs in (by making `Classical.propDecidable` an instance). However, it does not add a corresponding `InfoTree.context` node, so its effects are not visible when we want to replay a tactic sequence (for example when running a tactic in the tactic analysis framework). We should add a call to `Lean.Elab.withSafeInfoContext` to remedy this issue.

There are two potential places to add this class: in the meta-level `Lean.Elab.Tactic.classical` wrapper, or the tactic-level `evalClassical` tactic elaborator. I chose the latter since meta-level does not have access to info tree operations (unless we add many parameters to `Lean.Elab.Tactic.classical`: `[MonadNameGenerator m] [MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m]`).

I am not sure how best to test this: is there an easy way to access the current `ContextInfo` when running in a `by` tactic block? A testcase that uses the tactic analysis framework is available here: https://github.com/leanprover-community/mathlib4/pull/29501

src/Lean/Elab/Tactic/Classical.lean

@@ -30,6 +30,7 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t :
 
 @[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental]
 def evalClassical : Tactic := fun stx =>
-  classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
+  classical <| withSaveInfoContext <|
+    Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
 
 end Lean.Elab.Tactic