diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 225faa58bc4998a6a4a077ba933439a95af55468..2d57cc20278bb45046036d9f727d9b830fef4d3b 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 1dad62362a65fd44edf4f8d838980cebf3732b1d..b53bcacbd74ec1d3323b3c016b30c72cc270b0d1 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 bb53870271bdb5b2a577a956f3aadd7ada5059d5..4455a68bdb892531d4eeabb72860c9d9a35ebc62 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.