Merge PR #6743: Add notation {x & P} for sigT

3 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 0e80215fd..2b10aad68 100644
--- a/CHANGES
+++ b/CHANGES
@@ -281,6 +281,7 @@ Standard Library
   lemmas such as INR_IZR_INZ should be used instead.
 - Real constants are now represented using IZR rather than R0 and R1;
   this might cause rewriting rules to fail to apply to constants.
+- Added new notation {x & P} for sigT (without a type for x)
 
 Plugins
 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 683a442cb..72073bb4f 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -77,6 +77,7 @@ 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  &  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).
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 137bd3a0f..b6afba29a 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -51,6 +51,7 @@ 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)) :
   type_scope.