From 4427afa1bf250321def267aeaf36e43dd7688bad Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 14:11:41 +0200
Subject: [PATCH] Removed redundant lty scopes

---
 theories/logrel/examples/compute_client_list.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index eb02d4e..3ca9ca8 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -114,7 +114,7 @@ Section compute_example.
 
   Lemma compute_type_client_unfold_app_cont A :
     ⊢ compute_type_client A <:
-        (cont_type A <++> (recv_type A <++> compute_type_client A))%lty.
+        (cont_type A <++> (recv_type A <++> compute_type_client A)).
   Proof.
     rewrite {1}/compute_type_client /lty_rec fixpoint_unfold.
     replace (fixpoint (compute_type_client_aux A)) with
@@ -145,7 +145,7 @@ Section compute_example.
   Qed.
 
   Lemma recv_type_cont_type_swap A B :
-    ⊢ (recv_type B <++> cont_type A <: cont_type A <++> recv_type B)%lty.
+    ⊢ recv_type B <++> cont_type A <: cont_type A <++> recv_type B.
   Proof.
     iApply lty_le_trans.
     rewrite lty_app_recv lty_app_end_l.
@@ -161,7 +161,7 @@ Section compute_example.
   Qed.
 
   Lemma recv_type_stop_type_swap B :
-    ⊢ (recv_type B <++> stop_type <: stop_type <++> recv_type B)%lty.
+    ⊢ recv_type B <++> stop_type <: stop_type <++> recv_type B.
   Proof.
     iApply lty_le_trans.
     rewrite lty_app_recv lty_app_end_l.
-- 
GitLab