fix coq 8.12 warnings

4 files changed, 62 insertions, 84 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index de03369..5f1b7d7 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -158,11 +158,9 @@ Reserved Notation "\sum_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \sum_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\sum_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50). (* only parsing *)
 Reserved Notation "\sum_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50). (* only parsing *)
 Reserved Notation "\sum_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \sum_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -195,11 +193,9 @@ Reserved Notation "\max_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \max_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\max_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50). (* only parsing *)
 Reserved Notation "\max_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50). (* only parsing *)
 Reserved Notation "\max_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \max_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -232,11 +228,9 @@ Reserved Notation "\prod_ ( i | P ) F"
   (at level 36, F at level 36, i at level 50,
            format "'[' \prod_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\prod_ ( i : t | P ) F"
-  (at level 36, F at level 36, i at level 50,
-           only parsing).
+  (at level 36, F at level 36, i at level 50). (* only parsing *)
 Reserved Notation "\prod_ ( i : t ) F"
-  (at level 36, F at level 36, i at level 50,
-           only parsing).
+  (at level 36, F at level 36, i at level 50). (* only parsing *)
 Reserved Notation "\prod_ ( i < n | P ) F"
   (at level 36, F at level 36, i, n at level 50,
            format "'[' \prod_ ( i  <  n  |  P ) '/  '  F ']'").
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 5ec4037..c8b1490 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -101,8 +101,8 @@ Reserved Notation "x != y %[mod_eq e ]" (at level 70, y at next level,
   no associativity,   format "'[hv ' x '/'  !=  y '/'  %[mod_eq  e ] ']'").
 Reserved Notation "x <> y %[mod_eq e ]" (at level 70, y at next level,
   no associativity,   format "'[hv ' x '/'  <>  y '/'  %[mod_eq  e ] ']'").
-Reserved Notation "{eq_quot e }" (at level 0, e at level 0,
-  format "{eq_quot  e }", only parsing).
+Reserved Notation "{eq_quot e }"
+  (at level 0, e at level 0, format "{eq_quot  e }").
 
 Delimit Scope quotient_scope with qT.
 Local Open Scope quotient_scope.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 10a26f1..dd9099b 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -415,13 +415,13 @@ Reserved Notation "~` A" (at level 35, right associativity).
 
 (* Notations for dual partial and total order *)
 Reserved Notation "x <=^d y" (at level 70, y at next level).
-Reserved Notation "x >=^d y" (at level 70, y at next level, only parsing).
+Reserved Notation "x >=^d y" (at level 70, y at next level).
 Reserved Notation "x <^d y" (at level 70, y at next level).
-Reserved Notation "x >^d y" (at level 70, y at next level, only parsing).
+Reserved Notation "x >^d y" (at level 70, y at next level).
 Reserved Notation "x <=^d y :> T" (at level 70, y at next level).
-Reserved Notation "x >=^d y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "x >=^d y :> T" (at level 70, y at next level).
 Reserved Notation "x <^d y :> T" (at level 70, y at next level).
-Reserved Notation "x >^d y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "x >^d y :> T" (at level 70, y at next level).
 Reserved Notation "<=^d y" (at level 35).
 Reserved Notation ">=^d y" (at level 35).
 Reserved Notation "<^d y" (at level 35).
@@ -454,13 +454,13 @@ Reserved Notation "~^d` A" (at level 35, right associativity).
 
 (* Reserved notations for product ordering of prod or seq *)
 Reserved Notation "x <=^p y" (at level 70, y at next level).
-Reserved Notation "x >=^p y" (at level 70, y at next level, only parsing).
+Reserved Notation "x >=^p y" (at level 70, y at next level).
 Reserved Notation "x <^p y" (at level 70, y at next level).
-Reserved Notation "x >^p y" (at level 70, y at next level, only parsing).
+Reserved Notation "x >^p y" (at level 70, y at next level).
 Reserved Notation "x <=^p y :> T" (at level 70, y at next level).
-Reserved Notation "x >=^p y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "x >=^p y :> T" (at level 70, y at next level).
 Reserved Notation "x <^p y :> T" (at level 70, y at next level).
-Reserved Notation "x >^p y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "x >^p y :> T" (at level 70, y at next level).
 Reserved Notation "<=^p y" (at level 35).
 Reserved Notation ">=^p y" (at level 35).
 Reserved Notation "<^p y" (at level 35).
@@ -493,13 +493,13 @@ Reserved Notation "~^p` A" (at level 35, right associativity).
 
 (* Reserved notations for lexicographic ordering of prod or seq *)
 Reserved Notation "x <=^l y" (at level 70, y at next level).
-Reserved Notation "x >=^l y" (at level 70, y at next level, only parsing).
+Reserved Notation "x >=^l y" (at level 70, y at next level).
 Reserved Notation "x <^l y" (at level 70, y at next level).
-Reserved Notation "x >^l y" (at level 70, y at next level, only parsing).
+Reserved Notation "x >^l y" (at level 70, y at next level).
 Reserved Notation "x <=^l y :> T" (at level 70, y at next level).
-Reserved Notation "x >=^l y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "x >=^l y :> T" (at level 70, y at next level).
 Reserved Notation "x <^l y :> T" (at level 70, y at next level).
-Reserved Notation "x >^l y :> T" (at level 70, y at next level, only parsing).
+Reserved Notation "x >^l y :> T" (at level 70, y at next level).
 Reserved Notation "<=^l y" (at level 35).
 Reserved Notation ">=^l y" (at level 35).
 Reserved Notation "<^l y" (at level 35).
@@ -546,11 +546,9 @@ Reserved Notation "\gcd_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \gcd_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\gcd_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\gcd_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\gcd_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \gcd_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -583,11 +581,9 @@ Reserved Notation "\lcm_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \lcm_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\lcm_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\lcm_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\lcm_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \lcm_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -626,11 +622,9 @@ Reserved Notation "\meet_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \meet_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\meet_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\meet_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\meet_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \meet_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -663,11 +657,9 @@ Reserved Notation "\join_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \join_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\join_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\join_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\join_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \join_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -700,11 +692,9 @@ Reserved Notation "\min_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \min_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\min_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\min_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\min_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \min_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -737,11 +727,9 @@ Reserved Notation "\max_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \max_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\max_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\max_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\max_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \max_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -774,11 +762,9 @@ Reserved Notation "\meet^d_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \meet^d_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\meet^d_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\meet^d_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\meet^d_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \meet^d_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -811,11 +797,9 @@ Reserved Notation "\join^d_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \join^d_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\join^d_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\join^d_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\join^d_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \join^d_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -848,11 +832,9 @@ Reserved Notation "\min^d_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \min^d_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\min^d_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\min^d_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\min^d_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \min^d_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -885,11 +867,9 @@ Reserved Notation "\max^d_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \max^d_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\max^d_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\max^d_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\max^d_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \max^d_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -922,11 +902,9 @@ Reserved Notation "\meet^p_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \meet^p_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\meet^p_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\meet^p_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\meet^p_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \meet^p_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -959,11 +937,9 @@ Reserved Notation "\join^p_ ( i | P ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \join^p_ ( i  |  P ) '/  '  F ']'").
 Reserved Notation "\join^p_ ( i : t | P ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\join^p_ ( i : t ) F"
-  (at level 41, F at level 41, i at level 50,
-           only parsing).
+  (at level 41, F at level 41, i at level 50).
 Reserved Notation "\join^p_ ( i < n | P ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \join^p_ ( i  <  n  |  P ) '/  '  F ']'").
@@ -3160,7 +3136,9 @@ Context {T : porderType disp} {T' : porderType disp'}.
 Implicit Types (m n p : nat) (x y z : T) (u v w : T').
 Variables (D D' : {pred T}) (f : T -> T').
 
-Hint Resolve lexx lt_neqAle (@le_anti _ T) (@le_anti _ T') lt_def : core.
+Let leT_anti := @le_anti _ T.
+Let leT'_anti := @le_anti _ T'.
+Hint Resolve lexx lt_neqAle lt_def : core.
 
 Let ge_antiT : antisymmetric (>=%O : rel T).
 Proof. by move=> ? ? /le_anti. Qed.
@@ -3741,8 +3719,12 @@ Context {T : orderType disp} {T' : porderType disp'}.
 Variables (D : {pred T}) (f : T -> T').
 Implicit Types (x y z : T) (u v w : T').
 
-Hint Resolve (@le_anti _ T) (@le_anti _ T') (@lt_neqAle _ T) : core.
-Hint Resolve (@lt_neqAle _ T') (@lt_def _ T) (@le_total _ T) : core.
+Let leT_anti    := @le_anti _ T.
+Let leT'_anti   := @le_anti _ T'.
+Let ltT_neqAle  := @lt_neqAle _ T.
+Let ltT'_neqAle := @lt_neqAle _ T'.
+Let ltT_def     := @lt_def _ T.
+Let leT_total   := @le_total _ T.
 
 Lemma le_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}.
 Proof. exact: total_homo_mono. Qed.
@@ -4869,8 +4851,7 @@ Notation "[ 'porderMixin' 'of' T 'by' <: ]" :=
 
 Notation "[ 'totalOrderMixin' 'of' T 'by' <: ]" :=
   (sub_TotalOrderMixin _ : totalPOrderMixin [porderType of T])
-  (at level 0, format "[ 'totalOrderMixin'  'of'  T  'by'  <: ]",
-   only parsing) : form_scope.
+  (at level 0, only parsing) : form_scope.
 
 Canonical sub_POrderType.
 Canonical sub_LatticeType.
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 ']'").