diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 1c7c8c5cdb5ac4d2d97b2d20fa8d0ad4465e4a78..5114941cb23b1c4402cecd879976a8012d8cf9f3 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -24,7 +24,7 @@ Section cell.
 
   (* TODO: non-expansiveness, proper wrt. eqtype *)
 
-  Global Instance cell_type :
+  Global Instance cell_copy :
     Copy ty → Copy (cell ty).
   Proof.
     intros ty Hcopy. split; first by intros; simpl; apply _.