Commit 3793539d authored by Michael Sammler's avatar Michael Sammler
Browse files

use done instead of fast_done for sideconditions

parent 3ed83dc1
Pipeline #50414 passed with stage
in 16 minutes and 6 seconds
......@@ -664,7 +664,10 @@ Ltac liSideCond :=
| _ => fail "could not simplify goal with evar"
end
]
| _ => split; [ first [ fast_done | shelve ] | ]
(* We use done instead of fast_done here because solving more
sideconditions here is a bigger performance win than the overhead
of done. *)
| _ => split; [ first [ done | shelve ] | ]
end ] end
| _ => fail "do_side_cond: unknown goal"
end.
......
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