diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index eaac4b40d62f8af74f6c0fb5947be68e24e232f5..4b2f3e886b9f361fd246558ef0fe173807347ca8 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -161,7 +161,7 @@ Section rdcss.
 
   (** Definition of the invariant *)
 
-  (* Extract the TID of the winner from the prophecy value. The winner is the first thread that performs a CAS. *)
+  (** Extract the TID of the winner from the prophecy value. The winner is the first thread that performs a CAS. *)
   Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
     match pvs with
     | (_, LitV (LitProphecy tid)) :: _  => Some tid