diff --git a/program_logic/namespace.v b/program_logic/namespace.v
index 7cab6f273720918d8ad6379f4b7ad54a873c75c0..76e8a34c09f3bd1884392ff625bc742ef393d4bc 100644
--- a/program_logic/namespace.v
+++ b/program_logic/namespace.v
@@ -5,8 +5,7 @@ Definition namespace := list positive.
 Definition nnil : namespace := nil.
 Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
   encode x :: N.
-Definition nclose (N : namespace) : coPset := coPset_suffixes (encode N).
-Coercion nclose : namespace >-> coPset.
+Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
 
 Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.