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

7 files changed, 91 insertions, 80 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'
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b1b02ffd01..aa4a200e74 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -228,39 +228,39 @@ module Default = struct
 		error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
-	    (evd',{ uj_val = val'; uj_type = t })
+	  let nf = nf_isevar evd' in
+	    (evd',{ uj_val = nf val'; uj_type = nf t })
       | Some (init, cur) -> (isevars, cj)
       
-      
-
-  open Pp
-  let inh_conv_coerces_to loc env isevars t (abs, t') = isevars
-  (* Still bugguy 
-(*     (try *)
-(*        msgnl (str "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 () ++ *)
-(* 	      Termops.print_env env); *)
-(*      with _ -> ()); *)
-    try let (rels, rng) = 
-      (* a little more effort to get products is needed *) 
-      try decompose_prod_n abs t
-      with _ -> 
-	raise (Invalid_argument "Coercion.inh_conv_coerces_to")
-    in
-      if noccur_between 0 (succ abs) rng then (
-	(* msgnl (str "No occur between 0 and " ++ int (succ abs)); *)
-	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 abs t'
-	in
-	  try 
-	    pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
-	  with NoCoercion ->
-	    isevars) (* Maybe not enough information to unify *)
-	    (*let sigma = evars_of isevars in
-	      error_cannot_coerce env' sigma (t, t'))*)
-      else isevars
-    with Invalid_argument _ -> isevars *)
+    let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars
+      (* Still problematic, as it changes unification 
+      let nabsinit, nabs = 
+	match abs with
+	    None -> 0, 0
+	  | Some (init, cur) -> init, cur
+      in
+	try 
+	  let (rels, rng) = 
+	    (* a little more effort to get products is needed *) 
+	    try decompose_prod_n nabs t
+	    with _ -> 
+	      if !Options.debug then
+		msg_warning (str "decompose_prod_n failed");
+	      raise (Invalid_argument "Coercion.inh_conv_coerces_to")
+	  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) rng then (
+	      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'
+	      in
+		try 
+		  pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
+		with NoCoercion ->
+		  isevars) (* Maybe not enough information to unify *)
+	      (*let sigma = evars_of isevars in
+		error_cannot_coerce env' sigma (t, t'))*)
+	    else isevars
+	with Invalid_argument _ -> isevars	  *)
 end
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 79e25a5afc..0e3b8f62b3 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -642,38 +642,43 @@ let split_tycon loc env isevars tycon =
     let sigma = evars_of isevars in
     let t = whd_betadeltaiota env sigma c in
       match kind_of_term t with
-	| Prod (na,dom,rng) -> isevars, (na, mk_tycon dom, mk_tycon rng)
+	| Prod (na,dom,rng) -> isevars, (na, dom, rng)
 	| Evar ev when not (Evd.is_defined_evar isevars ev) ->
 	    let (isevars',prod) = define_evar_as_arrow isevars ev in
 	    let (_,dom,rng) = destProd prod in
-	      isevars',(Anonymous, mk_tycon dom, mk_tycon rng)
+	      isevars',(Anonymous, dom, rng)
 	| _ -> error_not_product_loc loc env sigma c
   in
     match tycon with
       | None -> isevars,(Anonymous,None,None)
       | Some (abs, c) ->
 	  (match abs with
-	       None -> real_split c
+	       None -> 
+		 let isevars', (n, dom, rng) = real_split c in
+		   isevars', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
-	       if cur = 1 then isevars, (Anonymous, None, 
-					 Some (Some (init, 0), c))
-	       else
-		 isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
+		 if cur = 0 then 
+		   let isevars', (x, dom, rng) = real_split c in
+		     isevars, (Anonymous, 
+			       Some (Some (init, 0), dom), 
+			       Some (Some (init, 0), rng))
+		 else
+		   isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
 
 let valcon_of_tycon x = 
   match x with
     | Some (None, t) -> Some t
     | _ -> None
 	
-let lift_tycon_type n (abs, t) =
-  abs, lift n t
-(*  match abs with 
-      None -> (abs, lift n t)
+let lift_abstr_tycon_type n (abs, t) =
+  match abs with 
+      None -> raise (Invalid_argument "lift_abstr_tycon_type: not an abstraction")
     | Some (init, abs) ->
 	let abs' = abs + n in 
-	  if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
-	  else (Some (init, abs'), lift n t)*)
+	  if abs' < 0 then raise (Invalid_argument "lift_abstr_tycon_type")
+	  else (Some (init, abs'), t)
 
+let lift_tycon_type n (abs, t) = (abs, lift n t)
 let lift_tycon n = option_app (lift_tycon_type n)
 
 let pr_tycon_type env (abs, t) =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 8c5fe9c99b..6ce30ff79b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -106,6 +106,8 @@ val split_tycon :
 
 val valcon_of_tycon : type_constraint -> val_constraint
 
+val lift_abstr_tycon_type : int -> type_constraint_type -> type_constraint_type
+
 val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
 val lift_tycon : int -> type_constraint -> type_constraint
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b3590492ab..f48ec74624 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -352,9 +352,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      None -> None
 	    | Some (None, ty) -> mk_abstr_tycon length ty
 	    | Some (Some (init, cur), ty) ->
-		Some (Some (length + init, cur), ty)
+		Some (Some (length + init, length + cur), ty)
 	in
-	let fj = pretype ftycon env isevars lvar f in
+	let fj = pretype empty_tycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
 	let rec apply_rec env n resj tycon = function
 	  | [] -> resj
@@ -368,23 +368,23 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
 		      let tycon = 
-			match tycon with			    
-			    Some (abs, ty) ->
-			      (match abs with
-				   None ->
-				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				       (abs, ty);
-				     Some (None, nf_isevar !isevars ty)
-				 | Some (init, cur) ->
-				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				       (abs, ty);
-				     Some (Some (init, pred cur), nf_isevar !isevars ty))
-			  | None -> None
+			option_app 
+			  (fun (abs, ty) ->
+			     match abs with
+				 None ->
+				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+				     (abs, ty);
+				   (abs, ty)
+			       | Some (init, cur) ->
+				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+				     (abs, ty);
+				   (Some (init, pred cur), ty))
+			  tycon
 		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
-			  tycon rest
+			  (option_app (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
@@ -392,7 +392,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = lift_tycon (-1) ftycon in
+	let ftycon = option_app (lift_abstr_tycon_type (-1)) ftycon in
 	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with