Skip to content
GitLab
Commit 9da8555a authored by Michael Sammler's avatar Michael Sammler
Browse files

bail out early for trivial sideconditions

parent b20b6026
Pipeline #57395 passed with stage
in 17 minutes and 23 seconds
Hide whitespace changes
Inline Side-by-side
theories/lithium/interpreter.v
View file @ 9da8555a
...@@ -724,6 +724,7 @@ Ltac liSideCond := ...@@ -724,6 +724,7 @@ Ltac liSideCond :=
lazymatch P with lazymatch P with
| shelve_hint _ => split; [ unfold shelve_hint; li_shelve_sidecond |] | shelve_hint _ => split; [ unfold shelve_hint; li_shelve_sidecond |]
| _ => first [ | _ => first [
split; [done_no_false|] |
progress normalize_goal_and | progress normalize_goal_and |
lazymatch P with lazymatch P with
| context [protected _] => first [ | 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