diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index a16239aaa8362cbc61a549a52a26c32a10559ef5..7d00192b0b79aa01a3cc1fa0fae6c4ba1d8fe9cf 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -16,7 +16,6 @@ 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/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 13879ab407550dfa1fdd07a9cf6f935888ff4f9d..139a5d78ba58eef4e2b060849513d94565111ba9 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -9,6 +9,7 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
   state_interp : Λstate → iProp Σ;
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
+Global Opaque iris_invG.
 
 Inductive stuckness := NotStuck | MaybeStuck.