From 2a444b2326612dc2dc70ac13bf2c32c1b71401de Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jan 2021 11:35:09 +0100
Subject: [PATCH] Apply 2 suggestion(s) to 2 file(s)

---
 iris/algebra/big_op.v | 2 +-
 iris/bi/big_op.v      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 91571f38b..1893566c2 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -482,7 +482,7 @@ Section gset.
 
   Lemma big_opS_list_to_set f (l : list A) :
     NoDup l →
-    ([^o set] x ∈ list_to_set l, f x) ≡ [^o list] _ ↦ x ∈ l, f x.
+    ([^o set] x ∈ list_to_set l, f x) ≡ [^o list] x ∈ l, f x.
   Proof.
     induction l as [|x l]; intros Hnodup.
     - rewrite big_opS_empty //.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 9d8d75198..7663101f0 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1633,7 +1633,7 @@ Section gset.
 
   Lemma big_sepS_list_to_set Φ (l : list A) :
     NoDup l →
-    ([∗ set] x ∈ list_to_set l, Φ x) ⊣⊢ [∗ list] _ ↦ x ∈ l, Φ x.
+    ([∗ set] x ∈ list_to_set l, Φ x) ⊣⊢ [∗ list] x ∈ l, Φ x.
   Proof. apply big_opS_list_to_set. Qed.
 
   Lemma big_sepS_sep Φ Ψ X :
-- 
GitLab