From 9e6ebe600adf95985f053a7dc7ba6b086571f5a6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 May 2019 18:56:33 +0200
Subject: [PATCH] Remove some useless Absorbing/Affine constraints for
 `big_andL`.

---
 theories/bi/big_op.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 629d448a9..ab0d787dd 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -489,7 +489,7 @@ Section and_list.
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_and PROP) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-  Lemma big_andL_lookup Φ l i x `{!Absorbing (Φ i x)} :
+  Lemma big_andL_lookup Φ l i x :
     l !! i = Some x → ([∧ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
   Proof.
     intros. rewrite -(take_drop_middle l i x) // big_andL_app /=.
@@ -497,7 +497,7 @@ Section and_list.
       eauto using lookup_lt_Some, Nat.lt_le_incl, and_elim_l', and_elim_r'.
   Qed.
 
-  Lemma big_andL_elem_of (Φ : A → PROP) l x `{!Absorbing (Φ x)} :
+  Lemma big_andL_elem_of (Φ : A → PROP) l x :
     x ∈ l → ([∧ list] y ∈ l, Φ y) ⊢ Φ x.
   Proof.
     intros [i ?]%elem_of_list_lookup; eauto using (big_andL_lookup (λ _, Φ)).
@@ -521,7 +521,7 @@ Section and_list.
     <pers> ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, <pers> (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
-  Lemma big_andL_forall `{BiAffine PROP} Φ l :
+  Lemma big_andL_forall Φ l :
     ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
   Proof.
     apply (anti_symm _).
-- 
GitLab