diff --git a/heap_lang/rules.v b/heap_lang/rules.v
index 4aac38ac289fa824e069092a4077cfffa4300b1e..e851f42d6a5f5c8fae0e656c8df7b123fa55a363 100644
--- a/heap_lang/rules.v
+++ b/heap_lang/rules.v
@@ -15,6 +15,7 @@ Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
   state_interp := gen_heap_ctx
 }.
+Global Opaque iris_invG.
 
 (** Override the notations so that scopes and coercions work out *)
 Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
diff --git a/program_logic/ownp.v b/program_logic/ownp.v
index 14add9b238178c661544a0f6ddf07b07be6cba47..4a22198ddaff984f338481b98e23c9c640246ebc 100644
--- a/program_logic/ownp.v
+++ b/program_logic/ownp.v
@@ -15,6 +15,7 @@ Instance ownPG_irisG `{ownPG' Λstate Σ} : irisG' Λstate Σ := {
   iris_invG := ownP_invG;
   state_interp σ := own ownP_name (● (Excl' (σ:leibnizC Λstate)))
 }.
+Global Opaque iris_invG.
 
 Definition ownPΣ (Λstate : Type) : gFunctors :=
   #[invΣ;