From 55b265face7377a244bf831a5c061385753aafd4 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 14:18:01 +0200
Subject: [PATCH] Killed another lty scope

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

diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 1a44409..0a5df7f 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -41,7 +41,7 @@ Definition compute_client : val :=
     recv_all_par "c" "ys" "n" "lk" "counter");; "ys".
 
 Definition lty_list_aux `{!heapG Σ} (A : ltty Σ) (X : ltty Σ) : ltty Σ :=
-  (() + (A * ref_uniq X))%lty.
+  () + (A * ref_uniq X).
 Instance lty_list_aux_contractive `{!heapG Σ} A :
   Contractive (@lty_list_aux Σ _ A).
 Proof. solve_proto_contractive. Qed.
-- 
GitLab