From 3f4603f02ee68149d3ed7746239c24fc53e69280 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 1 Oct 2021 20:26:35 +0200
Subject: [PATCH] Clarify funny proof of `tac_twp_cmpxchg_fail`

To avoid confusion from
https://gitlab.mpi-sws.org/iris/iris/-/commit/d2c226e769c48e2ac67baaa776d3cd6400f4524e#note_73999.
---
 iris_heap_lang/proofmode.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 9d44d43ee..ad370a361 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -473,7 +473,8 @@ Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
 Proof.
   rewrite envs_entails_eq. intros. rewrite -twp_bind.
   eapply wand_apply; first exact: twp_cmpxchg_fail.
-  rewrite envs_lookup_split //=. simpl. by do 2 f_equiv.
+  (* [//] solves some evars and enables further simplification. *)
+  rewrite envs_lookup_split /= // /=. by do 2 f_equiv.
 Qed.
 
 Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
-- 
GitLab