Commit 97b094da authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Renamed encoding proofs file

parent 9e81320c
......@@ -6,7 +6,7 @@ From iris.base_logic Require Import invariants.
From osiris.encodings Require Import stype_enc.
From osiris.examples Require Import examples.
Section ExampleProofsEncodings.
Section ExampleProofsEnc.
Context `{!heapG Σ} {N : namespace}.
Context `{!logrelG val Σ}.
......@@ -115,4 +115,4 @@ Section ExampleProofsEncodings.
by iApply "HΦ".
Qed.
End ExampleProofsEncodings.
\ No newline at end of file
End ExampleProofsEnc.
\ No newline at end of file
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