Commit 4800d9e2 authored by Robbert Krebbers's avatar Robbert Krebbers

Make iris_invG Opaque so that simpl does not unfold it.

parent 5a0f9ffa
...@@ -15,6 +15,7 @@ Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := { ...@@ -15,6 +15,7 @@ Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG; iris_invG := heapG_invG;
state_interp := gen_heap_ctx state_interp := gen_heap_ctx
}. }.
Global Opaque iris_invG.
(** Override the notations so that scopes and coercions work out *) (** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V) Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
......
...@@ -15,6 +15,7 @@ Instance ownPG_irisG `{ownPG' Λstate Σ} : irisG' Λstate Σ := { ...@@ -15,6 +15,7 @@ Instance ownPG_irisG `{ownPG' Λstate Σ} : irisG' Λstate Σ := {
iris_invG := ownP_invG; iris_invG := ownP_invG;
state_interp σ := own ownP_name ( (Excl' (σ:leibnizC Λstate))) state_interp σ := own ownP_name ( (Excl' (σ:leibnizC Λstate)))
}. }.
Global Opaque iris_invG.
Definition ownPΣ (Λstate : Type) : gFunctors := Definition ownPΣ (Λstate : Type) : gFunctors :=
#[invΣ; #[invΣ;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment