diff --git a/iris/cofe.v b/iris/cofe.v
index 818f266d87d87cad19c4982c0fe6d369fc08351a..aae619e6588a4ce32f67c54f002bd6e474619eba 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 }.