Using `only printing` and fixing coercion in notations

10 files changed, 58 insertions, 66 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a61116b..024ccc1 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -507,6 +507,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + `coprimez_mul(l|r)` -> `coprimezM(l|r)`
   + `coprimez_exp(l|r)` -> `coprimezX(l|r)`
 
+- in `finset.v`, fixed printing of notation `[set E | x in A , y in B & P ]`
+
 ### Removed
 
 - in `interval.v`, we remove the following:
diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local
index 2de68fc..c9604ab 100644
--- a/mathcomp/Makefile.test-suite.coq.local
+++ b/mathcomp/Makefile.test-suite.coq.local
@@ -1,4 +1,4 @@
-OUTPUT_TESTS=test_suite/output.v
+OUTPUT_TESTS=test_suite/output.v test_suite/imset2_finset.v test_suite/imset2_gproduct.v
 
 OUTPUT_ARTIFACTS=$(OUTPUT_TESTS:%.v=%.v.out.new)
 
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index e234504..9ea0ce4 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -67,10 +67,13 @@ Variant int : Set := Posz of nat | Negz of nat.
 Notation "n %:Z" := (Posz n) (only parsing) : int_scope.
 Notation "n %:Z" := (Posz n) (only parsing) : ring_scope.
 
-Notation "n = m :> 'in' 't'"  := (Posz n = Posz m) : ring_scope.
-Notation "n == m :> 'in' 't'" := (Posz n == Posz m) : ring_scope.
-Notation "n != m :> 'in' 't'" := (Posz n != Posz m) : ring_scope.
-Notation "n <> m :> 'in' 't'" := (Posz n <> Posz m) : ring_scope.
+Notation "n = m :> 'in' 't'"  := (Posz n = Posz m) (only printing) : ring_scope.
+Notation "n == m :> 'in' 't'" := (Posz n == Posz m)
+  (only printing) : ring_scope.
+Notation "n != m :> 'in' 't'" := (Posz n != Posz m)
+  (only printing) : ring_scope.
+Notation "n <> m :> 'in' 't'" := (Posz n <> Posz m)
+  (only printing) : ring_scope.
 
 Definition natsum_of_int (m : int) : nat + nat :=
   match m with Posz p => inl _ p | Negz n => inr _ n end.
@@ -452,8 +455,7 @@ Local Coercion Posz : nat >-> int.
 Implicit Types m n p : nat.
 Implicit Types x y z : int.
 
-Lemma lez_nat m n : (m <= n :> int) = (m <= n)%N.
-Proof. by []. Qed.
+Lemma lez_nat m n : (m <= n :> int) = (m <= n)%N. Proof. by []. Qed.
 
 Lemma ltz_nat  m n : (m < n :> int) = (m < n)%N.
 Proof. by rewrite ltnNge ltNge lez_nat. Qed.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index a844aa8..3d9acd6 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -661,11 +661,14 @@ Local Notation inlined_sub_rect :=
 Local Notation inlined_new_rect :=
   (fun K K_S u => let (x) as u return K u := u in K_S x).
 
+Reserved Notation "[ 'subType' 'for' v ]"
+  (at level 0, format "[ 'subType'  'for'  v ]").
+
 Notation "[ 'subType' 'for' v ]" := (SubType _ v _ inlined_sub_rect vrefl_rect)
- (at level 0, only parsing) : form_scope.
+ (only parsing) : form_scope.
 
-Notation "[ 'sub' 'Type' 'for' v ]" := (SubType _ v _ _ vrefl_rect)
- (at level 0, format "[ 'sub' 'Type'  'for'  v ]") : form_scope.
+Notation "[ 'subType' 'for' v ]" := (SubType _ v _ _ vrefl_rect)
+ (only printing) : form_scope.
 
 Notation "[ 'subType' 'for' v 'by' rec ]" := (SubType _ v _ rec vrefl)
  (at level 0, format "[ 'subType'  'for'  v  'by'  rec ]") : form_scope.
@@ -681,11 +684,13 @@ Definition NewType T U v c Urec :=
   SubType U v (fun x _ => c x) Urec'.
 Arguments NewType [T U].
 
+Reserved Notation "[ 'newType' 'for' v ]" (at level 0, format "[ 'newType'  'for'  v ]").
+
 Notation "[ 'newType' 'for' v ]" := (NewType v _ inlined_new_rect vrefl_rect)
- (at level 0, only parsing) : form_scope.
+ (only parsing) : form_scope.
 
-Notation "[ 'new' 'Type' 'for' v ]" := (NewType v _ _ vrefl_rect)
- (at level 0, format "[ 'new' 'Type'  'for'  v ]") : form_scope.
+Notation "[ 'newType' 'for' v ]" := (NewType v _ _ vrefl_rect)
+ (only printing) : form_scope.
 
 Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl)
  (at level 0, format "[ 'newType'  'for'  v  'by'  rec ]") : form_scope.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index ef47cd2..027b5d4 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -1101,16 +1101,16 @@ Notation "f @2: ( A , B )" := (imset2 f (mem A) (fun _ => mem B))
 Notation "[ 'set' E | x 'in' A ]" := ((fun x => E) @: A)
   (at level 0, E, x at level 99,
    format "[ '[hv' 'set'  E '/ '  |  x  'in'  A ] ']'") : set_scope.
-Notation "[ 'set' E | x 'in' A & P ]" := [set E | x in [set x in A | P]]
+Notation "[ 'set' E | x 'in' A & P ]" := [set E | x in pred_of_set [set x in A | P]]
   (at level 0, E, x at level 99,
    format "[ '[hv' 'set'  E '/ '  |  x  'in'  A '/ '  &  P ] ']'") : set_scope.
 Notation "[ 'set' E | x 'in' A , y 'in' B ]" :=
-  (imset2 (fun x y => E) (mem A) (fun x => (mem B)))
+  (imset2 (fun x y => E) (mem A) (fun x => mem B))
   (at level 0, E, x, y at level 99, format
    "[ '[hv' 'set'  E '/ '  |  x  'in'  A , '/   '  y  'in'  B ] ']'"
   ) : set_scope.
 Notation "[ 'set' E | x 'in' A , y 'in' B & P ]" :=
-  [set E | x in A, y in [set y in B | P]]
+  [set E | x in A, y in pred_of_set [set y in B | P]]
   (at level 0, E, x, y at level 99, format
    "[ '[hv' 'set'  E '/ '  |  x  'in'  A , '/   '  y  'in'  B '/ '  &  P ] ']'"
   ) : set_scope.
@@ -1122,7 +1122,7 @@ Notation "[ 'set' E | x : T 'in' A & P ]" :=
   [set E | x : T in [set x : T in A | P]]
   (at level 0, E, x at level 99, only parsing) : set_scope.
 Notation "[ 'set' E | x : T 'in' A , y : U 'in' B ]" :=
-  (imset2 (fun (x : T) (y : U) => E) (mem A) (fun (x : T) => (mem B)))
+  (imset2 (fun (x : T) (y : U) => E) (mem A) (fun (x : T) => mem B))
   (at level 0, E, x, y at level 99, only parsing) : set_scope.
 Notation "[ 'set' E | x : T 'in' A , y : U 'in' B & P ]" :=
   [set E | x : T in A, y : U in [set y : U in B | P]]
@@ -1133,7 +1133,8 @@ Local Notation predOfType T := (pred_of_simpl (@pred_of_argType T)).
 Notation "[ 'set' E | x : T ]" := [set E | x : T in predOfType T]
   (at level 0, E, x at level 99,
    format "[ '[hv' 'set'  E '/ '  |  x  :  T ] ']'") : set_scope.
-Notation "[ 'set' E | x : T & P ]" := [set E | x : T in [set x : T | P]]
+Notation "[ 'set' E | x : T & P ]" :=
+  [set E | x : T in pred_of_set [set x : T | P]]
   (at level 0, E, x at level 99,
    format "[ '[hv' 'set'  E '/ '  |  x  :  T '/ '  &  P ] ']'") : set_scope.
 Notation "[ 'set' E | x : T , y : U 'in' B ]" :=
@@ -1142,7 +1143,7 @@ Notation "[ 'set' E | x : T , y : U 'in' B ]" :=
    "[ '[hv' 'set'  E '/ '  |  x  :  T , '/   '  y  :  U  'in'  B ] ']'")
    : set_scope.
 Notation "[ 'set' E | x : T , y : U 'in' B & P ]" :=
-  [set E | x : T, y : U in [set y in B | P]]
+  [set E | x : T, y : U in pred_of_set [set y in B | P]]
   (at level 0, E, x, y at level 99, format
  "[ '[hv ' 'set'  E '/'  |  x  :  T , '/  '  y  :  U  'in'  B '/'  &  P ] ']'"
   ) : set_scope.
@@ -1152,7 +1153,7 @@ Notation "[ 'set' E | x : T 'in' A , y : U ]" :=
    "[ '[hv' 'set'  E '/ '  |  x  :  T  'in'  A , '/   '  y  :  U ] ']'")
    : set_scope.
 Notation "[ 'set' E | x : T 'in' A , y : U & P ]" :=
-  [set E | x : T in A, y : U in [set y in P]]
+  [set E | x : T in A, y : U in pred_of_set [set y in P]]
   (at level 0, E, x, y at level 99, format
    "[ '[hv' 'set'  E '/ '  |  x  :  T  'in'  A , '/   '  y  :  U  &  P ] ']'")
    : set_scope.
@@ -1162,7 +1163,7 @@ Notation "[ 'set' E | x : T , y : U ]" :=
    "[ '[hv' 'set'  E '/ '  |  x  :  T , '/   '  y  :  U ] ']'")
    : set_scope.
 Notation "[ 'set' E | x : T , y : U & P ]" :=
-  [set E | x : T, y : U in [set y in P]]
+  [set E | x : T, y : U in pred_of_set [set y in P]]
   (at level 0, E, x, y at level 99, format
    "[ '[hv' 'set'  E '/ '  |  x  :  T , '/   '  y  :  U  &  P ] ']'")
    : set_scope.
@@ -1181,48 +1182,6 @@ Notation "[ 'set' E | x , y ]" := [set E | x : _, y : _]
 Notation "[ 'set' E | x , y & P ]" := [set E | x : _, y : _ & P ]
   (at level 0, E, x, y at level 99, only parsing) : set_scope.
 
-(* Print-only variants to work around the Coq pretty-printer K-term kink. *)
-Notation "[ 'se' 't' E | x 'in' A , y 'in' B ]" :=
-  (imset2 (fun x y => E) (mem A) (fun _ => mem B))
-  (at level 0, E, x, y at level 99, format
-   "[ '[hv' 'se' 't'  E '/ '  |  x  'in'  A , '/   '  y  'in'  B ] ']'")
-   : set_scope.
-Notation "[ 'se' 't' E | x 'in' A , y 'in' B & P ]" :=
-  [se t E | x in A, y in [set y in B | P]]
-  (at level 0, E, x, y at level 99, format
- "[ '[hv ' 'se' 't'  E '/'  |  x  'in'  A , '/  '  y  'in'  B '/'  &  P ] ']'"
-  ) : set_scope.
-Notation "[ 'se' 't' E | x : T , y : U 'in' B ]" :=
-  (imset2 (fun x (y : U) => E) (mem (predOfType T)) (fun _ => mem B))
-  (at level 0, E, x, y at level 99, format
-   "[ '[hv ' 'se' 't'  E '/'  |  x  :  T , '/  '  y  :  U  'in'  B ] ']'")
-   : set_scope.
-Notation "[ 'se' 't' E | x : T , y : U 'in' B & P ]" :=
-  [se t E | x : T, y : U in [set y in B | P]]
-  (at level 0, E, x, y at level 99, format
-"[ '[hv ' 'se' 't'  E '/'  |  x  :  T , '/  '  y  :  U  'in'  B '/'  &  P ] ']'"
-  ) : set_scope.
-Notation "[ 'se' 't' E | x : T 'in' A , y : U ]" :=
-  (imset2 (fun x y => E) (mem A) (fun _ : T => mem (predOfType U)))
-  (at level 0, E, x, y at level 99, format
-   "[ '[hv' 'se' 't'  E '/ '  |  x  :  T  'in'  A , '/   '  y  :  U ] ']'")
-   : set_scope.
-Notation "[ 'se' 't' E | x : T 'in' A , y : U & P ]" :=
-  (imset2 (fun x (y : U) => E) (mem A) (fun _ : T => mem [set y \in P]))
-  (at level 0, E, x, y at level 99, format
-"[ '[hv ' 'se' 't'  E '/'  |  x  :  T  'in'  A , '/  '  y  :  U '/'  &  P ] ']'"
-  ) : set_scope.
-Notation "[ 'se' 't' E | x : T , y : U ]" :=
-  [se t E | x : T, y : U in predOfType U]
-  (at level 0, E, x, y at level 99, format
-   "[ '[hv' 'se' 't'  E '/ '  |  x  :  T , '/   '  y  :  U ] ']'")
-   : set_scope.
-Notation "[ 'se' 't' E | x : T , y : U & P ]" :=
-  [se t E | x : T, y : U in [set y in P]]
-  (at level 0, E, x, y at level 99, format
-   "[ '[hv' 'se' 't'  E '/'  |  x  :  T , '/   '  y  :  U '/'  &  P ] ']'")
-   : set_scope.
-
 Section FunImage.
 
 Variables aT aT2 : finType.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index a8b677d..9d2b6c0 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -285,12 +285,14 @@ Notation "[ 'pick' x | P ]" := (pick (fun x => P%B))
 Notation "[ 'pick' x : T | P ]" := (pick (fun x : T => P%B))
   (at level 0, x ident, only parsing) : form_scope.
 Definition pick_true T (x : T) := true.
+Reserved Notation "[ 'pick' x : T ]"
+  (at level 0, x ident, format "[ 'pick'  x : T ]").
 Notation "[ 'pick' x : T ]" := [pick x : T | pick_true x]
-  (at level 0, x ident, only parsing).
+  (only parsing) : form_scope.
+Notation "[ 'pick' x : T ]" := [pick x : T | pick_true _]
+  (only printing) : form_scope.
 Notation "[ 'pick' x ]" := [pick x : _]
   (at level 0, x ident, only parsing) : form_scope.
-Notation "[ 'pic' 'k' x : T ]" := [pick x : T | pick_true _]
-  (at level 0, x ident, format "[ 'pic' 'k'  x : T ]") : form_scope.
 Notation "[ 'pick' x | P & Q ]" := [pick x | P && Q ]
   (at level 0, x ident,
    format "[ '[hv ' 'pick'  x  |  P '/ '   &  Q ] ']'") : form_scope.
diff --git a/mathcomp/test_suite/imset2_finset.v b/mathcomp/test_suite/imset2_finset.v
new file mode 100644
index 0000000..c27a611
--- /dev/null
+++ b/mathcomp/test_suite/imset2_finset.v
@@ -0,0 +1,6 @@
+From mathcomp Require Import all_ssreflect.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Check @imset2_pair.
diff --git a/mathcomp/test_suite/imset2_finset.v.out b/mathcomp/test_suite/imset2_finset.v.out
new file mode 100644
index 0000000..f58fd8a
--- /dev/null
+++ b/mathcomp/test_suite/imset2_finset.v.out
@@ -0,0 +1,3 @@
+imset2_pair
+     : forall (aT aT2 : finType) (A : {set aT}) (B : {set aT2}),
+       [set (x, y) | x in A, y in B] = setX A B
diff --git a/mathcomp/test_suite/imset2_gproduct.v b/mathcomp/test_suite/imset2_gproduct.v
new file mode 100644
index 0000000..7b80a8d
--- /dev/null
+++ b/mathcomp/test_suite/imset2_gproduct.v
@@ -0,0 +1,7 @@
+From mathcomp Require Import all_ssreflect all_fingroup.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import GroupScope.
+Open Scope group_scope.
+Check @ker_sdprodm.
diff --git a/mathcomp/test_suite/imset2_gproduct.v.out b/mathcomp/test_suite/imset2_gproduct.v.out
new file mode 100644
index 0000000..673c27c
--- /dev/null
+++ b/mathcomp/test_suite/imset2_gproduct.v.out
@@ -0,0 +1,6 @@
+ker_sdprodm
+     : forall (gT rT : finGroupType) (H K G : {group gT})
+         (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT})
+         (eqHK_G : H ><| K = G) (actf : {in H & K, morph_act 'J 'J fH fK}),
+       'ker (sdprodm eqHK_G actf) =
+       [set a * b^-1 | a in H, b in K & fH a == fK b]