From be24d0bd183c3aff2d348c8e349bbcb1cc91fc39 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 15:58:39 +0200
Subject: [PATCH] Nits

---
 theories/logrel/examples/compute_client_list.v | 2 +-
 theories/logrel/examples/compute_service.v     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 0a5df7f..0c67948 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -56,7 +56,7 @@ Section compute_example.
   Definition compute_type_client_aux (A : ltty Σ) (rec : lsty Σ) : lsty Σ :=
     lty_select $ <[cont := (<!!> TY () ⊸ A; <??> TY A ; rec)%lty]> $
                  <[stop := END%lty]>∅.
-  Instance compute_type_rec_client_contractive A :
+  Instance compute_type_client_contractive A :
     Contractive (compute_type_client_aux A).
   Proof. solve_proto_contractive. Qed.
   Definition compute_type_client A : lsty Σ :=
diff --git a/theories/logrel/examples/compute_service.v b/theories/logrel/examples/compute_service.v
index 8384ee9..a83fea1 100644
--- a/theories/logrel/examples/compute_service.v
+++ b/theories/logrel/examples/compute_service.v
@@ -15,14 +15,14 @@ Definition compute_service : val :=
     (λ: "c", let: "v" := recv "c" in
              send "c" ("v" #());; "go" "c")
     (λ: "c", #()).
- 
+
 Section compute_example.
   Context `{heapG Σ, chanG Σ, spawnG Σ}.
 
   Definition compute_type_service_aux (rec : lsty Σ) : lsty Σ :=
     lty_branch $ <[cont := (<?? A> TY () ⊸ A; <!!> TY A ; rec)%lty]> $
                  <[stop := END%lty]> $ ∅.
-  Instance mapper_type_rec_service_contractive :
+  Instance mapper_type_service_contractive :
     Contractive (compute_type_service_aux).
   Proof. solve_proto_contractive. Qed.
   Definition compute_type_service : lsty Σ :=
-- 
GitLab