- Documentation of the Program tactics.

- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.



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

12 files changed, 369 insertions, 166 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b2ef8060d6..ec1246b745 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -352,7 +352,7 @@ let find_tomatch_tycon isevars env loc = function
   | Some (_,ind,_),_ 
   (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
   | None, Some (_,(ind,_)) ->
-      Some (inductive_template isevars env loc ind)
+      Some (0, inductive_template isevars env loc ind)
   | None, None -> 
       empty_tycon
 
@@ -412,7 +412,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
-		  pb.isevars (make_judge current typ) indt).uj_val in
+		  pb.isevars (make_judge current typ) (0, indt)).uj_val in
 	    let sigma = Evd.evars_of !(pb.isevars) in
 	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
 	    ((current,typ),deps))
@@ -1571,8 +1571,9 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
       e_new_evar isevars env  ~src:(loc, Evd.CasesType)
         (Retyping.get_type_of env (Evd.evars_of !isevars) c)
     else
-      map_constr_with_full_binders push_rel build_skeleton env c in
-  names, build_skeleton env (lift n c)
+      map_constr_with_full_binders push_rel build_skeleton env c 
+  in
+    names, build_skeleton env (lift n c)
   
 (* Here, [pred] is assumed to be in the context built from all *)
 (* realargs and terms to match *)
@@ -1639,6 +1640,15 @@ let extract_arity_signature env0 tomatchl tmsign =
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
+let inh_conv_coerce_to_tycon loc env isevars j tycon =
+  match tycon with
+    | Some p ->
+	let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
+          isevars := evd';
+          j
+    | None -> j
+
+
 (* Builds the predicate. If the predicate is dependent, its context is
  * made of 1+nrealargs assumptions for each matched term in an inductive
  * type and 1 assumption for each term not _syntactically_ in an
@@ -1653,11 +1663,11 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
   (* No type annotation *)
   | None ->
       (match tycon with
-       | None -> None
-       | Some t ->
-	 let names,pred = 
-	   prepare_predicate_from_tycon loc false env isevars tomatchs t in
-	 Some (build_initial_predicate false names pred))
+       | Some (0, t) ->
+	   let names,pred = 
+	     prepare_predicate_from_tycon loc false env isevars tomatchs t 
+	   in Some (build_initial_predicate false names pred)
+       | _ -> None)
 
   (* Some type annotation *)
   | Some rtntyp ->
@@ -1665,52 +1675,52 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let arsign = extract_arity_signature env tomatchs sign in
       let env = List.fold_right push_rels arsign env in
       let allnames = List.rev (List.map (List.map pi1) arsign) in
-      let predccl = (typing_fun (mk_tycon (new_Type ())) env rtntyp).uj_val in
-      Some (build_initial_predicate true allnames predccl)
+      let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
+      let _ = 
+	option_app (fun tycon -> 
+		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
+	  tycon
+      in
+      let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
+	Some (build_initial_predicate true allnames predccl)
 
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
   
-  let compile_cases loc (typing_fun, isevars) tycon env (predopt, tomatchl, eqns)=
+let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+  
+  (* We build the matrix of patterns and right-hand-side *)
+  let matx = matx_of_eqns env tomatchl eqns in
+    
+  (* We build the vector of terms to match consistently with the *)
+  (* constructors found in patterns *)
+  let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+    
+  (* We build the elimination predicate if any and check its consistency *)
+  (* with the type of arguments to match *)
+  let tmsign = List.map snd tomatchl in
+  let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
     
-    (* We build the matrix of patterns and right-hand-side *)
-    let matx = matx_of_eqns env tomatchl eqns in
-      
-    (* We build the vector of terms to match consistently with the *)
-    (* constructors found in patterns *)
-    let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
-      
-    (* We build the elimination predicate if any and check its consistency *)
-    (* with the type of arguments to match *)
-    let tmsign = List.map snd tomatchl in
-    let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
-      
-    (* We deal with initial aliases *)
-    let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
-      
-    (* We push the initial terms to match and push their alias to rhs' envs *)
-    (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-    let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-      
-    let pb =
-      { env      = env;
-	isevars  = isevars;
-	pred     = pred;
-	tomatch  = initial_pushed;
-	history  = start_history (List.length initial_pushed);
-	mat      = matx;
-	caseloc  = loc;
-	typing_function = typing_fun } in
-      
-    let _, j = compile pb in
-      
-      (* We check for unused patterns *)
-      List.iter (check_unused_pattern env) matx;
-      
-      match tycon with
-	| Some p ->
-	    let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
-              isevars := evd';
-              j
-	| None -> j
+  (* We deal with initial aliases *)
+  let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
+    
+  (* We push the initial terms to match and push their alias to rhs' envs *)
+  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+  let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+    
+  let pb =
+    { env      = env;
+      isevars  = isevars;
+      pred     = pred;
+      tomatch  = initial_pushed;
+      history  = start_history (List.length initial_pushed);
+      mat      = matx;
+      caseloc  = loc;
+      typing_function = typing_fun } in
+    
+  let _, j = compile pb in
+    (* We check for unused patterns *)
+    List.iter (check_unused_pattern env) matx;
+    inh_conv_coerce_to_tycon loc env isevars j tycon
 end
+  
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index cb8c2cf2b5..d7c8a6dd0c 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -31,7 +31,7 @@ open Mod_subst
 (* *)
 let w_coerce env c ctyp target evd =
   let j = make_judge c ctyp in
-  let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j target in
+  let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j (mk_tycon_type target) in
   (evd',j'.uj_val)
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3b2d85b1ff..841e6b0347 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -40,8 +40,15 @@ module type S = sig
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
-    env -> evar_defs -> unsafe_judgment -> types -> evar_defs * unsafe_judgment
+    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
     
+
+  (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+     is coercible to an object of type [t'] adding evar constraints if needed;
+     it fails if no coercion exists *)
+  val inh_conv_coerces_to : loc -> 
+    env -> evar_defs -> types -> type_constraint_type -> evar_defs
+
   (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
      raises [Not_found] if no coercion found *)
@@ -136,73 +143,129 @@ module Default = struct
 	| _ ->
 	    inh_tosort_force loc env isevars j
 
-  let inh_coerce_to_fail env isevars c1 hj =
-    let hj' =
+  let inh_coerce_to_fail env isevars c1 v t =
+    let v', t' =
       try 
 	let t1,i1 = class_of1 env (evars_of isevars) c1 in
-	let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
+	let t2,i2 = class_of1 env (evars_of isevars) t in
 	let p = lookup_path_between (i2,i1) in
-	  apply_coercion env p hj t2
+	  match v with
+	      Some v -> 
+		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		  Some j.uj_val, j.uj_type
+	    | None -> None, t
       with Not_found -> raise NoCoercion 
     in
-      try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+      try (the_conv_x_leq env t' c1 isevars, v', t')
       with Reduction.NotConvertible -> raise NoCoercion
-
-  let rec inh_conv_coerce_to_fail env isevars hj c1 =
-    let {uj_val = v; uj_type = t} = hj in
-      try (the_conv_x_leq env t c1 isevars, hj)
-      with Reduction.NotConvertible ->
-	(try 
-	   inh_coerce_to_fail env isevars c1 hj
+  open Pp
+  let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
+(*     (try *)
+(*        msgnl (str "inh_conv_coerces_to_fail called for " ++ *)
+(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
+(* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* 	      Termops.print_env env); *)
+(*      with _ -> ()); *)
+    try (the_conv_x_leq env t c1 isevars, v, t)
+    with Reduction.NotConvertible ->
+      (try 
+	 inh_coerce_to_fail env isevars c1 v t
 	 with NoCoercion ->
 	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
 	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
 		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = whd_betadeltaiota env (evars_of isevars) v in
+		    let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in
 		    let (evd',b) =
-		      match kind_of_term v' with
-			| Lambda (_,v1,v2) ->
-			    (try the_conv_x env v1 u1 isevars, true  (* leq v1 u1? *)
-			     with Reduction.NotConvertible -> (isevars, false))
-			| _  -> (isevars,false) in
-		      if b
-		      then 
-			let (x,v1,v2) = destLambda v' in
-			let env1 = push_rel (x,None,v1) env in
-			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
-			  {uj_val = v2; uj_type = t2 } u2 in
-			  (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
-				   uj_type = mkProd (x, v1, h2.uj_type) })
-		      else 
-			(* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
-			(* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
-			(* has type (name:u1)u2 (with v' recursively obtained) *)
-			let name = (match name with 
-				      | Anonymous -> Name (id_of_string "x")
-				      | _ -> name) in
-			let env1 = push_rel (name,None,u1) env in
-			let (evd',h1) =
-			  inh_conv_coerce_to_fail env1 isevars
-			    {uj_val = mkRel 1; uj_type = (lift 1 u1) }
-			    (lift 1 t1) in
-			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
-			  { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
-                            uj_type = subst1 h1.uj_val t2 }
-                          u2
-			in
-			  (evd'',
-			   { uj_val = mkLambda (name, u1, h2.uj_val);
-			     uj_type = mkProd (name, u1, h2.uj_type) })
+		      match v' with 
+			  Some v' ->
+			    (match kind_of_term v' with
+			       | Lambda (x,v1,v2) ->
+				   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)  (* leq v1 u1? *)
+				    with Reduction.NotConvertible -> (isevars, None))
+			       | _  -> (isevars, None))
+			| None -> (isevars, None)
+		    in 
+		      (match b with
+			   Some (x, v1, v2) ->
+			     let env1 = push_rel (x,None,v1) env in
+			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+						       (Some v2) t2 u2 in
+			       (evd'', option_app (fun v2' -> mkLambda (x, v1, v2')) v2', 
+				mkProd (x, v1, t2'))
+			 | None ->
+			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+			     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+			     (* has type (name:u1)u2 (with v' recursively obtained) *)
+			     let name = (match name with 
+					   | Anonymous -> Name (id_of_string "x")
+					   | _ -> name) in
+			     let env1 = push_rel (name,None,u1) env in
+			     let (evd', v1', t1') =
+			       inh_conv_coerce_to_fail loc env1 isevars
+				 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) 
+			     in
+			     let (evd'', v2', t2') = 
+			       let v2 =
+				 match v with 
+				     Some v -> option_app (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+				   | None -> None
+			       and evd', t2 =
+				 match v1' with 
+				     Some v1' -> evd', subst1 v1' t2
+				   | None -> 
+				       let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
+					 evd', subst1 ev t2
+			       in
+				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+			     in
+			       (evd'', option_app (fun v2' -> mkLambda (name, u1, v2')) v2',
+				mkProd (name, u1, t2')))
 		| _ -> raise NoCoercion))
-
+	
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to loc env isevars cj t =
-    let (evd',cj') = 
-      try 
-	inh_conv_coerce_to_fail env isevars cj t
-      with NoCoercion ->
-	let sigma = evars_of isevars in
-	  error_actual_type_loc loc env sigma cj t
+  let inh_conv_coerce_to loc env isevars cj (n, t) =
+    if n = 0 then
+      let (evd', val', type') = 
+	try 
+	  inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	with NoCoercion ->
+	  let sigma = evars_of isevars in
+	    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 })
+    else
+      (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
-      (evd',{ uj_val = cj'.uj_val; uj_type = t })
+      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 *)
 end
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index cc2211f5f8..667f207307 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -38,8 +38,14 @@ module type S = sig
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
-    env -> evar_defs -> unsafe_judgment -> types -> evar_defs * unsafe_judgment
-    
+    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+
+  (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+     is coercible to an object of type [t'] adding evar constraints if needed;
+     it fails if no coercion exists *)
+  val inh_conv_coerces_to : loc -> 
+    env -> evar_defs -> types -> type_constraint_type -> evar_defs
+   
   (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
      raises [Not_found] if no coercion found *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ec8fcd2a8c..e9f605ecb5 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -67,6 +67,17 @@ let nf_evar_info evc info =
     evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
     evar_body = info.evar_body}
 
+let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
+		     evm Evd.empty
+
+let nf_evar_defs isevars = Evd.evars_reset_evd (nf_evars (Evd.evars_of isevars)) isevars
+
+let nf_isevar isevars = nf_evar (Evd.evars_of isevars)
+let j_nf_isevar isevars = j_nf_evar (Evd.evars_of isevars)
+let jl_nf_isevar isevars = jl_nf_evar (Evd.evars_of isevars)
+let jv_nf_isevar isevars = jv_nf_evar (Evd.evars_of isevars)
+let tj_nf_isevar isevars = tj_nf_evar (Evd.evars_of isevars)
+
 (**********************)
 (* Creating new metas *)
 (**********************)
@@ -545,7 +556,9 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 
 (* Operations on value/type constraints *)
 
-type type_constraint = constr option
+type type_constraint_type = int * constr
+type type_constraint = type_constraint_type option
+
 type val_constraint = constr option
 
 (* Old comment...
@@ -565,8 +578,13 @@ type val_constraint = constr option
 (* The empty type constraint *)
 let empty_tycon = None
 
+let mk_tycon_type c = (0, c)
+let mk_abstr_tycon_type n c = (n, c)
+
 (* Builds a type constraint *)
-let mk_tycon ty = Some ty
+let mk_tycon ty = Some (mk_tycon_type ty)
+
+let mk_abstr_tycon n ty = Some (mk_abstr_tycon_type n ty)
 
 (* Constrains the value of a type *)
 let empty_valcon = None
@@ -579,7 +597,7 @@ let mk_valcon c = Some c
 (* Declaring any type to be in the sort Type shouldn't be harmful since
    cumulativity now includes Prop and Set in Type...
    It is, but that's not too bad *)
-let define_evar_as_arrow evd (ev,args) =
+let define_evar_as_abstraction abs evd (ev,args) =
   let evi = Evd.map (evars_of evd) ev in
   let evenv = evar_env evi in
   let (evd1,dom) = new_evar evd evenv (new_Type()) in
@@ -589,14 +607,20 @@ let define_evar_as_arrow evd (ev,args) =
   let newenv = push_named (nvar, None, dom) evenv in
   let (evd2,rng) =
     new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) in
-  let prod = mkProd (Name nvar, dom, subst_var nvar rng) in
+  let prod = abs (Name nvar, dom, subst_var nvar rng) in
   let evd3 = Evd.evar_define ev prod evd2 in
   let evdom = fst (destEvar dom), args in
   let evrng =
     fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
-  let prod' = mkProd (Name nvar, mkEvar evdom, mkEvar evrng) in
+  let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
   (evd3,prod')
 
+let define_evar_as_arrow evd (ev,args) =
+  define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
+
+let define_evar_as_lambda evd (ev,args) =
+  define_evar_as_abstraction (fun t -> mkLambda t) evd (ev,args)
+
 let define_evar_as_sort isevars (ev,args) =
   let s = new_Type () in
   Evd.evar_define ev s isevars, destSort s
@@ -612,20 +636,44 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
    constraint on its domain and codomain. If the input constraint is
    an evar instantiate it with the product of 2 new evars. *)
 
-let split_tycon loc env isevars = function
-  | None -> isevars,(Anonymous,None,None)
-  | Some c ->
-      let sigma = evars_of isevars in
-      let t = whd_betadeltaiota env sigma c in
+let split_tycon loc env isevars tycon = 
+  let rec real_split c = 
+    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, Some dom, Some rng)
+	| Prod (na,dom,rng) -> isevars, (na, mk_tycon dom, mk_tycon 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, Some dom, Some rng)
+	    let (_,dom,rng) = destProd prod in
+	      isevars',(Anonymous, mk_tycon dom, mk_tycon rng)
 	| _ -> error_not_product_loc loc env sigma c
-
-let valcon_of_tycon x = x
-
-let lift_tycon = option_app (lift 1)
+  in
+    match tycon with
+      | None -> isevars,(Anonymous,None,None)
+      | Some (abs, c) ->
+	  if abs = 0 then real_split c
+	  else if abs = 1 then 
+		isevars, (Anonymous, None, mk_tycon c)
+	      else
+		isevars, (Anonymous, None, Some (pred abs, c))
+
+let valcon_of_tycon x = 
+  match x with
+    | Some (0, t) -> Some t
+    | _ -> None
+	
+let lift_tycon_type n (abs, c) = 
+  let abs' = abs + n in 
+    if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
+    else (abs', c)
+
+let lift_tycon n = option_app (lift_tycon_type n)
+
+let pr_tycon_type env (abs, t) =
+  if abs = 0 then Termops.print_constr_env env t
+  else str "Abstract " ++ int abs ++ str " " ++ Termops.print_constr_env env t
+
+let pr_tycon env = function
+    None -> str "None"
+  | Some t -> pr_tycon_type env t
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 8550258c45..7260b5ad35 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -79,6 +79,7 @@ val solve_simple_eqn :
     evar_defs * bool
 
 val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
+val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
 val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
 (***********************************************************)
@@ -86,11 +87,16 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
 val judge_of_new_Type : unit -> unsafe_judgment
 
-type type_constraint = constr option
+type type_constraint_type = int * constr
+type type_constraint = type_constraint_type option
+
 type val_constraint = constr option
 
 val empty_tycon : type_constraint
+val mk_tycon_type : constr -> type_constraint_type
+val mk_abstr_tycon_type : int -> constr -> type_constraint_type
 val mk_tycon : constr -> type_constraint
+val mk_abstr_tycon : int -> constr -> type_constraint
 val empty_valcon : val_constraint
 val mk_valcon : constr -> val_constraint
 
@@ -100,7 +106,8 @@ val split_tycon :
 
 val valcon_of_tycon : type_constraint -> val_constraint
 
-val lift_tycon : type_constraint -> type_constraint
+val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
+val lift_tycon : int -> type_constraint -> type_constraint
 
 (***********************************************************)
 
@@ -117,8 +124,27 @@ val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 val nf_evar_info : evar_map -> evar_info -> evar_info
+val nf_evars : evar_map -> evar_map
+
+(* Same for evar defs *)
+val nf_isevar :  evar_defs -> constr -> constr
+val j_nf_isevar :  evar_defs -> unsafe_judgment -> unsafe_judgment
+val jl_nf_isevar :
+   evar_defs -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_isevar :
+   evar_defs -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_isevar :
+   evar_defs -> unsafe_type_judgment -> unsafe_type_judgment
+
+val nf_evar_defs : evar_defs -> evar_defs
 
 (* Replacing all evars *)
 exception Uninstantiated_evar of existential_key
 val whd_ise :  evar_map -> constr -> constr
 val whd_castappevar :  evar_map -> constr -> constr
+
+(*********************************************************************)
+(* debug pretty-printer: *)
+
+val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
+val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 26df8f7938..5da0a1a999 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -408,6 +408,13 @@ let is_undefined_evar isevars c = match kind_of_term c with
   | Evar ev -> not (is_defined_evar isevars ev)
   | _ -> false
 
+let undefined_evars isevars = 
+  let evd = 
+    fold (fun ev evi sigma -> if evi.evar_body = Evar_empty then 
+	    add sigma ev evi else sigma) 
+      isevars.evars empty
+  in 
+    { isevars with evars = evd }
 
 (* extracts conversion problems that satisfy predicate p *)
 (* Note: conv_pbs not satisying p are stored back in reverse order *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 2f51ebf2d3..35bcb67c70 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -126,6 +126,7 @@ type hole_kind =
   | TomatchTypeParameter of inductive * int
 val is_defined_evar :  evar_defs -> existential -> bool
 val is_undefined_evar :  evar_defs -> constr -> bool
+val undefined_evars : evar_defs -> evar_defs
 val evar_declare :
   Environ.named_context_val -> evar -> types -> ?src:loc * hole_kind ->
   evar_defs -> evar_defs
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index d87a26c223..a0f69e701b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -157,6 +157,9 @@ let error_unsolvable_implicit loc env sigma e =
 let error_cannot_unify env sigma (m,n) =
   raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
 
+let error_cannot_coerce env sigma (m,n) =
+  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index dc8fdd03d9..ad8293a3c7 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -82,6 +82,8 @@ val error_ill_typed_rec_body_loc :
 val error_not_a_type_loc :
   loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
+val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
+
 (*s Implicit arguments synthesis errors *)
 
 val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b99ada7693..217a9714be 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -72,6 +72,9 @@ sig
   
   val understand_tcc :
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+
+  val understand_tcc_evars :
+    evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
     
   (* More general entry point with evars from ltac *)
     
@@ -109,7 +112,7 @@ sig
 
   (* Idem but do not fail on unresolved evars *)
 
-  val understand_judgment_tcc : evar_map -> env -> rawconstr -> evar_map * unsafe_judgment
+  val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
   (*i*)
   (* Internal of Pretyping...
@@ -189,7 +192,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* coerce to tycon if any *)
   let inh_conv_coerce_to_tycon loc env isevars j = function
     | None -> j
-    | Some typ -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j typ
+    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t
 
   let push_rels vars env = List.fold_right push_rel vars env
 
@@ -256,8 +259,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [(evars_of isevars)] and *)
   (* the type constraint tycon *)
-  let rec pretype tycon env isevars lvar = function
-
+  let rec pretype (tycon : type_constraint) env isevars lvar c =
+(*    (try 
+       msgnl (str "pretype with tycon: " ++
+	      Evarutil.pr_tycon env tycon ++ str " with evars: " ++ spc () ++
+	      Evd.pr_evar_defs !isevars ++ str " in env: " ++ spc () ++
+	      Termops.print_env env);
+     with _ -> ());*)
+    match c with
     | RRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env isevars
 	  (pretype_ref isevars env ref)
@@ -285,8 +294,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RHole (loc,k) ->
 	let ty =
           match tycon with 
-            | Some ty -> ty
-            | None ->
+            | Some (n, ty) when n = 0 -> ty
+            | None | Some _ ->
 		e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
 	  { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
 
@@ -344,31 +353,48 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let fj = pretype empty_tycon env isevars lvar f in
-	let floc = loc_of_rawconstr f in
-	let rec apply_rec env n resj = function
+	let length = List.length args in	 
+	let ftycon = 
+	  match tycon with
+	      None -> None
+	    | Some (n, ty) ->
+		if n = 0 then mk_abstr_tycon length ty
+		else Some (n + length, ty)
+	in
+	let fj = pretype ftycon env isevars lvar f in
+ 	let floc = loc_of_rawconstr f in
+	let rec apply_rec env n resj tycon = function
 	  | [] -> resj
 	  | c::rest ->
 	      let argloc = loc_of_rawconstr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
-              let resty =
-		whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
+              let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
 		      let hj = pretype (mk_tycon c1) env isevars lvar c in
-		      let newresj =
-      			{ uj_val = applist (j_val resj, [j_val hj]);
-			  uj_type = subst1 hj.uj_val c2 } in
-			apply_rec env (n+1) newresj rest
+		      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) ->
+			      isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+			      (abs, ty);			      
+			      Some (pred abs, nf_isevar !isevars ty)
+			  | None -> None
+		      in 
+			apply_rec env (n+1) 
+			  { uj_val = nf_isevar !isevars value;
+			    uj_type = nf_isevar !isevars typ' }
+			  tycon rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
 			error_cant_apply_not_functional_loc 
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
-
-	in 
-	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
+	in
+	let ftycon = lift_tycon (-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
 	  | App (f,args) when isInd f ->
@@ -402,7 +428,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j = pretype empty_tycon env isevars lvar c1 in
 	let t = refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
-        let tycon = option_app (lift 1) tycon in
+        let tycon = lift_tycon 1 tycon in
 	let j' = pretype tycon (push_rel var env) isevars lvar c2 in
 	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	    uj_type = subst1 j.uj_val j'.uj_type }
@@ -454,7 +480,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
 		 | None -> 
-		     let tycon = option_app (lift cs.cs_nargs) tycon in
+		     let tycon = lift_tycon cs.cs_nargs tycon in
 		     let fj = pretype tycon env_f isevars lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
@@ -499,17 +525,24 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		let pj = pretype_type empty_valcon env_p isevars lvar p in
 		let ccl = nf_evar (evars_of !isevars) pj.utj_val in
 		let pred = it_mkLambda_or_LetIn ccl psign in
-		  pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
+		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
+		let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred;
+								     uj_type = typ} tycon 
+		in
+		  jtyp.uj_val, jtyp.uj_type
 	    | None -> 
 		let p = match tycon with
-		  | Some ty -> ty
-		  | None ->
+		  | Some (n, ty) when n = 0 -> ty
+		  | None | Some _ ->
                       e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+	  let pred = nf_evar (evars_of !isevars) pred in
+	  let p = nf_evar (evars_of !isevars) p in
+	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
-	    let pi = liftn n 2 pred in
+	    let pi = lift n pred in (* liftn n 2 pred ? *)
 	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
 	    let csgn = 
 	      if not !allow_anonymous_refs then
@@ -523,12 +556,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		cs.cs_args
 	    in
 	    let env_c = push_rels csgn env in 
-	    let bj = pretype (Some pi) env_c isevars lvar b in
+(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
+	    let bj = pretype (mk_tycon pi) env_c isevars lvar b in
 	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
 	  let b1 = f cstrs.(0) b1 in
 	  let b2 = f cstrs.(1) b2 in
-	  let pred = nf_evar (evars_of !isevars) pred in
-	  let p = nf_evar (evars_of !isevars) p in
 	  let v =
 	    let mis,_ = dest_ind_family indf in
 	    let ci = make_default_case_info env IfStyle mis in
@@ -542,7 +574,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  tycon env (* loc *) (po,tml,eqns)
 
     | RCast(loc,c,k,t) ->
-	let tj = pretype_type empty_tycon env isevars lvar t in
+	let tj = pretype_type empty_valcon env isevars lvar t in
 	let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
 	  (* User Casts are for helping pretyping, experimentally not to be kept*)
 	  (* ... except for Correctness *)
@@ -641,22 +673,21 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
 
-  let understand_judgment_tcc sigma env c =
-    let isevars = ref (create_evar_defs sigma) in
+  let understand_judgment_tcc isevars env c =
     let j = pretype empty_tycon env isevars ([],[]) c in
     let sigma = evars_of !isevars in
     let j = j_nf_evar sigma j in
-      sigma, j
+      j
 
   (* Raw calls to the unsafe inference machine: boolean says if we must
      fail on unresolved evars; the unsafe_judgment list allows us to
      extend env with some bindings *)
 
   let ise_pretype_gen fail_evar sigma env lvar kind c =
-    let isevars = ref (create_evar_defs sigma) in
+    let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
       if fail_evar then check_evars env sigma isevars c;
-      (!isevars, c)
+      !isevars, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
@@ -671,10 +702,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   let understand_ltac sigma env lvar kind c =
     ise_pretype_gen false sigma env lvar kind c
+      
+  let understand_tcc_evars isevars env kind c =
+    pretype_gen isevars env ([],[]) kind c
 
   let understand_tcc sigma env ?expected_type:exptyp c =
-    let evars,c = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
-      evars_of evars,c
+    let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+      Evd.evars_of ev, t
 end
 
 module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index ac8e6fec78..ca1a1ded4c 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,6 +38,9 @@ sig
   val understand_tcc :
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
     
+  val understand_tcc_evars :
+    evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
+
   (* More general entry point with evars from ltac *)
     
   (* Generic call to the interpreter from rawconstr to constr, failing
@@ -73,7 +76,7 @@ sig
   val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
   (* Idem but do not fail on unresolved evars *)
-  val understand_judgment_tcc : evar_map -> env -> rawconstr -> evar_map * unsafe_judgment
+  val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
        
   (*i*)