diff options
| author | Reynald Affeldt | 2020-08-25 23:07:15 +0900 |
|---|---|---|
| committer | Reynald Affeldt | 2020-08-25 23:07:15 +0900 |
| commit | bfd384ed5f7af818f6b893b50d0f8de49477c144 (patch) | |
| tree | f0ede5b76e6bb4f5db5112c873af92cb93ca323b /theories/ssr | |
| parent | a334a9405ee1706747715616f6c5c244036f877a (diff) | |
fix notation-incompatible-format warnings
(mathcomp commit 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b)
Diffstat (limited to 'theories/ssr')
| -rw-r--r-- | theories/ssr/ssrbool.v | 7 |
1 files changed, 6 insertions, 1 deletions
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. |