- 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

15 files changed, 703 insertions, 273 deletions

diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index 6face72d11..a9a22ca76e 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -21,8 +21,10 @@ End FixPoint.
 
 End Well_founded.
 
-(*Check Fix_sub.*)
-
 Notation "'forall' { x : A | P } , Q" :=
-  (forall x:{x:A|P}, (fun x => Q) (proj1_sig x))
-  (at level 200, x ident, right associativity).
\ No newline at end of file
+  (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
new file mode 100644
index 0000000000..ceb8279fc2
--- /dev/null
+++ b/contrib/subtac/Utils.v
@@ -0,0 +1,22 @@
+Set Implicit Arguments.
+Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
+  (t : sig P), P (proj1_sig t).
+Proof.
+intros.
+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.
+dependent inversion t.
+simpl.
+exact p.
+Defined.
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index ced1756f13..5703c0efc1 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -10,10 +10,14 @@ open Names
 open Evd
 open List
 open Pp
+open Util
 
 let reverse_array arr = 
   Array.of_list (List.rev (Array.to_list arr))
     
+let trace s = 
+  if !Options.debug then msgnl s
+  else ()
 
 (** Utilities to find indices in lists *)
 let list_index x l =
@@ -37,14 +41,14 @@ let subst_evars evs n t =
       | [] -> raise Not_found
     in 
     let (idx, hyps, v) = aux 0 evs in
-      idx + 1, hyps
+      n + idx + 1, hyps
   in
   let rec substrec depth c = match kind_of_term c with
     | Evar (k, args) ->
 	(try 
 	   let index, hyps = evar_info k in
-	     msgnl (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
-		      int (List.length hyps) ++ str " hypotheses");
+	     trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+		    int (List.length hyps) ++ str " hypotheses");
 
 	   let ex = mkRel (index + depth) in
 	     (* Evar arguments are created in inverse order, 
@@ -63,8 +67,7 @@ let subst_evars evs n t =
 	   in
 	     mkApp (ex, Array.of_list args)
 	 with Not_found -> 
-	   msgnl (str "Evar " ++ int k ++ str " not found!!!");
-	   c)
+	   anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found"))
     | _ -> map_constr_with_binders succ substrec depth c
   in 
     substrec 0 t
@@ -100,29 +103,33 @@ let etype_of_evar evs ev hyps =
 
 open Tacticals
     
-let eterm evm t = 
+let eterm_term evm t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
   let evl = to_list evm in
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
-    fold_left 
-      (fun l (id, ev) ->
+    fold_right 
+      (fun (id, ev) l ->
 	 let hyps = Environ.named_context_of_val ev.evar_hyps in
 	 let y' = (id, hyps, etype_of_evar l ev hyps) in
 	   y' :: l) 
-      [] evl 
+      evl []
   in 
   let t' = (* Substitute evar refs in the term by De Bruijn indices *)
     subst_evars evts 0 t 
   in
-  let t'' = 
-    (* Make the lambdas 'generalizing' the existential variables *)
-    fold_left
-      (fun acc (id, _, c) ->
-	 mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)),
-		   c, acc))
-      t' evts
+  let evar_names = 
+    List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts
+  in
+  let evar_bl =
+    List.map (fun (id, c) -> Name id, None, c) evar_names
+  in
+  let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
+    (* Generalize over the existential variables *)
+  let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl 
+  and tycon = option_app 
+		(fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
   in
   let _declare_evar (id, c) =
     let id = id_of_string ("Evar" ^ string_of_int id) in
@@ -133,12 +140,29 @@ let eterm evm t =
     let id = id_of_string ("Evar" ^ string_of_int id) in
       tclTHEN acc (Tactics.assert_tac false (Name id) c)
   in
-    msgnl (str "Term given to eterm" ++ spc () ++
+    trace (str "Term given to eterm" ++ spc () ++
 	   Termops.print_constr_env (Global.env ()) t);
-    msgnl (str "Term constructed in eterm" ++ spc () ++
+    trace (str "Term constructed in eterm" ++ spc () ++
 	   Termops.print_constr_env (Global.env ()) t'');
-    Tactics.apply_term t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts)
+    ignore(option_app 
+	     (fun typ ->
+		trace (str "Type :" ++ spc () ++
+		       Termops.print_constr_env (Global.env ()) typ))
+	     tycon);
+    t'', tycon, evar_names
+
+let mkMetas n = 
+  let rec aux i acc = 
+    if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc)
+    else acc
+  in aux n []
+
+let eterm evm t (tycon : types option) = 
+  let t, tycon, evs = eterm_term evm t tycon in
+    match tycon with
+	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) []
+      | None -> Tactics.apply_term t (mkMetas (List.length evs))
      
 open Tacmach
 
-let etermtac (evm, t) = eterm evm t
+let etermtac (evm, t) = eterm evm t None
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index bcb9b4c56d..d6f058ebda 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -9,5 +9,12 @@
 (*i $Id$ i*)
 
 open Tacmach
+open Term
+open Evd
+open Names
 
-val etermtac : Evd.open_constr -> tactic
+val mkMetas : int -> constr list
+
+val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list
+
+val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index d9c7a8c023..2f47608c10 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -49,13 +49,6 @@ GEXTEND Gram
     ;
   END
 
-(* type wf_proof_type_argtype = (Subtac_utils.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
-
-(* let (wit_subtac_wf_proof_type : wf_proof_type_argtype), *)
-(*   (globwit_subtac_wf_proof_type : wf_proof_type_argtype), *)
-(*   (rawwit_subtac_wf_proof_type : wf_proof_type_argtype) = *)
-(*   Genarg.create_arg "subtac_wf_proof_type" *)
-
 type gallina_loc_argtype = (Vernacexpr.vernac_expr located, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
 
 let (wit_subtac_gallina_loc : gallina_loc_argtype),
@@ -63,18 +56,6 @@ let (wit_subtac_gallina_loc : gallina_loc_argtype),
   (rawwit_subtac_gallina_loc : gallina_loc_argtype) =
   Genarg.create_arg "subtac_gallina_loc"
 
-(* type subtac_recdef_argtype = (Subtac_utils.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *)
-
-(* let (wit_subtac_recdef : subtac_recdef_argtype), *)
-(*   (globwit_subtac_recdef : subtac_recdef_argtype), *)
-(*   (rawwit_subtac_recdef : subtac_recdef_argtype) = *)
-(*   Genarg.create_arg "subtac_recdef" *)
-
-(* VERNAC COMMAND EXTEND SubtacRec *)
-(* [ "Recursive" "program" ident(id) subtac_binders(l) subtac_recdef(f) ] ->  *)
-(*   [ Interp.subtac id l Environ.empty_env f ] *)
-(* END *)
-  
 VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> 
   [ Subtac.subtac g ]
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 01c959a47d..8b59b7eff5 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -119,6 +119,7 @@ let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
   require_library "Coq.subtac.FixSub";
+  require_library "Coq.subtac.Utils";
   try
     match command with
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index c605314018..4b4a25e718 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -35,7 +35,7 @@ let make_name s = Name (id_of_string s)
 
 module Coercion = struct
 
-  exception NoCoercion
+  exception NoSubtacCoercion
 
   let rec disc_subset x = 
     match kind_of_term x with
@@ -86,6 +86,8 @@ module Coercion = struct
       | Type _, Prop Null -> Prop Null
       | _, Type _ -> s2
 
+  let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
+
   let rec mu env isevars t =   
     let rec aux v = 
       match disc_subset v with
@@ -101,17 +103,22 @@ module Coercion = struct
   and coerce loc env isevars (x : Term.constr) (y : Term.constr) 
       : (Term.constr -> Term.constr) option 
       =
-    trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
-	     str " and "++ my_print_constr env y);
-
+    let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
+      trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
+	     str " and "++ my_print_constr env y ++ 
+	     str " with evars: " ++ spc () ++
+	     my_print_evardefs !isevars);
     let rec coerce_unify env x y =
-      if e_cumul env isevars x y then (
+      trace (str "coerce_unify from " ++ (my_print_constr env x) ++ 
+	     str " to "++ my_print_constr env y);
+      try 
+	isevars := the_conv_x_leq env x y !isevars;
 	trace (str "Unified " ++ (my_print_constr env x) ++ 
-		 str " and "++ my_print_constr env y);
+	       str " and "++ my_print_constr env y);
 	None
-      ) else coerce' env x y (* head recutions needed *)
+      with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
     and coerce' env x y : (Term.constr -> Term.constr) option =
-      let subco () = subset_coerce env x y in
+      let subco () = subset_coerce env isevars x y in
 	trace (str "coerce' from " ++ (my_print_constr env x) ++ 
 		 str " to "++ my_print_constr env y);
 	match (kind_of_term x, kind_of_term y) with
@@ -137,43 +144,78 @@ module Coercion = struct
 		  
 	  | App (c, l), App (c', l') ->
 	      (match kind_of_term c, kind_of_term c' with
-		   Ind i, Ind i' ->
+		   Ind i, Ind i' -> (* Sigma types *)
 		     let len = Array.length l in
 		     let existS = Lazy.force existS in
-		       if len = Array.length l' && len = 2
-			 && i = i' && i = Term.destInd existS.typ 
-		       then
-			 begin (* Sigma types *)
-			   debug 1 (str "In coerce sigma types");
-			   let (a, pb), (a', pb') = 
-			     pair_of_array l, pair_of_array l' 
-			   in
-			   let c1 = coerce_unify env a a' in
-			   let remove_head c = 
-			     let (_, _, x) = Term.destProd c in
-			       x
-			   in
-			   let b, b' = remove_head pb, remove_head pb' in
-			   let env' = push_rel (make_name "x", None, a) env in
-			   let c2 = coerce_unify env' b b' in
-			     match c1, c2 with
-				 None, None -> None
-			       | _, _ ->
-				   Some 
-				     (fun x ->
-					let x, y = 
-					  app_opt c1 (mkApp (existS.proj1,
-							     [| a; pb; x |])),
-					  app_opt c2 (mkApp (existS.proj2, 
-							     [| a; pb'; x |]))
-					in
-					  mkApp (existS.intro, [| x ; y |]))
-			 end
+		     let prod = Lazy.force prod in
+		       if len = Array.length l' && len = 2 && i = i'
+		       then 
+			 if i = Term.destInd existS.typ 
+			 then
+			   begin 
+			     debug 1 (str "In coerce sigma types");
+			     let (a, pb), (a', pb') = 
+			       pair_of_array l, pair_of_array l' 
+			     in
+			     let c1 = coerce_unify env a a' in
+			     let rec remove_head a c = 
+			       match kind_of_term c with 
+				 | Lambda (n, t, t') -> c, t'
+				     (*| Prod (n, t, t') -> t'*)
+				 | Evar (k, args) ->
+				     let (evs, t) = Evarutil.define_evar_as_lambda !isevars (k,args) in
+				       isevars := evs;
+				       let (n, dom, rng) = destLambda t in
+				       let (domk, args) = destEvar dom in
+					 isevars := evar_define domk a !isevars;
+					 t, rng
+				 | _ -> raise NoSubtacCoercion
+			     in
+			     let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
+			     let env' = push_rel (make_name "x", None, a) env in
+			     let c2 = coerce_unify env' b b' in
+			       match c1, c2 with
+				   None, None -> 
+				     trace (str "No coercion needed");
+				     None
+				 | _, _ ->
+				     Some 
+				       (fun x ->
+					  let x, y = 
+					    app_opt c1 (mkApp (existS.proj1,
+							       [| a; pb; x |])),
+					    app_opt c2 (mkApp (existS.proj2, 
+							       [| a; pb; x |]))
+					  in
+					    mkApp (existS.intro, [| a'; pb'; x ; y |]))
+			   end
+			 else if i = Term.destInd prod.typ then
+			   begin 
+			     debug 1 (str "In coerce prod types");
+			     let (a, b), (a', b') = 
+			       pair_of_array l, pair_of_array l' 
+			     in
+			     let c1 = coerce_unify env a a' in
+			     let c2 = coerce_unify env b b' in
+			       match c1, c2 with
+				   None, None -> None
+				 | _, _ ->
+				     Some 
+				       (fun x ->
+					  let x, y = 
+					    app_opt c1 (mkApp (prod.proj1,
+							       [| a; b; x |])),
+					    app_opt c2 (mkApp (prod.proj2, 
+							       [| a; b; x |]))
+					  in
+					    mkApp (prod.intro, [| a'; b'; x ; y |]))
+			   end
+			 else subco ()
 		       else subco ()
 		 | _ ->  subco ())
 	  | _, _ ->  subco ()
 
-    and subset_coerce env x y =
+    and subset_coerce env isevars x y =
       match disc_subset x with
 	  Some (u, p) -> 
 	    let c = coerce_unify env u y in
@@ -193,15 +235,16 @@ module Coercion = struct
 			   (mkApp 
 			      ((Lazy.force sig_).intro, 
 			       [| u; p; cx; evar |])))
-	      | None -> raise NoCoercion
+	      | None -> 
+		  raise NoSubtacCoercion
+		    (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars;
+		  None*)
     in coerce_unify env x y
 
-  let coerce_itf loc env isevars hj c1 =
-    let {uj_val = v; uj_type = t} = hj in
+  let coerce_itf loc env isevars v t c1 =
     let evars = ref isevars in
     let coercion = coerce loc env evars t c1 in
-      !evars, {uj_val = app_opt coercion v;
-	       uj_type = t}
+      !evars, option_app (app_opt coercion) v, t
 	
   (* Taken from pretyping/coercion.ml *)
 
@@ -224,9 +267,8 @@ module Coercion = struct
     in 
       apply_rec [] funj.uj_type argl
 
-  exception NoCoercion
-
   (* appliquer le chemin de coercions de patterns p *)
+  exception NoCoercion
 
   let apply_pattern_coercion loc pat p =
     List.fold_left
@@ -275,7 +317,7 @@ module Coercion = struct
 	       try 
 		 let coercef, t = mu env isevars t in
 		   (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
-	       with NoCoercion ->
+	       with NoSubtacCoercion | NoCoercion ->
 		 (isevars,j))
 
   let inh_tosort_force loc env isevars j =
@@ -297,79 +339,141 @@ module Coercion = 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
+  let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
+    (try
+       trace (str "inh_conv_coerce_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 =
-    trace (str "inh_conv_coerce_to called for " ++ (my_print_constr env cj.uj_type) ++ 
-	     str " and "++ my_print_constr env t);
-    let (evd',cj') = 
-      try 
-	inh_conv_coerce_to_fail env isevars cj t
-      with NoCoercion ->
-	try
-	  coerce_itf loc env isevars cj t
+  let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
+    (try 
+       trace (str "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 () ++
+	      Termops.print_env env);
+     with _ -> ());
+    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
-	    debug 2 (str "No coercion found");
-	    error_actual_type_loc loc env sigma cj t
+	    try
+	      coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
+	    with NoSubtacCoercion ->
+	      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)
+
+  let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
+    (try 
+       trace (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 _ -> ());
+    let (rels, rng) = 
+      (* a little more effort to get products is needed *) 
+      try decompose_prod_n abs t
+      with _ -> 
+	trace (str "decompose_prod_n failed");
+	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to")
     in
-      (evd',{ uj_val = cj'.uj_val; uj_type = t })
+      (* 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 abs) rng then (
+	trace (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 (try inh_conv_coerce_to_fail loc env' isevars None t t'
+		 with NoCoercion ->
+		   coerce_itf loc env' isevars None t t') 
+	  with NoSubtacCoercion ->
+	    let sigma = evars_of isevars in
+	      error_cannot_coerce env' sigma (t, t'))
+      else isevars 
 end
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 5659950bc9..94f2d70ac4 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -1,4 +1,3 @@
-
 open Closure
 open RedFlags
 open Declarations
@@ -34,7 +33,9 @@ open Mod_subst
 open Printer
 open Inductiveops
 open Syntax_def
-
+open Environ
+open Tactics
+open Tacticals
 open Tacinterp
 open Vernacexpr
 open Notation
@@ -46,13 +47,17 @@ open Pretyping
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
+let evar_nf isevars c =
+  isevars := Evarutil.nf_evar_defs !isevars;
+  Evarutil.nf_isevar !isevars c
+
 let interp_gen kind isevars env 
                ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
   let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
-    non_instanciated_map env isevars, c'
+    evar_nf isevars c'
     
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c 
@@ -64,14 +69,47 @@ let interp_casted_constr isevars env ?(impls=([],[])) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c 
 
 let interp_open_constr isevars env c =
-  SPretyping.pretype_gen isevars env ([], []) (OfType None) 
-    (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
+  let c = SPretyping.pretype_gen isevars env ([], []) (OfType None) 
+	    (Constrintern.intern_constr (Evd.evars_of !isevars) env c) in
+    evar_nf isevars c
 
 let interp_constr_judgment isevars env c =
-  let s, j = SPretyping.understand_judgment_tcc (Evd.evars_of !isevars) env
-    (Constrintern.intern_constr (Evd.evars_of !isevars) env c)
-  in 
-    Evd.create_evar_defs s, j
+  let j = 
+    SPretyping.understand_judgment_tcc isevars env
+      (Constrintern.intern_constr (Evd.evars_of !isevars) env c) 
+  in
+    { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
+
+let locate_if_isevar loc na = function
+  | RHole _ -> 
+      (try match na with
+	| Name id ->  Reserve.find_reserved_type id
+	| Anonymous -> raise Not_found 
+      with Not_found -> RHole (loc, Evd.BinderType na))
+  | x -> x
+
+let interp_binder sigma env na t =
+  let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
+    SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t)
+      
+
+let interp_context sigma env params = 
+  List.fold_left
+    (fun (env,params) d -> match d with
+      | LocalRawAssum ([_,na],(CHole _ as t)) ->
+	  let t = interp_binder sigma env na t in
+	  let d = (na,None,t) in
+	  (push_rel d env, d::params)
+      | LocalRawAssum (nal,t) ->
+	  let t = interp_type sigma env t in
+	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+	  let ctx = List.rev ctx in
+	  (push_rel_context ctx env, ctx@params)
+      | LocalRawDef ((_,na),c) ->
+	  let c = interp_constr_judgment sigma env c in
+	  let d = (na, Some c.uj_val, c.uj_type) in
+	  (push_rel d env,d::params))
+    (env,[]) params
 
 (* try to find non recursive definitions *)
 
@@ -85,7 +123,7 @@ let collect_non_rec env =
       let i = 
         list_try_find_i
           (fun i f ->
-             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+             if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec
              then i else failwith "try_find_i")
           0 lnamerec 
       in
@@ -108,6 +146,9 @@ let collect_non_rec env =
   in 
   searchrec [] 
 
+let definition_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is defined")
+
 let recursive_message v =
   match Array.length v with
     | 0 -> error "no recursive definition"
@@ -115,13 +156,27 @@ let recursive_message v =
     | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
 		    spc () ++ str "are recursively defined")
 
+let filter_map f l = 
+  let rec aux acc = function
+      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
+		     | None -> aux acc tl)
+    | [] -> List.rev acc
+  in aux [] l
+
+let list_of_local_binders l = 
+  let rec aux acc = function
+      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
+    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
+	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
+    | [] -> List.rev acc
+  in aux [] l
+
 let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
   let sigma = Evd.empty
   and env0 = Global.env()
-  and protos = List.map (fun ((f, n, _, _, _),_) -> f,n) lnameargsardef
   in 
-  let lnameargsardef = 
-    List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))
+  let lnameargsardef =
+    (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
       lnameargsardef
   in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
@@ -130,16 +185,56 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
   (* Build the recursive context and notations for the recursive types *)
   let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
-      (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> 
-        let arityc = Command.generalize_constr_expr arityc bl in
-	let isevars = ref (Evd.create_evar_defs sigma) in
-        let isevars, arity = interp_type isevars env0 arityc in
-	let impl = 
-	  if Impargs.is_implicit_args()
-	  then Impargs.compute_implicits env0 arity
-	  else [] in
-	let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
-          (Environ.push_named (recname,None,arity) env, impls', (isevars, arity)::arl))
+      (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) -> 
+	let isevars = ref (Evd.create_evar_defs sigma) in	  
+	  match ro with
+	      CStructRec ->
+		let arityc = Command.generalize_constr_expr arityc bl in
+		let arity = interp_type isevars env0 arityc in
+		let impl = 
+		  if Impargs.is_implicit_args()
+		  then Impargs.compute_implicits env0 arity
+		  else [] in
+		let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+		  (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
+	    | CWfRec r -> 		    
+		let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
+			       Ppconstr.pr_binders bl ++ str " : " ++ 
+			       Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+			       Ppconstr.pr_constr_expr body)
+		in
+		let env', binders_rel = interp_context isevars env0 bl in
+		let before, ((argname, _, argtyp) as arg), after = list_chop_hd n binders_rel in
+		let argid = match argname with Name n -> n | _ -> assert(false) in
+		let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
+		let envwf = push_rel_context before env0 in
+		let wf_rel = interp_constr isevars envwf r in
+		let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
+		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| wf_rel; mkRel 1 |])) in
+		let argid' = id_of_string (string_of_id argid ^ "'") in
+		let before_length, after_length = List.length before, List.length after in
+		let full_length = before_length + 1 + after_length in
+		let wfarg = (Name argid, None, 
+			     mkSubset (Name argid') argtyp 
+			       (mkApp (wf_rel, [|mkRel 1; mkRel (full_length + 1)|])))
+		in
+		let new_bl = before @ (arg :: accarg :: after')
+		and intern_bl =  before @ (wfarg :: after)
+		in
+		let intern_env = push_rel_context intern_bl env0 in
+		let env' = push_rel_context new_bl env0 in
+		let arity = interp_type isevars intern_env arityc in
+		let intern_arity = it_mkProd_or_LetIn arity intern_bl in
+		let arity' = interp_type isevars env' arityc in
+		let arity' = it_mkProd_or_LetIn arity' new_bl in
+		let fun_bl = before @ (arg :: (Name recname, None, arity) :: after') in
+		let impl = 
+		  if Impargs.is_implicit_args()
+		  then Impargs.compute_implicits intern_env arity'
+		  else [] in
+		let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
+		  (Environ.push_named (recname,None,arity') env, impls', 
+		   (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
       (env0,[],[]) lnameargsardef in
   let arityl = List.rev arityl in
   let notations = 
@@ -155,10 +250,17 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
 	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
 	List.map2
-	  (fun ((_,_,bl,_,def),_) (evm, arity) ->
-             let def = abstract_constr_expr def bl in
-               interp_casted_constr (ref (Evd.create_evar_defs evm)) rec_sign ~impls:([],rec_impls)
-		def arity)
+	  (fun ((_,_,bl,_,def),_) (isevars, info, arity) ->
+	     match info with
+		 None ->
+		   let def = abstract_constr_expr def bl in
+		     isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+		       def arity
+	       | Some (n, artyp, wfrel, bl, intern_bl, intern_arity) ->
+		   let rec_sign = push_rel_context bl rec_sign in
+		   let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+				def intern_arity
+		   in isevars, info, cstr)
           lnameargsardef arityl
       with e ->
 	States.unfreeze fs; raise e in
@@ -173,7 +275,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
       Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
     let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
     let rec declare i fi =
-      trace (str "Declaring: " ++ pr_id fi);
+      trace (str "Declaring: " ++ pr_id fi ++ spc () ++
+	     my_print_constr env0 (recvec.(i)));
       let ce = 
 	{ const_entry_body = mkFix ((nvrec',i),recdecls); 
           const_entry_type = Some arrec.(i);
@@ -185,76 +288,131 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
       (* declare the recursive definitions *)
     let lrefrec = Array.mapi declare namerec in
       Options.if_verbose ppnl (recursive_message lrefrec);
-      (*  (* The others are declared as normal definitions *)
-	  let var_subst id = (id, Constrintern.global_reference id) in
-	  let _ = 
-	  List.fold_left
+
+
+      (*(* The others are declared as normal definitions *)
+      let var_subst id = (id, Constrintern.global_reference id) in
+      let _ = 
+	List.fold_left
 	  (fun subst (f,def,t) ->
-	  let ce = { const_entry_body = replace_vars subst def;
-	  const_entry_type = Some t;
-          const_entry_opaque = false;
-	  const_entry_boxed = boxed } in
-	  let _ =
-	  Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
-	  in
-      	  warning ((string_of_id f)^" is non-recursively defined");
-      	  (var_subst f) :: subst)
+	     let ce = { const_entry_body = replace_vars subst def;
+			const_entry_type = Some t;
+			const_entry_opaque = false;
+			const_entry_boxed = boxed } in
+	     let _ =
+	       Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
+	     in
+      	       warning ((string_of_id f)^" is non-recursively defined");
+      	       (var_subst f) :: subst)
 	  (List.map var_subst (Array.to_list namerec))
 	  lnonrec 
-	  in*)
+      in*)
       List.iter (fun (df,c,scope) ->
 		   Metasyntax.add_notation_interpretation df [] c scope) notations
   in 
   let declare l = 
     let recvec = Array.of_list l
-    and arrec = Array.map snd arrec
+    and arrec = Array.map pi3 arrec
     in declare arrec recvec
   in
   let recdefs = Array.length defrec in
     trace (int recdefs ++ str " recursive definitions");
     (* Solve remaining evars *)
-  let rec solve_evars i acc = 
+  let rec collect_evars i acc = 
     if i < recdefs then
-      let (evm, def) = defrec.(i) in
-	if Evd.dom evm = [] then 
-	  solve_evars (succ i) (def :: acc)
-	else
-	  let _,typ = arrec.(i) in
-	  let id = namerec.(i) in
-	    (* Generalize by the recursive prototypes  *)
-	  let def = 
-	    Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
-	  and typ = 
-	    Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
-	  let tac = Eterm.etermtac (evm, def) in 
-	  let _ =
-	    trace (str "Starting proof of a fixpoint def:" ++ spc () ++ my_print_constr env0 def ++
-		   spc () ++ str " with goal: " ++ my_print_constr env0 typ ++
-		   spc () ++ str " with evar map = " ++ Evd.pr_evar_map evm)
-	  in
-	    begin
-	      Command.start_proof (id_of_string (string_of_id id ^ "_evars"))  goal_kind typ
-		(fun _ gr -> 
-		   let _ = trace (str "Got a proof of: " ++ pr_global gr) in
-		   let constant = match gr with Libnames.ConstRef c -> c
-		     | _ -> assert(false)
-		   in
-		     try 
-		       let def = Environ.constant_value (Global.env ()) constant in
-		       let _ = trace (str "Got constant value") in		 
-		       let _, c = decompose_lam_n recdefs def in
-		       let _ = trace (str "Fixpoint body is: " ++ spc () ++ my_print_constr (Global.env ()) c) in
-			 solve_evars (succ i) (c :: acc)
-		     with Environ.NotEvaluableConst cer ->
-		       match cer with
-			   Environ.NoBody -> trace (str "Constant has no body")
-			 | Environ.Opaque -> trace (str "Constant is opaque")
-		);
-	      trace (str "Started proof");
-	      Pfedit.by tac;
-	      trace (str "Applied eterm tac");
-	    end
-    else declare (List.rev acc)
-  in solve_evars 0 []
+      let (isevars, info, def) = defrec.(i) in
+      let _ = trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) in
+      let def = evar_nf isevars def in
+      let isevars = Evd.undefined_evars !isevars in
+      let _ = trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) in
+      let evm = Evd.evars_of isevars in
+      let _, _, typ = arrec.(i) in
+      let id = namerec.(i) in
+      let def = 
+	match info with 
+	    Some (n, artyp, wfrel, funbl, bl, arity) ->
+	      def (* mkApp (def, *)
 
-    
+	  | None -> def
+		     in
+	(* Generalize by the recursive prototypes  *)
+      let def = 
+	Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
+      and typ = 
+	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
+      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 
+      (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
+      (*let fi = id_of_string (string_of_id id ^ "_evars") in*)
+      (*let ce = 
+	{ const_entry_body = evars_def; 
+	  const_entry_type = Some evars_typ;
+	  const_entry_opaque = false;
+	  const_entry_boxed = boxed} in
+      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in
+	definition_message fi;
+	trace (str (string_of_id fi) ++ str " is defined");*)
+	let evar_sum =
+	  if evars = [] then None
+	  else 
+	    let sum = Subtac_utils.build_dependent_sum evars in
+	      trace (str "Evars sum: " ++ my_print_constr env0 (pi1 sum));
+	      Some sum
+	in
+	  collect_evars (succ i) ((id, evars_def, evar_sum) :: acc)
+    else acc
+  in 
+  let defs = collect_evars 0 [] in
+
+  (* Solve evars then create the definitions *)
+  let real_evars = 
+    filter_map (fun (id, kn, sum) ->
+		  match sum with Some (sumg, sumtac, _) -> Some (id, kn, sumg, sumtac) | None -> None)
+      defs
+  in
+    Subtac_utils.and_tac real_evars
+      (fun f _ gr ->
+	 let _ = trace (str "Got a proof of: " ++ pr_global gr) in
+	 let constant = match gr with Libnames.ConstRef c -> c
+	   | _ -> assert(false)
+	 in
+	   try
+	     (*let value = Environ.constant_value (Global.env ()) constant in*)
+	     let pis = f (mkConst constant) in
+	       trace (str "Accessors: " ++
+		      List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
+			pis (mt()));
+	       trace (str "Applied existentials: " ++
+		      (List.fold_right
+			 (fun (id, kn, sumg, pi) acc ->
+			    let args = Subtac_utils.destruct_ex pi sumg in
+			      my_print_constr env0 (mkApp (kn, Array.of_list args)))
+			 pis (mt ())));
+	       let rec aux pis acc = function
+		   (id, kn, sum) :: tl ->
+		     (match sum with 
+			  None -> aux pis (kn :: acc) tl
+			| Some (sumg, _, _) -> 
+			    let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
+			    let args = Subtac_utils.destruct_ex pi sumg in
+			    let args = 
+			      List.map (fun c -> 
+					  try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c
+					  with Not_found ->
+					    trace (str "Not_found while reducing " ++
+						   my_print_constr (Global.env ()) c);
+					    c
+				       ) args 				  
+			    in
+			    let _, newdef = decompose_lam_n (recdefs + List.length args) kn in
+			    let constr = Term.substl (mkRel 1 :: List.rev args) newdef in
+			      aux pis (constr :: acc) tl)
+		 | [] -> List.rev acc
+	       in
+		 declare (aux pis [] defs)
+	   with Environ.NotEvaluableConst cer ->
+	     match cer with
+		 Environ.NoBody -> trace (str "Constant has no body")
+	       | Environ.Opaque -> trace (str "Constant is opaque")
+      )
+      
+      
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 6c1b0103ff..e1bbbbb5b0 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -16,26 +16,26 @@ val interp_gen :
   ?impls:full_implicits_env ->
   ?allow_soapp:bool ->
   ?ltacvars:ltac_sign ->
-  constr_expr -> evar_map * constr
+  constr_expr -> constr
 val interp_constr :
   evar_defs ref ->
-  env -> constr_expr -> evar_map * constr
+  env -> constr_expr -> constr
 val interp_type :
   evar_defs ref ->
   env ->
   ?impls:full_implicits_env ->
-  constr_expr -> evar_map * constr
+  constr_expr -> constr
 val interp_casted_constr :
   evar_defs ref ->
   env ->
   ?impls:full_implicits_env ->
-  constr_expr -> types -> evar_map * constr
+  constr_expr -> types -> constr
 val interp_open_constr :
   evar_defs ref -> env -> constr_expr -> constr
 val interp_constr_judgment :
   evar_defs ref ->
   env ->
-  constr_expr -> evar_defs * unsafe_judgment
+  constr_expr -> unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
 val recursive_message : global_reference array -> std_ppcmds
 val build_recursive :
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 3ed5790e33..599dbe39e2 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -51,8 +51,8 @@ let list_of_local_binders l =
     | [] -> List.rev acc
   in aux [] l
        
-let abstract_constr_expr_bl c bl =
-  List.fold_right (fun (n, t) c -> mkLambdaC ([n], t, c)) bl c
+let abstract_constr_expr_bl abs c bl =
+  List.fold_right (fun (n, t) c -> abs ([n], t, c)) bl c
 
 let pr_binder_list b = 
   List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++
@@ -73,14 +73,14 @@ let rewrite_fixpoint env l (f, decl) =
 			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
 			 Ppconstr.pr_constr_expr body)
 	  in
-	  let after, before = list_chop n bls in
+	  let before, after = list_chop n bls in
 	  let _ = trace (str "Binders before the recursion arg: " ++ spc () ++
 			 pr_binder_list before ++ str "; after the recursion arg: " ++
 			 pr_binder_list after)
 	  in
-	  let ((locn, name), ntyp), before = match before with
+	  let ((locn, name) as lnid, ntyp), after = match after with
 	      hd :: tl -> hd, tl
-	    | _ -> assert(false) (* Rec arg must be in before *)
+	    | _ -> assert(false) (* Rec arg must be in after *)
 	  in
 	  let nid = match name with
 	      Name id -> id
@@ -96,27 +96,36 @@ let rewrite_fixpoint env l (f, decl) =
 	      id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid)
 	  in
 	  let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in
-	  let coqP = abstract_constr_expr_bl typ after in
+	  let wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
+	  let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in
+	  let typnid' = mkSubset lnid' ntyp wf_prop in
+	  let internal_type = 
+	    abstract_constr_expr_bl mkProdC 
+	      (mkProdC ([lnid'], typnid', 
+			mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'), 
+				  abstract_constr_expr_bl mkProdC typ after)))
+	      before
+	  in
 	  let body' =
-	    let prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
-	    let lamprop = mkLambdaC ([lnid'], ntyp, prop) in
-	    let typnid' = mkSubset lnid' ntyp prop in
+	    let body =
+	      (* cast or we will loose some info at pretyping time as body
+		 is a function *)
+	      CCast (dummy_loc, body,  DEFAULTcast, typ) 
+	    in
 	    let body' = (* body abstracted by rec call *)
-	      mkLambdaC ([(dummy_loc, Name id)], 
-			 mkProdC ([lnid'], typnid', coqP),
-			 body)
+	      mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
 	    in
 	      mkAppC (body',
 		      [mkLambdaC 
 			 ([lnid'], typnid',
 			  mkAppC (mkIdentC id, 
-				  [mkProj1 ntyp lamprop (mkIdentC nid');
+				  [mkProj1 ntyp lam_wf_prop (mkIdentC nid');
 				   (mkAppExplC (acc_inv_ref,
 						[ ntyp; wfrel;
 						  mkIdentC nid;
 						  mkIdentC accproofid;
-						  mkProj1 ntyp lamprop (mkIdentC nid');
-						  mkProj2 ntyp lamprop (mkIdentC nid') ])) ]))])
+						  mkProj1 ntyp lam_wf_prop (mkIdentC nid');
+						  mkProj2 ntyp lam_wf_prop (mkIdentC nid') ])) ]))])
 	  in
 	  let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in
 	  let bl' = 
@@ -127,12 +136,12 @@ let rewrite_fixpoint env l (f, decl) =
 		  let rec aux' bl' = function
 		      ((loc, name') as x) :: tl ->
 			if name' = name then
-			  LocalRawAssum (List.rev (x :: bl'), typ) ::
-			    LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
-			    if tl = [] then [] else [LocalRawAssum (tl, typ)]
+			  (if tl = [] then [] else [LocalRawAssum (tl, typ)]) @
+			  LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
+			    [LocalRawAssum (List.rev (x :: bl'), typ)]
 			else aux' (x :: bl') tl
 		    | [] -> [assum]
-		  in aux (acc @ List.rev (aux' [] bl)) tl
+		  in aux (aux' [] bl @ acc) tl
 	      | [] -> List.rev acc
 	    in aux [] bl
 	  in
@@ -173,7 +182,7 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
   let po = 
     List.fold_right
       (fun (n,t) acc ->
-	 RProd (dummy_loc, n, t, acc))
+	 RProd (dummy_loc, Anonymous, t, acc))
       eqs_types (match po with 
 		     Some e -> e
 		   | None -> mkHole)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index ef551aa8d2..b0de064167 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -12,10 +12,6 @@ val mkProj2 :
 val list_of_local_binders :
   Topconstr.local_binder list ->
   (Names.name Util.located * Topconstr.constr_expr) list
-val abstract_constr_expr_bl :
-  Topconstr.constr_expr ->
-  (Names.name Util.located * Topconstr.constr_expr) list ->
-  Topconstr.constr_expr
 val pr_binder_list :
   (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
 val rewrite_rec_calls : 'a -> 'b -> 'b
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 5cc7351855..f73a6e393d 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -71,7 +71,8 @@ let merge_evms x y =
 
 let interp env isevars c tycon = 
   let j = pretype tycon env isevars ([],[]) c in
-    j.uj_val, j.uj_type
+  let evm = evars_of !isevars in    
+    nf_evar evm j.uj_val, nf_evar evm j.uj_type
 
 let find_with_index x l =
   let rec aux i = function
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index eb9888c161..d620c8e9fa 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -12,11 +12,15 @@ let contrib_name = "subtac"
 
 let subtac_dir = [contrib_name]
 let fix_sub_module = "FixSub"
+let utils_module = "Utils"
 let fixsub_module = subtac_dir @ [fix_sub_module]
+let utils_module = subtac_dir @ [utils_module]
 let init_constant dir s = gen_constant contrib_name dir s
 let init_reference dir s = gen_reference contrib_name dir s
 
 let fixsub = lazy (init_constant fixsub_module "Fix_sub")
+let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
+let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
 
 let make_ref s =  Qualid (dummy_loc, (qualid_of_string s))
 let well_founded_ref = make_ref "Init.Wf.Well_founded"
@@ -41,6 +45,12 @@ let eqind = lazy (init_constant ["Init"; "Logic"] "eq")
 let eqind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
 let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
 
+let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
+let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
+
+let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
+let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
+
 let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
 let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
 let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
@@ -49,9 +59,14 @@ let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
   
 let existS = lazy (build_sigma_set ())
 
+let prod = lazy (build_prod ())
+
+
 (* orders *)
 let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
 let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
+let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
+let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
 
 let extconstr = Constrextern.extern_constr true (Global.env ())
 let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
@@ -62,21 +77,22 @@ let my_print_constr = Termops.print_constr_env
 let my_print_context = Termops.print_rel_context
 let my_print_env = Termops.print_env
 let my_print_rawconstr = Printer.pr_rawconstr_env
+let my_print_evardefs = Evd.pr_evar_defs
+
+let my_print_tycon_type = Evarutil.pr_tycon_type
 
-let debug_level = ref 0
 
 let debug n s = 
-  if n >= !debug_level then (
-    msgnl s;
-    msg_warning s;
-  ) else ()
+  if !Options.debug then
+    msgnl s
+  else ()
 
 let debug_msg n s = 
-  if n >= !debug_level then s
+  if !Options.debug then s
   else mt ()
 
 let trace s = 
-  if !debug_level < 2 then (msgnl s)
+  if !Options.debug then msgnl s
   else ()
 
 let wf_relations = Hashtbl.create 10
@@ -138,3 +154,92 @@ let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definiti
 
 let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
 let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
+
+open Tactics
+open Tacticals
+
+let build_dependent_sum l =
+  let rec aux (acc, tac, typ) = function
+      (n, t) :: tl ->
+	let t' = mkLambda (Name n, t, typ) in
+	  trace (str ("treating " ^ string_of_id n) ++
+		 str "assert: " ++ my_print_constr (Global.env ()) t);
+	let tac' = 
+	  tclTHEN (assert_tac true (Name n) t) 
+	    (tclTHENLIST
+	       [intros;
+		(tclTHENSEQ 
+		   [tclTRY (constructor_tac (Some 1) 1 
+		       (Rawterm.ImplicitBindings [mkVar n]));
+		    tac]);
+	       ])
+	in
+	  aux (mkApp (Lazy.force ex_ind, [| t; t'; |]), tac', t') tl
+    | [] -> acc, tac, typ
+  in 
+    match l with 
+	(_, hd) :: tl -> aux (hd, intros, hd) tl
+      | [] -> raise (Invalid_argument "build_dependent_sum")
+
+open Proof_type
+open Tacexpr
+
+let mkProj1 a b c = 
+  mkApp (Lazy.force proj1, [| a; b; c |])
+
+let mkProj2 a b c = 
+  mkApp (Lazy.force proj2, [| a; b; c |])
+
+let mk_ex_pi1 a b c =
+  mkApp (Lazy.force ex_pi1, [| a; b; c |])
+
+let mk_ex_pi2 a b c =
+  mkApp (Lazy.force ex_pi2, [| a; b; c |])
+    
+
+let mkSubset name typ prop = 
+  mkApp ((Lazy.force sig_).typ,
+	 [| typ; mkLambda (name, typ, prop) |])
+
+let and_tac l hook =
+  let andc = Coqlib.build_coq_and () in      
+  let rec aux ((accid, goal, tac, extract) as acc) = function
+    | [] -> (* Singleton *) acc
+	
+    | (id, x, elgoal, eltac) :: tl ->
+	let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
+	let proj = fun c -> mkProj2 goal elgoal c in
+	let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
+	  aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac', 
+	       (id, x, elgoal, proj) :: extract) tl
+
+  in
+  let and_proof_id, and_goal, and_tac, and_extract = 
+    match l with
+      | [] -> raise (Invalid_argument "and_tac: empty list of goals")
+      | (hdid, x, hdg, hdt) :: tl -> aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
+  in
+  let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
+    Command.start_proof and_proofid goal_kind and_goal
+      (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
+    trace (str "Started and proof");
+    Pfedit.by and_tac;
+    trace (str "Applied and tac")
+      
+
+let destruct_ex ext ex = 
+  let rec aux c acc = 
+    match kind_of_term c with
+	App (f, args) ->
+	  (match kind_of_term f with
+	       Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
+		 let (dom, rng) = 
+		   try (args.(0), args.(1))
+		   with _ -> assert(false)
+		 in
+		   (mk_ex_pi1 dom rng acc) :: aux rng (mk_ex_pi2 dom rng acc)
+	     | _ -> [acc])
+      | _ -> [acc]
+  in aux ex ext
+
+
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 84001c3740..a53016484b 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -8,6 +8,8 @@ open Decl_kinds
 open Topconstr
 open Rawterm
 open Util
+open Evarutil
+open Names
 
 val contrib_name : string
 val subtac_dir : string list
@@ -36,15 +38,22 @@ val natind : constr lazy_t
 val intind : constr lazy_t
 val existSind : constr lazy_t
 val existS : coq_sigma_data lazy_t
+val prod : coq_sigma_data lazy_t
+
 val well_founded : constr lazy_t
 val fix : constr lazy_t
+val acc : constr lazy_t
+val acc_inv : constr lazy_t
 val extconstr : constr -> constr_expr
 val extsort : sorts -> constr_expr
 val my_print_constr : env -> constr -> std_ppcmds
+val my_print_evardefs : evar_defs -> std_ppcmds
 val my_print_context : env -> std_ppcmds
 val my_print_env : env -> std_ppcmds
 val my_print_rawconstr : env -> rawconstr -> std_ppcmds
-val debug_level : int ref
+val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
+
+
 val debug : int -> std_ppcmds -> unit
 val debug_msg : int -> std_ppcmds -> std_ppcmds
 val trace : std_ppcmds -> unit
@@ -61,3 +70,15 @@ val global_kind : logical_kind
 val goal_kind : locality_flag * goal_object_kind
 val global_fix_kind : logical_kind
 val goal_fix_kind : locality_flag * goal_object_kind
+
+val mkSubset : name -> constr -> constr -> constr
+val mkProj1 : constr -> constr -> constr -> constr
+val mkProj1 : constr -> constr -> constr -> constr
+val mk_ex_pi1 : constr -> constr -> constr -> constr
+val mk_ex_pi1 : constr -> constr -> constr -> constr
+
+val build_dependent_sum : (identifier * types) list -> constr * Proof_type.tactic * types
+val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->  
+  ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
+
+val destruct_ex : constr -> constr -> constr list
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 39a12a7ea7..871a7f15cb 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -214,7 +214,6 @@ let theory_filename xml_library_root =
     None -> None  (* stdout *)
   | Some xml_library_root' ->
      let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
-     let hd = List.hd toks in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")