From b3e74c0d82d499df67f140f7f3abe53bd0cc564a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Jun 2019 15:49:28 +0200
Subject: [PATCH] Comment about traces.

---
 theories/program_logic/adequacy.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 448ec6427..093d14d77 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -154,7 +154,8 @@ Proof.
 Qed.
 
 (** Since the full adequacy statement is quite a mouthful, we prove some more
-intuitive and simpler corollaries. *)
+intuitive and simpler corollaries. These lemmas are morover stated in terms of
+[rtc erased_step] so one does not have to provide the trace. *)
 Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
     (φ : val Λ → state Λ → Prop) := {
   adequate_result t2 σ2 v2 :
-- 
GitLab