From fcd41fdf95716808e623a5e9efe9887a3e967cf0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 Oct 2017 13:03:18 +0100
Subject: [PATCH] Remove useless cast.

---
 theories/tests/one_shot.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index 2097a1b67..566f52580 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].
-- 
GitLab