From a7b8d5f8270cbd047cecae5621ff9fb05ca07646 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 29 Nov 2017 19:40:35 +0100
Subject: [PATCH] Generalize `merge_ext`.

---
 theories/fin_maps.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 37a9b4d7..124966f7 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -181,7 +181,8 @@ Section setoid.
     intros ?? Hf; apply partial_alter_proper.
     by destruct 1; constructor; apply Hf.
   Qed.
-  Lemma merge_ext f g `{!DiagNone f, !DiagNone g} :
+  Lemma merge_ext `{Equiv B, Equiv C} (f g : option A → option B → option C)
+      `{!DiagNone f, !DiagNone g} :
     ((≡) ==> (≡) ==> (≡))%signature f g →
     ((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g).
   Proof.
-- 
GitLab