diff --git a/modures/cofe.v b/modures/cofe.v
index b0b2de1944d7ecbd00507999da15df55d8dd316a..b2c214a1e6f51762f2332220e37e10d5db7877d3 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -235,6 +235,8 @@ Section unit.
   Definition unit_cofe_mixin : CofeMixin unit.
   Proof. by repeat split; try exists 0. Qed.
   Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
+  Global Instance unit_timeless (x : ()) : Timeless x.
+  Proof. done. Qed.
 End unit.
 
 (** Product *)