From e824f642d6ee038defb7081e90886b58a9496ea0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 20 Nov 2017 21:20:48 +0100
Subject: [PATCH] Correct some `Params` instances.

---
 theories/algebra/ofe.v               | 1 +
 theories/base_logic/lib/saved_prop.v | 2 +-
 theories/base_logic/lib/wsat.v       | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index b51402803..9cf97615e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1061,6 +1061,7 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.
 Arguments later_car {_} _.
+Instance: Params (@Next) 1.
 
 Section later.
   Context {A : ofeT}.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index b1d1c462a..e91c5670e 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -21,7 +21,7 @@ Definition saved_anything_own `{savedAnythingG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
   own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
-Instance: Params (@saved_anything_own) 3.
+Instance: Params (@saved_anything_own) 4.
 
 Section saved_anything.
   Context `{savedAnythingG Σ F}.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index bfa226e3c..a26f4f6ae 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -23,6 +23,7 @@ Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
 Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
+Instance: Params (@invariant_unfold) 1.
 Instance: Params (@ownI) 3.
 
 Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
-- 
GitLab