diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 0a5df7f414c090178000c63671d2caec66d1a301..0c67948d1dbdfbb1cb16efba3b9b3a56fff468af 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 8384ee91ce3262e7192e05a12aaebec16bc0bf13..a83fea1865cbc68ab42ab4cdae63dc6e8dbd8887 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 Σ :=