From b357a22ca82fadfc0fd2f202556d263be7634333 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@gmail.com>
Date: Wed, 27 Jul 2022 08:09:52 -0500
Subject: [PATCH] Fix a proof broken on Coq master
---
iris_staging/heap_lang/interpreter.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/iris_staging/heap_lang/interpreter.v b/iris_staging/heap_lang/interpreter.v
index 322b43439..27d398447 100644
--- a/iris_staging/heap_lang/interpreter.v
+++ b/iris_staging/heap_lang/interpreter.v
@@ -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.
--
GitLab