From bbec6617809dd84c3717be50c5f38147f7c748ff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jun 2016 14:50:13 +0200
Subject: [PATCH] Fix some Params instances.

---
 heap_lang/heap.v     | 4 ++++
 program_logic/auth.v | 6 +++---
 program_logic/sts.v  | 1 +
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 225faa58b..2d57cc202 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -36,7 +36,11 @@ Section definitions.
   Global Instance heap_ctx_persistent N : PersistentP (heap_ctx N).
   Proof. apply _. Qed.
 End definitions.
+
 Typeclasses Opaque heap_ctx heap_mapsto.
+Instance: Params (@heap_inv) 1.
+Instance: Params (@heap_mapsto) 4.
+Instance: Params (@heap_ctx) 2.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 1dad62362..b53bcacbd 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -41,9 +41,9 @@ Section definitions.
 End definitions.
 
 Typeclasses Opaque auth_own auth_ctx.
-Instance: Params (@auth_inv) 6.
-Instance: Params (@auth_own) 6.
-Instance: Params (@auth_ctx) 7.
+Instance: Params (@auth_inv) 5.
+Instance: Params (@auth_own) 5.
+Instance: Params (@auth_ctx) 6.
 
 Section auth.
   Context `{AuthI : authG Λ Σ A}.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index bb5387027..4455a68bd 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -46,6 +46,7 @@ Section definitions.
   Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
   Proof. apply _. Qed.
 End definitions.
+
 Typeclasses Opaque sts_own sts_ownS sts_ctx.
 Instance: Params (@sts_inv) 5.
 Instance: Params (@sts_ownS) 5.
-- 
GitLab