Add notation {x & P} for sigT

Analogous to existing `{x | P}` notation for `sig`, where the type of
`x` is inferred instead of specified.

3 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index cb4b966b0..69f492a9c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -223,6 +223,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 5e8d2faa5..70a6c61e7 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -75,6 +75,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 3b4f833a3..c42cc00b8 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -49,6 +49,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.