Skip to content
Snippets Groups Projects
Commit 29502179 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Update CPP21.md

parent 9306e49e
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment