From c6e8c5d5ee7a12aaf7a7e1c25f342e78614c0a35 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 6 Nov 2018 17:56:53 +0100
Subject: [PATCH] More permissive `gmap_fmap_mono`.

---
 theories/algebra/gmap.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 1ae544dbc..ef26c1a77 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -475,7 +475,7 @@ Proof.
     [done|by rewrite lookup_singleton].
 Qed.
 
-Lemma gmap_fmap_mono {B : ucmraT} (f : A → B) m1 m2 :
+Lemma gmap_fmap_mono {B : cmraT} (f : A → B) m1 m2 :
   Proper ((≡) ==> (≡)) f →
   (∀ x y, x ≼ y → f x ≼ f y) → m1 ≼ m2 → fmap f m1 ≼ fmap f m2.
 Proof.
-- 
GitLab