5 files changed, 57 insertions, 6 deletions
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 035c4e466..2c2bea4a6 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -107,6 +107,11 @@ Proof.
  intros. symmetry. now apply Nat.lt_succ_pred with m.
 Qed.
 
+Lemma S_pred_pos n: O < n -> n = S (pred n).
+Proof.
+ apply S_pred.
+Qed.
+
 Lemma lt_pred n m : S n < m -> n < pred m.
 Proof.
  apply Nat.lt_succ_lt_pred.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 037d37daf..053ed601f 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -267,6 +267,13 @@ Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
     format "'[' 'exists2'  '/  ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
+Notation "'exists2' ' x , p & q" := (ex2 (fun x => p) (fun x => q))
+  (at level 200, x strict pattern, p at level 200, right associativity) : type_scope.
+Notation "'exists2' ' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
+  (at level 200, x strict pattern, A at level 200, p at level 200, right associativity,
+    format "'[' 'exists2'  '/  ' ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
+  : type_scope.
+
 (** Derived rules for universal quantification *)
 
 Section universal_quantification.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 5e8d2faa5..a9051e761 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -78,6 +78,33 @@ 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 "{ ' 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 }").
+Reserved Notation "{ ' pat : A | P & Q }"
+  (at level 0, pat strict pattern, format "{ ' pat  :  A  |  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 }").
+
+(** Support for Gonthier-Ssreflect's "if c is pat then u else v" *)
+
+Module IfNotations.
+
+Notation "'if' c 'is' p 'then' u 'else' v" :=
+  (match c with p => u | _ => v end)
+  (at level 200, p pattern at level 100).
+
+End IfNotations.
+
+(** Scopes *)
+
 Delimit Scope type_scope with type.
 Delimit Scope function_scope with function.
 Delimit Scope core_scope with core.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 3b4f833a3..47e8a7558 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -53,6 +53,15 @@ 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)) :
+  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.
 Add Printing Let sig2.
 Add Printing Let sigT.
diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v
index a0545c0a4..95c8336d2 100644
--- a/theories/Unicode/Utf8_core.v
+++ b/theories/Unicode/Utf8_core.v
@@ -10,10 +10,12 @@
 
 
 (* Logic *)
-Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)
-  (at level 200, x binder, y binder, right associativity) : type_scope.
-Notation "∃  x .. y , P" := (exists x, .. (exists y, P) ..)
-  (at level 200, x binder, y binder, right associativity) : type_scope.
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' ∀  x  ..  y ']' ,  P") : type_scope.
+Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' ∃  x  ..  y ']' ,  P") : type_scope.
 
 Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
 Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
@@ -25,5 +27,6 @@ Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope.
 Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.
 
 (* Abstraction *)
-Notation "'λ'  x .. y , t" := (fun x => .. (fun y => t) ..)
-  (at level 200, x binder, y binder, right associativity).
+Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' 'λ'  x  ..  y ']' ,  t").