From aba0b1a7c197e09e93095ce65ccb634d39f7cf93 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 31 Aug 2018 16:11:10 +0200
Subject: [PATCH] update a comment

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

diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index ceff03979..4843e6f03 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -31,7 +31,8 @@ Inductive step : relation (state sts * tokens sts) :=
      tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
 Notation steps := (rtc step).
 Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
-  (* Probably equivalent definition: (\mathcal{L}(s') ## T) ∧ s \rightarrow s' *)
+  (* Possible alternative definition: (tok s2) ## T) ∧ s \rightarrow s'.
+     This is not equivalent, but it might be good enough? *)
   | Frame_step T1 T2 :
      T1 ## tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2.
 Notation frame_steps T := (rtc (frame_step T)).
-- 
GitLab