diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 3e3eaea6e7c55ee87dd578d87dac8697972eb649..233fd939a1488ce299b7549f3b1c402494173939 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -163,7 +163,7 @@ Section rdcss.
 
   Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
     match pvs with
-    | ((_, #true)%V, LitV (LitProphecy tid)) :: _  => Some tid
+    | ((_, _)%V, LitV (LitProphecy tid)) :: _  => Some tid
     | _                               => None
     end.