Skip to content
Snippets Groups Projects
Unverified Commit b357a22c authored by Tej Chajed's avatar Tej Chajed
Browse files

Fix a proof broken on Coq master

parent 7211cd79
No related branches found
No related tags found
No related merge requests found
......@@ -418,9 +418,9 @@ Section interpreter.
repeat (case_match; simplify_eq/=; auto).
- pose proof (explain_vals_compare_safe_fail_wf v1 v2).
intuition eauto.
- pose proof (explain_vals_compare_safe_fail_wf v1 v2) as H.
replace (explain_vals_compare_safe_fail v1 v2) in H.
rewrite -> is_Some_alt in H.
- pose proof (explain_vals_compare_safe_fail_wf v1 v2) as Hwf.
replace (explain_vals_compare_safe_fail v1 v2) in Hwf.
rewrite -> is_Some_alt in Hwf.
intuition eauto.
Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment