From 837655995e4ef895992b4d798a85b8675bc32b9f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Jun 2018 01:00:34 +0200
Subject: [PATCH] Fix inconsistent big operator instance names.

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

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 4825fd551..0ad6b7c5a 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -70,7 +70,7 @@ Section sep_list.
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
            (big_opL (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_sep_mono' :
+  Global Instance big_sepL_id_mono' :
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_sep M) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
@@ -238,7 +238,7 @@ Section and_list.
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
            (big_opL (@bi_and PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
-  Global Instance big_and_mono' :
+  Global Instance big_andL_id_mono' :
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_and M) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-- 
GitLab