From c2367a655d44016f252b4fa582dfd0222acfb4d3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 4 Apr 2020 09:09:36 +0200
Subject: [PATCH] Fix bug that makes compilation with Coq 8.9 fail.

---
 theories/algebra/ofe.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index ac685874b..b1274e30f 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -955,7 +955,7 @@ Canonical Structure ZO := leibnizO Z.
 
 Section prop.
   Instance Prop_equiv : Equiv Prop := iff.
-  Instance Prop_equivalence : Equivalence (≡@{PROP}) := _.
+  Instance Prop_equivalence : Equivalence (≡@{Prop}) := _.
   Canonical Structure PropO := discreteO Prop.
 End prop.
 
-- 
GitLab