From cc9827c0e20813884697f47c1738013cf1738a90 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Mon, 4 Sep 2017 16:10:10 +0200
Subject: [PATCH] one more cleanup
---
theories/examples/rcu.v | 3 ---
1 file changed, 3 deletions(-)
diff --git a/theories/examples/rcu.v b/theories/examples/rcu.v
index 9b760c9f..87fb8704 100644
--- a/theories/examples/rcu.v
+++ b/theories/examples/rcu.v
@@ -541,9 +541,6 @@ Section RCU.
∗ vPred_big_opL (seq 0 NPosn)
(λ _ t, wnToks Γ t (dead D)
∗ [XP (ZplusPos (rc + t) (lhd Γ)) in (D,m) | RCP Γ t]_R).
- (*FIXME [∗ list] t ∈ seq 0 NPosn,
- wnToks Γ t (dead D)
- ∗ [XP (ZplusPos (rc + t) (lhd Γ)) in (D,m) | RCP Γ t]_R)%VP. *)
Local Open Scope VP.
Definition DeadFrom_elem Γ l i : vPred :=
--
GitLab