From 991c1ca90cfc5fddf19112fa6a94d5b3a80d7029 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Sep 2016 12:16:45 +0200
Subject: [PATCH] Comment.
---
perm.v | 2 +-
type.v | 4 ++++
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/perm.v b/perm.v
index da600e7f..b4c0a98c 100644
--- a/perm.v
+++ b/perm.v
@@ -79,4 +79,4 @@ Section duplicable.
Global Instance top_dup : Duplicable ⊤.
Proof. intros tid. apply _. Qed.
-End duplicable.
\ No newline at end of file
+End duplicable.
diff --git a/type.v b/type.v
index b35b238a..3e916c8d 100644
--- a/type.v
+++ b/type.v
@@ -55,6 +55,10 @@ Section defs.
Program Definition ty_of_st (st : simple_type) : type :=
{| ty_size := st.(st_size); ty_dup := true;
ty_own := st.(st_own);
+
+ (* [st.(st_own) tid vl] needs to be outside of the fractured
+ borrow, otherwise I do not knwo how to prove the shr part of
+ [lft_incl_ty_incl_shared_borrow]. *)
ty_shr := λ κ tid _ l,
(∃ vl, (&frac{κ} λ q, l ↦★{q} vl) ★ ▷ st.(st_own) tid vl)%I
|}.
--
GitLab