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

Reviewed-by: JasonGross
Ack-by: herbelin

5 files changed, 103 insertions, 27 deletions

diff --git a/doc/changelog/10-standard-library/11957-signotations.rst b/doc/changelog/10-standard-library/11957-signotations.rst
new file mode 100644
index 0000000000..fc5d434274
--- /dev/null
+++ b/doc/changelog/10-standard-library/11957-signotations.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }``
+  (`#11957 <https://github.com/coq/coq/pull/11957>`_,
+  by Olivier Laurent).
diff --git a/test-suite/output/NotationsSigma.out b/test-suite/output/NotationsSigma.out
new file mode 100644
index 0000000000..0e4df87148
--- /dev/null
+++ b/test-suite/output/NotationsSigma.out
@@ -0,0 +1,40 @@
+{0 = 0} + {0 < 1}
+     : Set
+(0 = 0) + {0 < 1}
+     : Set
+{x : nat | x = 1}
+     : Set
+{x : nat | x = 1 & 0 < x}
+     : Set
+{x : nat | x = 1}
+     : Set
+{x : nat | x = 1 & 0 < x}
+     : Set
+{x : nat & x = 1}
+     : Set
+{x : nat & x = 1 & 0 < x}
+     : Set
+{x : nat & x = 1}
+     : Set
+{x : nat & x = 1 & 0 < x}
+     : Set
+{'(x, _) : nat * ?T | x = 1}
+     : Type
+where
+?T : [pat : nat * ?T |- Type] (pat cannot be used)
+{'(x, y) : nat * nat | x = 1 & y = 0}
+     : Set
+{'(x, _) : nat * nat | x = 1}
+     : Set
+{'(x, y) : nat * nat | x = 1 & y = 0}
+     : Set
+{'(x, _) : nat * ?T & x = 1}
+     : Type
+where
+?T : [pat : nat * ?T |- Type] (pat cannot be used)
+{'(x, y) : nat * nat & x = 1 & y = 0}
+     : Type
+{'(x, _) : nat * nat & x = 1}
+     : Type
+{'(x, y) : nat * nat & x = 1 & y = 0}
+     : Type
diff --git a/test-suite/output/NotationsSigma.v b/test-suite/output/NotationsSigma.v
new file mode 100644
index 0000000000..6780d63a04
--- /dev/null
+++ b/test-suite/output/NotationsSigma.v
@@ -0,0 +1,22 @@
+(* Check notations for sigma types *)
+
+Check { 0 = 0 } + { 0 < 1 }.
+Check (0 = 0) + { 0 < 1 }.
+
+Check { x | x = 1 }.
+Check { x | x = 1 & 0 < x }.
+Check { x : nat | x = 1 }.
+Check { x : nat | x = 1 & 0 < x }.
+Check { x & x = 1 }.
+Check { x & x = 1 & 0 < x }.
+Check { x : nat & x = 1 }.
+Check { x : nat & x = 1 & 0 < x }.
+
+Check {'(x,y) | x = 1 }.
+Check {'(x,y) | x = 1 & y = 0 }.
+Check {'(x,y) : nat * nat | x = 1 }.
+Check {'(x,y) : nat * nat | x = 1 & y = 0 }.
+Check {'(x,y) & x = 1 }.
+Check {'(x,y) & x = 1 & y = 0 }.
+Check {'(x,y) : nat * nat & x = 1 }.
+Check {'(x,y) : nat * nat & x = 1 & y = 0 }.
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.