From 9306e49e47e0b81de59d8444e3b7724ba06144ad Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 23 Sep 2020 10:33:49 +0200
Subject: [PATCH] Addressed discrepancies with displayed Coq code

---
 papers/CPP21.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/papers/CPP21.md b/papers/CPP21.md
index dcc1f4c..ff9780f 100644
--- a/papers/CPP21.md
+++ b/papers/CPP21.md
@@ -23,6 +23,11 @@ contains an overview of the files in that directory.
 - The mechanisation employs a typing judgement for values (`ltyped_val`),
   for technical reasons. More details on this is found in
   [theories/logrel/term_typing_judgment.v](../theories/logrel/term_typing_judgment.v)
+- Minor simplifications have been made for the displayed Coq code of Section 5,
+  such as assuming that an implicit variable (e.g. `{!heapG Σ}) is available from
+  a context, rather than as an implicit variable of the definitions.
+  The definitions between the paper and Coq code are identical,
+  as this is just refactoring.
 
 # Examples
 
-- 
GitLab