Fixes for new unification, not used in default version as it really changes unification.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8695 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 6 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index ceb8279fc2..9acb10aeff 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -1,4 +1,12 @@
 Set Implicit Arguments.
+
+Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
+intros.
+induction t.
+exact x.
+Defined.
+
+Check proj1_sig.
 Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
   (t : sig P), P (proj1_sig t).
 Proof.
@@ -7,12 +15,6 @@ induction t.
  simpl ; auto.
 Qed.
 
-Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
-intros.
-induction t.
-exact x.
-Defined.
-
 Lemma ex_pi2  : forall (A : Prop) (P : A -> Prop) (t : ex P),
  P (ex_pi1 t).
 intros A P.
@@ -20,3 +22,13 @@ dependent inversion t.
 simpl.
 exact p.
 Defined.
+
+Notation "'forall' { x : A | P } , Q" :=
+  (forall x:{x:A|P}, Q)
+  (at level 200, x ident, right associativity).
+
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.