diff --git a/papers/CPP21.md b/papers/CPP21.md index 683bdc5f59d67af7f08a61f5b530412da0f0e8e5..a8ba65c63df9b3229f5b2157a9fc5ac45b811f16 100644 --- a/papers/CPP21.md +++ b/papers/CPP21.md @@ -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.