Commit 7b665ce0 authored by Michael Sammler's avatar Michael Sammler
Browse files

don't call splitting_fast_done on goals with protected evars

parent c1b44eaa
Pipeline #57705 passed with stage
in 22 minutes and 55 seconds
......@@ -724,7 +724,10 @@ Ltac liSideCond :=
lazymatch P with
| shelve_hint _ => split; [ unfold shelve_hint; li_shelve_sidecond |]
| _ => first [
split; [splitting_fast_done|] |
lazymatch P with
| context [protected _] => fail
| _ => split; [splitting_fast_done|]
end |
progress normalize_goal_and |
lazymatch P with
| context [protected _] => first [
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment