From 97b094daa50752ce49cd90b79b13f4b6fa650968 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Thu, 25 Apr 2019 15:09:51 +0200
Subject: [PATCH] Renamed encoding proofs file
---
theories/examples/{encoding_proofs.v => proofs_enc.v} | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
rename theories/examples/{encoding_proofs.v => proofs_enc.v} (98%)
diff --git a/theories/examples/encoding_proofs.v b/theories/examples/proofs_enc.v
similarity index 98%
rename from theories/examples/encoding_proofs.v
rename to theories/examples/proofs_enc.v
index 16850a5..b0eb0d9 100644
--- a/theories/examples/encoding_proofs.v
+++ b/theories/examples/proofs_enc.v
@@ -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
--
GitLab