diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v index 2097a1b672286109cdd505760453b8ce94cc8fe2..566f525801ab8e67eacf332228bbd2fb34ca33e2 100644 --- a/theories/tests/one_shot.v +++ b/theories/tests/one_shot.v @@ -21,8 +21,8 @@ Definition one_shot_example : val := λ: <>, end)). Definition one_shotR := csumR (exclR unitC) (agreeR ZC). -Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR). -Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR). +Definition Pending : one_shotR := Cinl (Excl ()). +Definition Shot (n : Z) : one_shotR := Cinr (to_agree n). Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }. Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].