From 83996ca3846db000f65cfb7aa09205538cbfbbcb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 21 Nov 2016 15:17:09 +0100
Subject: [PATCH] Add some missing Proper instances on big ops.

---
 algebra/cmra_big_op.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 92312ba12..f20066f74 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -349,13 +349,13 @@ Section gset.
     ([⋅ set] x ∈ X, f x) ≡ ([⋅ set] x ∈ X, g x).
   Proof. apply big_opS_forall; apply _. Qed.
 
-  Lemma big_opS_ne X n :
+  Global Instance big_opS_ne X n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X).
   Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
-  Lemma big_opS_proper' X :
+  Global Instance big_opS_proper' X :
     Proper (pointwise_relation _ (≡) ==> (≡)) (big_opS (M:=M) X).
   Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
-  Lemma big_opS_mono' X :
+  Global Instance big_opS_mono' X :
     Proper (pointwise_relation _ (≼) ==> (≼)) (big_opS (M:=M) X).
   Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
 
@@ -433,13 +433,13 @@ Section gmultiset.
     ([⋅ mset] x ∈ X, f x) ≡ ([⋅ mset] x ∈ X, g x).
   Proof. apply big_opMS_forall; apply _. Qed.
 
-  Lemma big_opMS_ne X n :
+  Global Instance big_opMS_ne X n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (big_opMS (M:=M) X).
   Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
-  Lemma big_opMS_proper' X :
+  Global Instance big_opMS_proper' X :
     Proper (pointwise_relation _ (≡) ==> (≡)) (big_opMS (M:=M) X).
   Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
-  Lemma big_opMS_mono' X :
+  Global Instance big_opMS_mono' X :
     Proper (pointwise_relation _ (≼) ==> (≼)) (big_opMS (M:=M) X).
   Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
 
-- 
GitLab