Commit 8d8ba0ff authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Minor changes

parent 97b094da
......@@ -7,7 +7,7 @@ From osiris.encodings Require Import stype_enc.
From osiris.examples Require Import examples.
Section ExampleProofsEnc.
Context `{!heapG Σ} {N : namespace}.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ (stype'_to_stype sτ) c s)
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