From c731c726bc675ae9d789153b0913db2fe279867b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 15 Mar 2016 10:49:53 +0100
Subject: [PATCH] simplify the types in join-exist/client_spec

---
 examples/joining_existentials.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/joining_existentials.v b/examples/joining_existentials.v
index 110e84db2..fdfd528a2 100644
--- a/examples/joining_existentials.v
+++ b/examples/joining_existentials.v
@@ -28,7 +28,7 @@ Context (P' : iProp) (P P1 P2 Q Q1 Q2 : X → iProp).
 Context {P_split : (∃ x:X, P x) ⊢ ((∃ x:X, P1 x) ★ (∃ x:X, P2 x))}.
 Context {Q_join  : ((∃ x:X, Q1 x) ★ (∃ x:X, Q2 x)) ⊢ (∃ x:X, Q x)}.
 
-Lemma client_spec eM eM' eW1 eW1' eW2 eW2' (R : iProp) :
+Lemma client_spec (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: [])) (R : iProp) :
   eM' = wexpr' eM → eW1' = wexpr' eW1 → eW2' = wexpr' eW2 →
   R ⊢ ({{ P' }} eM {{ λ _, ∃ x, P x }}) →
   R ⊢ (∀ x, {{ P1 x }} eW1 {{ λ _, Q1 x }}) →
-- 
GitLab