From 230f34545952a4b70872a17d9da39d9c5b7551fc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Jan 2016 18:45:56 +0100
Subject: [PATCH] Unit is timeless.

---
 modures/cofe.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/modures/cofe.v b/modures/cofe.v
index b0b2de194..b2c214a1e 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 *)
-- 
GitLab