From 0dab33784b3aacd3afc160cd46a2495a8af97312 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 25 Dec 2016 17:13:53 +0100
Subject: [PATCH] Fix build.
---
theories/typing/borrow.v | 2 +-
theories/typing/sum.v | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index c9062f75..edec4c76 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.base_logic Require Import big_op.
From lrust.lifetime Require Import reborrow frac_borrow.
From lrust.lang Require Import heap.
-From lrust.typing Require Export uniq_bor shr_bor own sum.
+From lrust.typing Require Export uniq_bor shr_bor own.
From lrust.typing Require Import lft_contexts type_context programs.
(** The rules for borrowing and derferencing borrowed non-Copy pointers are in
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 4adb9c51..d261ffeb 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -123,11 +123,11 @@ Section sum.
by iApply (Hty2 with "* [] []"). }
clear -Hleq. iSplit; last iSplit.
- simpl. by rewrite Hleq.
- - iNext. iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+ - iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
iExists i, vl', vl''. iSplit; first done.
iSplit; first by rewrite -Hleq.
iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
- - iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
+ - iAlways. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
iExists i. iSplitR "Hshr".
+ rewrite /is_pad -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
iDestruct "Hlen" as %<-. done.
--
GitLab