Commit f3ca2f8f authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

small fix

parent ea7f7b7b
Pipeline #17832 failed with stage
......@@ -84,10 +84,10 @@ Definition get : val :=
match r with
InjL n =>
if n = n1 then
complete(l_descr, l_m, l_n, m1, n1, n2, p) ;; #true
complete(l_descr, l_m, l_n, m1, n1, n2, p) ;; n1
else
(* CAS failed, hence we could linearize at the CAS *)
#false
n
| InjR l_descr_other =>
let (l_m', m1', n1', n2', p') := !l_descr_other in
complete(l_descr_other, l_m', l_n, m1', n1', n2', p') ;;
......
Markdown is supported
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