From 2c759645e54350fc460a4479ef1c3929b403111b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 May 2018 23:48:07 +0200
Subject: [PATCH] Move `Opaque iris_invG` to the appropriate place.

---
 theories/heap_lang/lifting.v        | 1 -
 theories/program_logic/weakestpre.v | 1 +
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index a16239aaa..7d00192b0 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 13879ab40..139a5d78b 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.
 
-- 
GitLab