diff --git a/theories/examples/rcu.v b/theories/examples/rcu.v
index 9b760c9ff51d927a9a957a7c992178da0e4c3228..87fb87046a98c8cfd603dc51b5a36479ecd61eae 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 :=