From fdce31921b5f7d99bac4ce17386dd72005df1f90 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 28 Jun 2021 17:17:32 +0200
Subject: [PATCH] more implicit

---
 iris/bi/big_op.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 99bb3d465..d8c8f241f 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2091,7 +2091,7 @@ Section gset.
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y.
   Proof. apply big_opS_delete. Qed.
 
-  Lemma big_sepS_insert_2 Φ X x :
+  Lemma big_sepS_insert_2 {Φ X} x :
     TCOr (Affine (Φ x)) (Absorbing (Φ x)) →
     Φ x -∗ ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ {[ x ]} ∪ X, Φ y).
   Proof.
@@ -2104,7 +2104,7 @@ Section gset.
     auto.
   Qed.
 
-  Lemma big_sepS_delete_2 Φ X x :
+  Lemma big_sepS_delete_2 {Φ X} x :
     Affine (Φ x) →
     Φ x -∗ ([∗ set] y ∈ X ∖ {[ x ]}, Φ y) -∗ [∗ set] y ∈ X, Φ y.
   Proof.
-- 
GitLab