From bfd384ed5f7af818f6b893b50d0f8de49477c144 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Tue, 25 Aug 2020 23:07:15 +0900
Subject: fix notation-incompatible-format warnings (mathcomp commit
 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b)

---
 theories/ssr/ssrbool.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index 8c881b1f89..468854f364 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -1310,7 +1310,12 @@ Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x => SimplPred (r x).
 Definition relU {T} (r1 r2 : rel T) := SimplRel (xrelU r1 r2).
 Definition relpre {aT rT} (f : aT -> rT) (r : rel rT) := SimplRel (xrelpre f r).
 
-Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) : fun_scope.
+(* Required to avoid an incompatible format warning with coq-8.12 *)
+Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident,
+  format "'[hv' [ 'rel'  x  y  :  T  | '/ '  E ] ']'").
+
+Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B))
+  (only parsing) : fun_scope.
 Notation "[ 'rel' x y : T | E ]" :=
   (SimplRel (fun x y : T => E%B)) (only parsing) : fun_scope.
 
-- 
cgit v1.2.3