From 87bf32315e7651d684a5143272aa29d55e53f33d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 May 2017 15:24:44 +0200
Subject: [PATCH] explain a weird design choice

---
 theories/typing/sum.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index c2da2ff9..599957ba 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -9,7 +9,7 @@ Section sum.
   Context `{typeG Σ}.
 
   Program Definition emp : type :=
-    {| ty_size := 1%nat;
+    {| ty_size := 1%nat; (* This is 1 so that emp is equal to the empty sum. *)
        ty_own tid vl := False%I;
        ty_shr κ tid l := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
-- 
GitLab