From 19e984a6d4545c1b5a2d3fab4e5ec7ddcdd6022c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 May 2020 16:37:51 +0200
Subject: [PATCH] tweak comments

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

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 824d4cd0a..4968ecc2a 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -148,7 +148,7 @@ Section ectx_language.
       head_step e σ κ e' σ' efs →
       if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
 
-  (* Some lemmas about this language *)
+  (** * Some lemmas about this language *)
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
 
@@ -158,6 +158,10 @@ 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. *)
   Lemma head_redex_unique K K' e e' σ :
     fill K e = fill K' e' →
     head_reducible e σ →
-- 
GitLab