diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index ac685874bb2f1aea68115dc43d0cb64e409e5009..b1274e30f759deb47252d1dfa848c2831114048b 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.