diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 8 |
2 files changed, 8 insertions, 2 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 935d165..d748fe3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -23,6 +23,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Changed +- in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 + ### Renamed ### Removed diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 892705b..3e493dd 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -38,10 +38,14 @@ Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x => SimplPred (r x). Coercion rel_of_simpl_rel T (sr : simpl_rel T) : rel T := sr. Arguments rel_of_simpl_rel {T} sr x / y : rename. +(* 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)) (at level 0, x ident, y ident, format "'[hv' [ 'rel' x y | '/ ' E ] ']'") : fun_scope. -Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) (at level 0, - x ident, y ident, only parsing) : fun_scope. +Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) + (only parsing) : fun_scope. Notation "[ 'rel' x y 'in' A & B | E ]" := [rel x y | (x \in A) && (y \in B) && E] (at level 0, x ident, y ident, format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'") : fun_scope. |