From eb3117bda42a6a0b6048b38abb53dcc2bcd82026 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 20 May 2019 18:41:23 +0200
Subject: [PATCH] Fix compilation with Coq master.

---
 tests/algebra.v                 | 2 +-
 theories/base_logic/lib/iprop.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/algebra.v b/tests/algebra.v
index 5dd2e68aa..f26776d28 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import invariants.
 
-Instance test_cofe: Cofe (iPreProp Σ) := _.
+Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _.
 
 Section tests.
   Context `{!invG Σ}.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 58a3f135c..c587e07ff 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -122,7 +122,7 @@ Module Type iProp_solution_sig.
   Notation iPropI Σ := (uPredI (iResUR Σ)).
   Notation iPropSI Σ := (uPredSI (iResUR Σ)).
 
-  Global Declare Instance iPreProp_cofe: Cofe (iPreProp Σ).
+  Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ).
   Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
   Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
   Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
@@ -141,7 +141,7 @@ Module Export iProp_solution : iProp_solution_sig.
     ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
   Notation iProp Σ := (uPredC (iResUR Σ)).
 
-  Global Instance iPreProp_cofe: Cofe (iPreProp Σ) := _.
+  Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _.
   Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
     solution_fold (iProp_result Σ).
   Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
-- 
GitLab