Commit c2367a65 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix bug that makes compilation with Coq 8.9 fail.

parent 5de26893
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment