From 11bb8eb2f2748735fd975819e14b43e0c0bf514f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jul 2022 12:47:56 -0400
Subject: [PATCH] make a proof script slightly more robust

---
 iris/algebra/functions.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 529e24031..e16afa57a 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -150,7 +150,7 @@ Section cmra.
     exists (discrete_fun_singleton x y2); split; [by apply HQ|].
     intros x'; destruct (decide (x' = x)) as [->|].
     - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
-    - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //. apply Hg.
+    - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //; by apply Hg.
   Qed.
   Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) :
     ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
-- 
GitLab