Using `only printing` and fixing coercion in notations

3 files changed, 25 insertions, 59 deletions

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.