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

3 files changed, 22 insertions, 18 deletions

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index a9a22ca76e..bbf722dbb2 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -20,11 +20,3 @@ Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
 End FixPoint.
 
 End Well_founded.
-
-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).
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.
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index e0d779ca38..a138c69413 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -423,7 +423,7 @@ module Coercion = struct
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
     (try 
-       trace (str "inh_conv_coerce_to called for " ++
+       trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++
 	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ 
 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -448,7 +448,7 @@ module Coercion = struct
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
     (try 
-       trace (str "inh_conv_coerces_to called for " ++
+       trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++
 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ 
 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -468,8 +468,8 @@ module Coercion = struct
     in
       (* The final range free variables must have been replaced by evars, we accept only that evars
 	 in rng are applied to free vars. *)
-      if noccur_with_meta 0 (succ (nabsinit - nabs)) rng then (
-	trace (str "No occur between 0 and " ++ int (succ (nabsinit - nabs)));
+      if noccur_with_meta 0 (succ nabsinit) rng then (
+	trace (str "No occur between 0 and " ++ int (succ nabsinit));
 	let env', t, t' = 
 	  let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
 	    env', rng, lift nabs t'