From 6019fde60a9d68d271f767ee504dc130b2a604ed Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 12 May 2020 13:33:21 +0200
Subject: [PATCH] tweak wording

---
 theories/program_logic/ectx_language.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 0e0c1475e..417bc5615 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -35,7 +35,7 @@ Section ectx_language_mixin.
         [K''].  In particular, this implies [e1 = fill K'' e1'] by [fill_inj],
         i.e., [e1] contains the head redex.)
 
-        This implies there can always be only one head redex, see
+        This implies there can be only one head redex, see
         [head_redex_unique]. *)
     mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
       fill K e1 = fill K' e1' →
@@ -158,10 +158,11 @@ Section ectx_language.
   Lemma not_head_reducible e σ : ¬head_reducible e σ ↔ head_irreducible e σ.
   Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
 
-  (** Head redices are unique.  In all sensible instances, [comp_ectx K'
-      empty_ectx] will be the same as [K'], so the conclusion is [K = K' ∧ e =
-      e'], but we do not require a law to actually prove that so we cannot use
-      that fact here. *)
+  (** The decomposition into head redex and context is unique.
+
+      In all sensible instances, [comp_ectx K' empty_ectx] will be the same as
+      [K'], so the conclusion is [K = K' ∧ e = e'], but we do not require a law
+      to actually prove that so we cannot use that fact here. *)
   Lemma head_redex_unique K K' e e' σ :
     fill K e = fill K' e' →
     head_reducible e σ →
-- 
GitLab