We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
native_decide
1 parent 9caad98 commit 1eff493Copy full SHA for 1eff493
src/Lean/Elab/Tactic/ElabTerm.lean
@@ -416,7 +416,7 @@ private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType
416
-- disable async codegen so we can catch its exceptions; we don't want to report `evalConst`
417
-- failures below when the actual reason was a codegen failure
418
withOptions (Elab.async.set · false) do
419
- addAndCompile decl
+ addAndCompile (mayPostPoneCompile := false) decl
420
catch ex =>
421
throwError m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
422
0 commit comments