From 4800d9e2c483253b5ea0b27aaba78f36c53e5d6d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Dec 2016 20:20:30 +0100
Subject: [PATCH] Make iris_invG Opaque so that simpl does not unfold it.

---
 heap_lang/rules.v    | 1 +
 program_logic/ownp.v | 1 +
 2 files changed, 2 insertions(+)

diff --git a/heap_lang/rules.v b/heap_lang/rules.v
index 4aac38ac2..e851f42d6 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 14add9b23..4a22198dd 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Σ;
-- 
GitLab