From 4f6f564f3b171a935a81df0340bfe9dc5376b1fa Mon Sep 17 00:00:00 2001
From: euisuny <ey222@cornell.edu>
Date: Fri, 30 Jul 2021 17:16:09 +0200
Subject: [PATCH] A little bit of cleaning
---
theories/simulation/behavior.v | 4 ----
1 file changed, 4 deletions(-)
diff --git a/theories/simulation/behavior.v b/theories/simulation/behavior.v
index 5aa1cc4c..bcfb37bd 100644
--- a/theories/simulation/behavior.v
+++ b/theories/simulation/behavior.v
@@ -136,10 +136,6 @@ Section beh.
stuck_pool p T σ →
t ≈ ub -> has_beh p T σ t
| HasBehDiv T σ t :
- (* IY: itrees don't particularly capture a notion of fairness, but the
- divergence predicate can be encoded .. *)
- (* This constructor may contain trees that have undefined behavior.
- How does this work w.r.t. fairness? (Also, does UB contain divergence?) *)
fair_div p T σ → has_divergence t -> has_beh p T σ t
| HasBehRet v T σ t:
t ≈ Ret v ->
--
GitLab