From 4a85888cd92558c09a5cf87db440a60a2871428c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Jun 2019 10:35:19 +0200
Subject: [PATCH] disable some notation for now

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

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 680d64b82..1568c9917 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.
+*)
-- 
GitLab