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

Update CPP21.md

parent 29502179
No related branches found
No related tags found
No related merge requests found
......@@ -25,7 +25,7 @@ contains an overview of the files in that directory.
[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 implicit variables (e.g., `{!heapG Σ}`) are available from
a `Context`, rather than as an implicit variable of the definitions.
a `Context`, rather than as implicits variables 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