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