From ca5138249890e65cf0e21d09ffb5c5e54d31a34c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Jun 2019 15:21:18 +0200
Subject: [PATCH] Fix `Params` for functors.

---
 theories/algebra/cmra.v | 4 ++--
 theories/algebra/ofe.v  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index f44e3f3c4..455592862 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -781,7 +781,7 @@ Record rFunctor := RFunctor {
     CmraMorphism (rFunctor_map fg)
 }.
 Existing Instances rFunctor_ne rFunctor_mor.
-Instance: Params (@rFunctor_map) 5 := {}.
+Instance: Params (@rFunctor_map) 9 := {}.
 
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
@@ -818,7 +818,7 @@ Record urFunctor := URFunctor {
     CmraMorphism (urFunctor_map fg)
 }.
 Existing Instances urFunctor_ne urFunctor_mor.
-Instance: Params (@urFunctor_map) 5 := {}.
+Instance: Params (@urFunctor_map) 9 := {}.
 
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 52bc4c554..3bded308f 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -676,7 +676,7 @@ Record cFunctor := CFunctor {
     cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
 }.
 Existing Instance cFunctor_ne.
-Instance: Params (@cFunctor_map) 5 := {}.
+Instance: Params (@cFunctor_map) 9 := {}.
 
 Delimit Scope cFunctor_scope with CF.
 Bind Scope cFunctor_scope with cFunctor.
-- 
GitLab