diff options
| author | Cyril Cohen | 2020-06-09 01:16:56 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-09 04:45:15 +0200 |
| commit | 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf (patch) | |
| tree | 805fe2e3ff31c9741ae0ded3cd7ab24b7068f60d /mathcomp/ssreflect/ssrnotations.v | |
| parent | 6784363d60493b8ec154bbf1e827ec677d6b5921 (diff) | |
fix coq 8.12 warnings
Diffstat (limited to 'mathcomp/ssreflect/ssrnotations.v')
| -rw-r--r-- | mathcomp/ssreflect/ssrnotations.v | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v index d85fdf8..ae83c2a 100644 --- a/mathcomp/ssreflect/ssrnotations.v +++ b/mathcomp/ssreflect/ssrnotations.v @@ -63,6 +63,9 @@ Reserved Notation "A :\ b" (at level 50, left associativity). Reserved Notation "<< A >>" (at level 0, format "<< A >>"). Reserved Notation "<[ a ] >" (at level 0, format "<[ a ] >"). +(* Reserved notation for the order of an element (group, polynomial, etc) *) +Reserved Notation "#[ x ]" (at level 0, format "#[ x ]"). + (* Reserved notation for centralisers and centers. *) Reserved Notation "''C' [ x ]" (at level 8, format "''C' [ x ]"). Reserved Notation "''C_' A [ x ]" @@ -72,8 +75,8 @@ Reserved Notation "''C_' B ( A )" (at level 8, B at level 2, format "''C_' B ( A )"). Reserved Notation "''Z' ( A )" (at level 8, format "''Z' ( A )"). (* Compatibility with group action centraliser notation. *) -Reserved Notation "''C_' ( A ) [ x ]" (at level 8, only parsing). -Reserved Notation "''C_' ( B ) ( A )" (at level 8, only parsing). +Reserved Notation "''C_' ( A ) [ x ]" (at level 8). +Reserved Notation "''C_' ( B ) ( A )" (at level 8). (* Reserved notation for Euclidean division and divisibility. *) Reserved Notation "m %/ d" (at level 40, no associativity). @@ -101,8 +104,8 @@ Reserved Notation "x <= y ?= 'iff' c" (at level 70, y, c at next level, (* Reserved notation for cast comparison. *) Reserved Notation "x <= y :> T" (at level 70, y at next level). -Reserved Notation "x >= y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >= y :> T" (at level 70, y at next level). Reserved Notation "x < y :> T" (at level 70, y at next level). -Reserved Notation "x > y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x > y :> T" (at level 70, y at next level). Reserved Notation "x <= y ?= 'iff' c :> T" (at level 70, y, c at next level, - format "x '[hv' <= y '/' ?= 'iff' c :> T ']'").
\ No newline at end of file + format "x '[hv' <= y '/' ?= 'iff' c :> T ']'"). |