diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v index da060db51554e3dd23928e7676e1ddd7cda84891..5d847b13308bb3e97edbe601ec5492411143640f 100644 --- a/heap_lang/tactics.v +++ b/heap_lang/tactics.v @@ -179,6 +179,7 @@ Definition atomic (e : expr) := | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2)) | CAS e0 e1 e2 => bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)) + | Fork _ => true (* Make "skip" atomic *) | App (Rec _ _ (Lit _)) (Lit _) => true | _ => false