From 5a0f9ffa0a7c4463fa8f83c005c1f8f0a4a8dcd7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 9 Dec 2016 20:03:15 +0100
Subject: [PATCH] OFE instances for number types.

---
 algebra/ofe.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/algebra/ofe.v b/algebra/ofe.v
index 0e59c6727..cf0dff498 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -732,8 +732,11 @@ Proof. by intros x y. Qed.
 Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
 Proof. by intros x y. Qed.
 
-Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
+Canonical Structure natC := leibnizC nat.
+Canonical Structure positiveC := leibnizC positive.
+Canonical Structure NC := leibnizC N.
+Canonical Structure ZC := leibnizC Z.
 
 (* Option *)
 Section option.
-- 
GitLab