From d204fae0be084a4d39171cae804bf3ff749f5479 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Mar 2017 15:45:45 +0100
Subject: [PATCH] Fix build

This is strange, I did "make vio2vo" before pushing...
---
 theories/typing/lib/fake_shared_box.v  | 2 +-
 theories/typing/lib/refcell/ref_code.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index b0dc67a5..82ef21c1 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,7 +11,7 @@ Section fake_shared_box.
 
   Lemma cell_replace_type ty :
     typed_val fake_shared_box
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
                               [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 1799970b..e1575126 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -116,7 +116,7 @@ Section ref_functions.
 
   Lemma ref_deref_type ty :
     typed_val ref_deref
-      (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-- 
GitLab