From a26a33679c78ad78864d2ead76b000bd7e45da02 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Mar 2016 10:34:55 +0100
Subject: [PATCH] remark about one_shot

---
 algebra/one_shot.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 65a96aa4d..14cb69b26 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
+(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *)
 Inductive one_shot {A : Type} :=
   | OneShotPending : one_shot
   | Shot : A → one_shot
-- 
GitLab