From 2c1ff4857c06e2599d68e51f73480b05580e010d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Nov 2020 19:53:17 +0100
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 theories/base_logic/lib/own.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 40cd577e6..3417797d8 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -346,7 +346,7 @@ Section big_op_instances.
   Lemma big_opL_own_1 {B} γ (f : nat → B → A) (l : list B) :
     own γ ([^op list] k↦x ∈ l, f k x) ⊢ [∗ list] k↦x ∈ l, own γ (f k x).
   Proof. apply (big_opL_commute _). Qed.
-  Lemma big_opM_own_1 {B} `{Countable K} γ (g : K → B → A) (m : gmap K B) :
+  Lemma big_opM_own_1 `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) :
     own γ ([^op map] k↦x ∈ m, g k x) ⊢ [∗ map] k↦x ∈ m, own γ (g k x).
   Proof. apply (big_opM_commute _). Qed.
   Lemma big_opS_own_1 `{Countable B} γ (g : B → A) (X : gset B) :
-- 
GitLab