From 6e9a9572ae0ab130e61b3f06cbcf581f67af1ebf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Dec 2015 15:38:25 +0100
Subject: [PATCH] COFEs on nat and bool.
---
iris/cofe.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/iris/cofe.v b/iris/cofe.v
index 818f266d8..aae619e65 100644
--- a/iris/cofe.v
+++ b/iris/cofe.v
@@ -273,6 +273,8 @@ End discrete_cofe.
Arguments discreteC _ {_ _}.
Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
+Canonical Structure natC := leibnizC nat.
+Canonical Structure boolC := leibnizC bool.
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
--
GitLab