Compare commits
No commits in common. "0a987174bc27686d0744fe601c3678646f4639fd" and "eca7431977602d74832c420d73d661bcf3485ecb" have entirely different histories.
0a987174bc
...
eca7431977
|
@ -81,7 +81,6 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
|
||||||
: EMainM α := do
|
: EMainM α := do
|
||||||
let scope := (← get).scope
|
let scope := (← get).scope
|
||||||
let context := {
|
let context := {
|
||||||
errToSorry := false,
|
|
||||||
isNoncomputableSection := scope.isNoncomputable,
|
isNoncomputableSection := scope.isNoncomputable,
|
||||||
}
|
}
|
||||||
let state := {
|
let state := {
|
||||||
|
|
Loading…
Reference in New Issue