Commit 2c759645 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Move `Opaque iris_invG` to the appropriate place.

parent 7a7e1d22
...@@ -16,7 +16,6 @@ Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := { ...@@ -16,7 +16,6 @@ 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)
......
...@@ -9,6 +9,7 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG { ...@@ -9,6 +9,7 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
state_interp : Λstate iProp Σ; state_interp : Λstate iProp Σ;
}. }.
Notation irisG Λ Σ := (irisG' (state Λ) Σ). Notation irisG Λ Σ := (irisG' (state Λ) Σ).
Global Opaque iris_invG.
Inductive stuckness := NotStuck | MaybeStuck. Inductive stuckness := NotStuck | MaybeStuck.
......
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