From 295021795f7d0bd4c8675238d3240e9b507e1681 Mon Sep 17 00:00:00 2001 From: Robbert <gitlab-sws@robbertkrebbers.nl> Date: Wed, 23 Sep 2020 10:38:35 +0200 Subject: [PATCH] Update CPP21.md --- papers/CPP21.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/papers/CPP21.md b/papers/CPP21.md index ff9780f..683bdc5 100644 --- a/papers/CPP21.md +++ b/papers/CPP21.md @@ -24,8 +24,8 @@ contains an overview of the files in that directory. 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. + such as assuming that implicit variables (e.g., `{!heapG Σ}`) are 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. -- GitLab