Skip to content
Snippets Groups Projects
Commit 19480ebd authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy
Browse files

minor change

parent 92d6baf8
No related branches found
No related tags found
1 merge request!26Continuation change, extract_proph_winner change
Hide whitespace changes
Inline Side-by-side
theories/logatom/rdcss/rdcss.v
+ 1
− 1
View file @ 19480ebd
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment