diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 1a444090f70d68aeb96a9e0f122c68e2e70619af..0a5df7f414c090178000c63671d2caec66d1a301 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.