From 88efaeeba6b04b9b305ae81311fc8bd013a9acdf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 3 Apr 2020 16:40:37 +0200
Subject: [PATCH] add OFE structure for Prop

---
 theories/algebra/ofe.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 82d3e7dc8..ac685874b 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -946,12 +946,19 @@ Notation discrete_ofe_equivalence_of A := ltac:(
 Instance leibnizO_leibniz A : LeibnizEquiv (leibnizO A).
 Proof. by intros x y. Qed.
 
+(** * Basic Coq types *)
 Canonical Structure boolO := leibnizO bool.
 Canonical Structure natO := leibnizO nat.
 Canonical Structure positiveO := leibnizO positive.
 Canonical Structure NO := leibnizO N.
 Canonical Structure ZO := leibnizO Z.
 
+Section prop.
+  Instance Prop_equiv : Equiv Prop := iff.
+  Instance Prop_equivalence : Equivalence (≡@{PROP}) := _.
+  Canonical Structure PropO := discreteO Prop.
+End prop.
+
 (** * Option type *)
 Section option.
   Context {A : ofeT}.
-- 
GitLab