diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 680d64b82fba638e419cc7e3b1d4ac1759b40766..1568c9917f5f2a101f72ab072725171ad2f57296 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1454,5 +1454,9 @@ Section sigTOF.
 End sigTOF.
 Arguments sigTOF {_} _%OF.
 
+(*
+FIXME: Notation disabled because it causes strange conflicts in Coq 8.7.
+Enable again once we drop support for that version.
 Notation "{ x  &  P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope.
 Notation "{ x : A &  P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.
+*)