diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index fe90d7a79d1a33935ed791eae4f4d834f90ab061..f7c195e6329cbb02cbecd1d54b871f0ebb3370e3 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -161,7 +161,6 @@ Section rdcss.
   Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
     match pvs with
     | ((_, #true)%V, LitV (LitProphecy p)) :: _  => Some p
-    | _                         :: vs => proph_extract_winner vs
     | _                               => None
     end.