From a196520219faf83c60a1ebc067cc365ec99e575d Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 30 Apr 2020 18:45:10 +0200
Subject: [PATCH] Used iMsg notation for session type definitions.

---
 theories/logrel/session_types.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index fd77092..46eeacd 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -7,10 +7,10 @@ Delimit Scope lmsg_scope with lmsg.
 Bind Scope lmsg_scope with lmsg.
 
 Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
-  iMsg_exist M.
+  (∃ v, M v)%msg.
 
 Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
-  iMsg_exist (λ v, iMsg_base v (▷ ltty_car A v) (lsty_car S)).
+  (∃ v, MSG v {{ ▷ ltty_car A v}} ; (lsty_car S))%msg.
 
 Definition lty_end {Σ} : lsty Σ := Lsty END.
 
-- 
GitLab