From 39f0153e5d1989b6cae3943560d34866180474d3 Mon Sep 17 00:00:00 2001
From: Dmitry Khalanskiy <Dmitry.Khalanskiy@jetbrains.com>
Date: Wed, 29 Jan 2020 17:06:43 +0300
Subject: [PATCH] Make types of `big_op{L,M}_gen_proper_2` more generic

This version allows to relate structures over different types.
---
 theories/algebra/big_op.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index dd1da98a5..4ea5f8f7b 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -101,7 +101,8 @@ Section list.
   Lemma big_opL_unit l : ([^o list] k↦y ∈ l, monoid_unit) ≡ (monoid_unit : M).
   Proof. induction l; rewrite /= ?left_id //. Qed.
 
-  Lemma big_opL_gen_proper_2 (R : relation M) f g l1 l2 :
+  Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat → B → M)
+        l1 (l2 : list B) :
     R monoid_unit monoid_unit →
     Proper (R ==> R ==> R) o →
     (∀ k,
@@ -230,8 +231,8 @@ Section gmap.
   Implicit Types m : gmap K A.
   Implicit Types f g : K → A → M.
 
-
-  Lemma big_opM_gen_proper_2 (R : relation M) f g m1 m2 :
+  Lemma big_opM_gen_proper_2 {B} (R : relation M) f (g : K → B → M)
+        m1 (m2 : gmap K B) :
     subrelation (≡) R → Equivalence R →
     Proper (R ==> R ==> R) o →
     (∀ k,
-- 
GitLab