Merge PR #11957: [stdlib] update sigma-type notations

Reviewed-by: JasonGross
Ack-by: herbelin

2 files changed, 37 insertions, 27 deletions

diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index fdb88a0c82..a5e4178b93 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -68,33 +68,40 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
 
 (** Notations for sigma-types or subsets *)
 
-Reserved Notation "{ A }  + { B }" (at level 50, left associativity).
-Reserved Notation "A + { B }" (at level 50, left associativity).
+Reserved Notation "{ A }  +  { B }" (at level 50, left associativity).
+Reserved Notation "A  +  { B }" (at level 50, left associativity).
 
-Reserved Notation "{ x  |  P }" (at level 0, x at level 99).
-Reserved Notation "{ x  |  P  & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x | P }" (at level 0, x at level 99).
+Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
 
-Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A  |  P  & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
 
-Reserved Notation "{ x  &  P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
-Reserved Notation "{ x : A  & P  & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x & P }" (at level 0, x at level 99).
+Reserved Notation "{ x & P & Q }" (at level 0, x at level 99).
+
+Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
+Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
 
 Reserved Notation "{ ' pat | P }"
-  (at level 0, pat strict pattern, format "{ ' pat  |  P  }").
+  (at level 0, pat strict pattern, format "{ ' pat  |  P }").
 Reserved Notation "{ ' pat | P & Q }"
-  (at level 0, pat strict pattern, format "{ ' pat  |  P  & Q }").
+  (at level 0, pat strict pattern, format "{ ' pat  |  P  &  Q }").
 
 Reserved Notation "{ ' pat : A | P }"
   (at level 0, pat strict pattern, format "{ ' pat  :  A  |  P }").
 Reserved Notation "{ ' pat : A | P & Q }"
-  (at level 0, pat strict pattern, format "{ ' pat  :  A  |  P  & Q }").
+  (at level 0, pat strict pattern, format "{ ' pat  :  A  |  P  &  Q }").
+
+Reserved Notation "{ ' pat & P }"
+  (at level 0, pat strict pattern, format "{ ' pat  &  P }").
+Reserved Notation "{ ' pat & P & Q }"
+  (at level 0, pat strict pattern, format "{ ' pat  &  P  &  Q }").
 
 Reserved Notation "{ ' pat : A & P }"
-  (at level 0, pat strict pattern, format "{ ' pat  :  A  & P }").
+  (at level 0, pat strict pattern, format "{ ' pat  :  A  &  P }").
 Reserved Notation "{ ' pat : A & P & Q }"
-  (at level 0, pat strict pattern, format "{ ' pat  :  A  & P  & Q }").
+  (at level 0, pat strict pattern, format "{ ' pat  :  A  &  P  &  Q }").
 
 (** Support for Gonthier-Ssreflect's "if c is pat then u else v" *)
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 692fe3d8d0..59ee252d35 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -58,23 +58,26 @@ Arguments sig2 (A P Q)%type.
 Arguments sigT (A P)%type.
 Arguments sigT2 (A P Q)%type.
 
-Notation "{ x  |  P }" := (sig (fun x => P)) : type_scope.
-Notation "{ x  |  P  & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
-Notation "{ x : A  |  P }" := (sig (A:=A) (fun x => P)) : type_scope.
-Notation "{ x : A  |  P  & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
+Notation "{ x | P }" := (sig (fun x => P)) : type_scope.
+Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
+Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
+Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) :
   type_scope.
-Notation "{ x  &  P }" := (sigT (fun x => P)) : type_scope.
-Notation "{ x : A  & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
-Notation "{ x : A  & P  & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
+Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.
+Notation "{ x & P & Q }" := (sigT2 (fun x => P) (fun x => Q)) : type_scope.
+Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
+Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) :
   type_scope.
 
-Notation "{ ' pat  |  P }" := (sig (fun pat => P)) : type_scope.
-Notation "{ ' pat  |  P  & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope.
-Notation "{ ' pat : A  |  P }" := (sig (A:=A) (fun pat => P)) : type_scope.
-Notation "{ ' pat : A  |  P  & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) :
+Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope.
+Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope.
+Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope.
+Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) :
   type_scope.
-Notation "{ ' pat : A  & P }" := (sigT (A:=A) (fun pat => P)) : type_scope.
-Notation "{ ' pat : A  & P  & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) :
+Notation "{ ' pat & P }" := (sigT (fun pat => P)) : type_scope.
+Notation "{ ' pat & P & Q }" := (sigT2 (fun pat => P) (fun pat => Q)) : type_scope.
+Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope.
+Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) :
   type_scope.
 
 Add Printing Let sig.