Julien:

+ Recursive definition (repository contrib/recdef) can now be used with GenFixpoint syntax by just replacing the usual  {struct x} annotation by {wf R x} where x is one of the function declared arguments and R is a expression well-typed in the x typing environment.
+ Bug correction in new functional induction
+ For now no induction principle for general recursive definition is generated.


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

8 files changed, 952 insertions, 416 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 5f5bcb3f43..c02c83c3a1 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -7,7 +7,9 @@ open Indfun_common
 open Libnames
 open Rawterm
 
-type annot = identifier 
+type annot = 
+    Struct of identifier 
+  | Wf of Topconstr.constr_expr * identifier 
 
 
 type newfixpoint_expr =
@@ -95,7 +97,7 @@ let register is_rec fixpoint_exprl =
 	Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
 	
 
-let generate_correction_proof_struct is_rec ind_kn mut_ind newfixpoint_exprl =
+let generate_correction_proof_struct  ind_kn  newfixpoint_exprl =
   let fname_kn (fname,_,_,_,_) =
     let f_ref = Ident (dummy_loc,fname) in
     locate_with_msg
@@ -120,66 +122,217 @@ let generate_correction_proof_struct is_rec ind_kn mut_ind newfixpoint_exprl =
        newfixpoint_exprl
     );
     ()
-
-let do_generate_principle fix_rec_l = 
-  let compute_annot (name,annot,args,types,body) =
-    let names = List.map snd (Topconstr.names_of_local_assums args) in
-    match annot with
-      | None ->
-          if List.length names > 1 then
+ 
+let compute_annot (name,annot,args,types,body) =
+  let names = List.map snd (Topconstr.names_of_local_assums args) in
+  match annot with
+    | None ->
+        if List.length names > 1 then
             user_err_loc
               (dummy_loc,"GenFixpoint",
                Pp.str "the recursive argument needs to be specified");
-          let new_annot = (id_of_name (List.hd names)) in 
-	  (name,new_annot,args,types,body)
-      | Some r -> (name,r,args,types,body)
+        let new_annot = (id_of_name (List.hd names)) in
+	(name,Struct new_annot,args,types,body)
+    | Some r -> (name,r,args,types,body)
+
+
+
+let rec is_rec names = 
+  let names = List.fold_right Idset.add names Idset.empty in 
+  let check_id id =  Idset.mem id names in 
+  let rec lookup = function 
+    | RVar(_,id) -> check_id id
+    | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
+    | RCast(_,b,_,_) -> lookup b
+    | RRec _ -> assert false 
+    | RIf _ -> failwith "Rif not implemented"
+    | RLetTuple _ -> failwith "RLetTuple not implemented"
+    | RLetIn(_,_,t,b) | RLambda(_,_,t,b) | RProd(_,_,t,b) -> 
+	lookup t || lookup b
+    | RApp(_,f,args) -> List.exists lookup (f::args)
+    | RCases(_,_,el,brl) -> 
+	List.exists (fun (e,_) -> lookup e) el ||
+	  List.exists (fun (_,_,_,ret)-> lookup ret) brl
   in
-  let newfixpoint_exprl = List.map compute_annot fix_rec_l in 
-  let prepare_body (name,annot,args,types,body) rt = 
-    let fun_args,rt' = chop_rlambda_n (Topconstr.local_binders_length args) rt in 
-    (name,annot,args,types,body,fun_args,rt')
+  lookup 
+
+    
+let register_struct is_rec fixpoint_exprl = 
+  match fixpoint_exprl with 
+    | [(fname,_,bl,ret_type,body),_] when not is_rec -> 
+	Command.declare_definition
+	  fname
+	  (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition)
+	  bl
+	  None
+  	  body
+	  (Some ret_type)
+	  (fun _ _ -> ())
+    | _ -> 
+	Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
+
+let register_wf fname wf_rel_expr wf_arg args ret_type body =  
+  let type_of_f = Command.generalize_constr_expr ret_type args in 
+  let rec_arg_num = 
+    let names = 
+      List.map
+	snd
+	(Topconstr.names_of_local_assums args) 
+    in 
+    Util.list_index (Name wf_arg) names 
   in
-  match build_newrecursive newfixpoint_exprl with 
-    | [] -> assert false
-    | l ->
-	let l' = List.map2 prepare_body newfixpoint_exprl l in 
-	let names = List.map (function (name,_,_,_,_,_,_) -> name) l' in 
-	let funs_args = List.map (function (_,_,_,_,_,fun_args,_) -> fun_args) l' in 
-	let funs_types =  List.map (function (_,_,_,types,_,_,_) -> types) l' in 
-(* 	let t1 = Sys.time () in  *)
-	Rawterm_to_relation.build_inductive names funs_args funs_types l;
-(* 	let t2 = Sys.time () in  *)
-(* 	Pp.msgnl (str "Time to compute graph" ++ str (string_of_float (t2 -. t1))); *)
-	let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
-	let ind =
-	  locate_with_msg
-	    (pr_reference f_R_mut++str ": Not an inductive type!")
-	    locate_ind
-	    f_R_mut
-	in
-	let mut_ind,_ = Global.lookup_inductive ind in
-	let is_rec = 
-	  List.exists (is_rec names) l
-	in
-(* 	msgnl (str "Inductives registered ... "); *)
-	let fixpoint_exprl : (Topconstr.fixpoint_expr*'a) list =
-	  List.map
-	    (fun (fname,annot,args,types,body) ->
-	       let names = List.map snd (Topconstr.names_of_local_assums args) in
-	       let annot =
-		 match annot with
-		   |  id ->
-			Util.list_index (Name id) names - 1
+  let unbounded_eq = 
+    let f_app_args = 
+      Topconstr.CApp 
+	(dummy_loc, 
+	 (None,Topconstr.mkIdentC fname) ,
+	 (List.map 
+	    (function
+	       | _,Anonymous -> assert false 
+	       | _,Name e -> (Topconstr.mkIdentC e,None)
+	    ) 
+	    (Topconstr.names_of_local_assums args)
+	 )
+	) 
+    in
+    Topconstr.CApp (dummy_loc,(None,Topconstr.mkIdentC (id_of_string "eq")),
+		    [(f_app_args,None);(body,None)])
+  in
+  let eq = Command.generalize_constr_expr unbounded_eq args in 
+  Recdef.recursive_definition fname type_of_f wf_rel_expr rec_arg_num eq
+    
+
+
+let register (fixpoint_exprl :  newfixpoint_expr list) = 
+  let recdefs = build_newrecursive fixpoint_exprl in 
+  let is_struct = 
+    match fixpoint_exprl with 
+      | [((name,Wf (wf_rel,wf_x),args,types,body))] -> 
+	  register_wf name wf_rel wf_x args types body;
+	  false
+      | _ -> 
+	  
+	  let old_fixpoint_exprl =  
+	    List.map 
+	      (function
+		 | (name,Struct id,args,types,body) -> 
+		     let names = 
+		       List.map
+			 snd
+			 (Topconstr.names_of_local_assums args) 
+		     in 
+		     let annot = Util.list_index (Name id) names - 1 in 
+ 		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
+		 | (_,Wf _,_,_,_) -> 
+		     error 
+		       ("Cannot use mutual definition with well-founded recursion")
+	      ) 
+	      fixpoint_exprl 
+	  in
+	  (* ok all the expressions are structural *) 
+	  let fix_names = 
+	    List.map (function (name,_,_,_,_) -> name) fixpoint_exprl 
+	  in
+	  let is_rec = List.exists (is_rec fix_names) recdefs in
+	  register_struct is_rec old_fixpoint_exprl;
+	  true
+						 
+  in
+  recdefs,is_struct
+
+let prepare_body (name,annot,args,types,body) rt = 
+  let fun_args,rt' = chop_rlambda_n (Topconstr.local_binders_length args) rt in
+  (fun_args,rt')
+
+let do_generate_principle fix_rec_l = 
+  (* we first of all checks whether on not all the correct 
+     assumption  are here 
+  *)
+  let newfixpoint_exprl = List.map compute_annot fix_rec_l in 
+  (* we can then register the functions *) 
+  let recdefs,is_struct = register newfixpoint_exprl in 
+(*   Pp.msgnl (str "Fixpoint(s) registered"); *)
+  let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
+  let fun_bodies = List.map2 prepare_body newfixpoint_exprl recdefs in
+  let funs_args = List.map fst fun_bodies in
+  let funs_types =  List.map (function (_,_,_,types,_) -> types) fix_rec_l in
+  try 
+    (* We then register the Inductive graphs of the functions  *)
+    Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
+    let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
+    let ind =
+      locate_with_msg
+	(pr_reference f_R_mut++str ": Not an inductive type!")
+	locate_ind
+	f_R_mut
+    in
+    (*   let mut_ind,_ = Global.lookup_inductive ind in *)
+    if is_struct 
+    then
+      generate_correction_proof_struct (fst ind)  newfixpoint_exprl
+  with _ -> () 
+;;
+
+
+(* let do_generate_principle fix_rec_l = *)
+(*   let compute_annot (name,annot,args,types,body) = *)
+(*     let names = List.map snd (Topconstr.names_of_local_assums args) in *)
+(*     match annot with *)
+(*       | None -> *)
+(*           if List.length names > 1 then *)
+(*             user_err_loc *)
+(*               (dummy_loc,"GenFixpoint", *)
+(*                Pp.str "the recursive argument needs to be specified"); *)
+(*           let new_annot = (id_of_name (List.hd names)) in *)
+(* 	  (name,new_annot,args,types,body) *)
+(*       | Some r -> (name,r,args,types,body) *)
+(*   in *)
+(*   let newfixpoint_exprl = List.map compute_annot fix_rec_l in *)
+(*   let prepare_body (name,annot,args,types,body) rt = *)
+(*     let fun_args,rt' = chop_rlambda_n (Topconstr.local_binders_length args) rt in *)
+(*     (name,annot,args,types,body,fun_args,rt') *)
+(*   in *)
+(*   match build_newrecursive newfixpoint_exprl with *)
+(*     | [] -> assert false *)
+(*     | l -> *)
+(* 	let l' = List.map2 prepare_body newfixpoint_exprl l in *)
+(* 	let names = List.map (function (name,_,_,_,_,_,_) -> name) l' in *)
+(* 	let funs_args = List.map (function (_,_,_,_,_,fun_args,_) -> fun_args) l' in *)
+(* 	let funs_types =  List.map (function (_,_,_,types,_,_,_) -> types) l' in *)
+(* (\* 	let t1 = Sys.time () in  *\) *)
+(* 	Rawterm_to_relation.build_inductive names funs_args funs_types l; *)
+(* (\* 	let t2 = Sys.time () in  *\) *)
+(* (\* 	Pp.msgnl (str "Time to compute graph" ++ str (string_of_float (t2 -. t1))); *\) *)
+(* 	let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in *)
+(* 	let ind = *)
+(* 	  locate_with_msg *)
+(* 	    (pr_reference f_R_mut++str ": Not an inductive type!") *)
+(* 	    locate_ind *)
+(* 	    f_R_mut *)
+(* 	in *)
+(* 	let mut_ind,_ = Global.lookup_inductive ind in *)
+(* 	let is_rec = *)
+(* 	  List.exists (is_rec names) l *)
+(* 	in *)
+(* (\* 	msgnl (str "Inductives registered ... "); *\) *)
+(* 	let fixpoint_exprl : (Topconstr.fixpoint_expr*'a) list = *)
+(* 	  List.map *)
+(* 	    (fun (fname,annot,args,types,body) -> *)
+(* 	       let names = List.map snd (Topconstr.names_of_local_assums args) in *)
+(* 	       let annot = *)
+(* 		 match annot with *)
+(* 		   |  id -> *)
+(* 			Util.list_index (Name id) names - 1 *)
 			  
-	       in
-	       (fname,annot,args,types,body),(None:Vernacexpr.decl_notation)
-	    )
-	    newfixpoint_exprl
-	in
-	register is_rec fixpoint_exprl;
-
-	generate_correction_proof_struct
-	  is_rec
-	  (fst ind)
-	  mut_ind
-	  newfixpoint_exprl
+(* 	       in *)
+(* 	       (fname,annot,args,types,body),(None:Vernacexpr.decl_notation) *)
+(* 	    ) *)
+(* 	    newfixpoint_exprl *)
+(* 	in *)
+(* 	register is_rec fixpoint_exprl; *)
+
+(* 	generate_correction_proof_struct *)
+(* 	  is_rec *)
+(* 	  (fst ind) *)
+(* 	  mut_ind *)
+(* 	  newfixpoint_exprl *)
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 19c68d4834..3969623006 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -156,3 +156,158 @@ let find_reference sl s =
 let eq = lazy(coq_constant "eq")
 let refl_equal = lazy(coq_constant "refl_equal")
 
+
+(************************************************) 
+(* Should be removed latter                     *)
+(* Comes from new induction  (cf Pierre)        *)
+(************************************************) 
+
+open Sign
+open Term
+
+type elim_scheme = { (* lists are in reverse order! *)
+  params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  branches: rel_context;    (* branchr,...,branch1 *)
+  args: rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
+  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) if present, None otherwise *)
+  concl: types;            (* Qi x1...xni HI, some prmis may not be present *)
+  indarg_in_concl:bool;    (* true if HI appears at the end of conclusion (dependent scheme) *)
+}
+
+
+
+let occur_rel n c = 
+  let res = not (noccurn n c) in
+  res
+
+let list_filter_firsts f l =
+  let rec list_filter_firsts_aux f acc l =
+    match l with
+      | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l'
+      | _ -> acc,l
+  in
+  list_filter_firsts_aux f [] l
+
+let count_rels_from n c =
+  let rels = Termops.free_rels c in
+  let cpt,rg = ref 0, ref n in
+  while Util.Intset.mem !rg rels do
+    cpt:= !cpt+1; rg:= !rg+1;
+  done;
+  !cpt
+
+let count_nonfree_rels_from n c =
+  let rels = Termops.free_rels c in
+  if Util.Intset.exists (fun x -> x >= n) rels then
+    let cpt,rg = ref 0, ref n in
+    while not (Util.Intset.mem !rg rels) do
+      cpt:= !cpt+1; rg:= !rg+1;
+    done;
+    !cpt
+  else raise Not_found
+
+(* cuts a list in two parts, first of size n. Size must be greater than n *)
+let cut_list n l =
+  let rec cut_list_aux acc n l =
+    if n<=0 then acc,l
+    else match l with
+      | [] -> assert false
+      | e::l' -> cut_list_aux (acc@[e]) (n-1) l' in
+  let res = cut_list_aux [] n l in
+  res
+
+let exchange_hd_prod subst_hd t =
+  let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args)
+
+let compute_elim_sig elimt  =
+  (* conclusion is the final (Qi ...) *)
+  let hyps,conclusion = decompose_prod_assum elimt in
+  (* ccl is conclusion where Qi (that is rel <something>) is replaced
+     by a constant (Prop) to avoid it being counted as an arg or
+parameter in the following. *)
+  let ccl = exchange_hd_prod mkProp conclusion in
+  (* indarg is the inductive argument if it exists. If it exists it is
+the last hyp before the conclusion, so it is the first element of
+     hyps. To know the first elmt is an inductive arg, we check if the
+     it appears in the conclusion (as rel 1). If yes, then it is not
+     an inductive arg, otherwise it is. There is a pathological case
+     with False_inf where Qi is rel 1, so we first get rid of Qi in
+     ccl. *)
+  (* if last arg of ccl is an application then this a functional ind
+principle *) let last_arg_ccl = 
+    try List.hd (List.rev (snd (decompose_app ccl))) 
+    with Failure "hd" -> mkProp in (* dummy constr that is not an app
+*) let hyps',indarg,dep = 
+    if isApp last_arg_ccl 
+    then 
+      hyps,None , false (* no HI at all *)
+    else 
+      try 
+	if noccurn 1 ccl (* rel 1 does not occur in ccl *)
+	then
+	  List.tl hyps , Some (List.hd hyps), false (* it does not
+occur in concl *) else
+	  List.tl hyps , Some (List.hd hyps) , true (* it does occur in concl *) 
+      with Failure s -> Util.error "cannot recognise an induction schema"
+  in
+
+  (* Arguments [xni...x1] must appear in the conclusion, so we count
+     successive rels appearing in conclusion **Qi is not considered a
+rel** *) let nargs = count_rels_from 
+    (match indarg with
+      | None -> 1
+      | Some _ -> 2) ccl in
+  let args,hyps'' = cut_list nargs hyps' in
+  let rel_is_pred (_,_,c) = isSort (snd(decompose_prod_assum c)) in
+  let branches,hyps''' = 
+    list_filter_firsts (function x -> not (rel_is_pred x)) hyps''
+  in
+  (* Now we want to know which hyps remaining are predicates and which
+     are parameters *)
+  (* We rebuild 
+     
+     forall (x1:Ti_1) (xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY
+x1...xni HI ^^^^^^^^^^^^^^^^^^^^^^^^^                  ^^
+                                          optional
+opt
+
+     Free rels appearing in this term are parameters. We catch all of
+     them if HI is present. In this case the number of parameters is
+     the number of free rels. Otherwise (principle generated by
+     functional induction or by hand) WE GUESS that all parameters
+     appear in Ti_js, IS THAT TRUE??.
+
+     TODO: if we want to generalize to the case where arges are merged
+     with branches (?) and/or where several predicates are cited in
+     the conclusion, we should do something more precise than just
+     counting free rels.
+ *)
+  let concl_with_indarg = 
+    match indarg with
+    | None -> ccl
+    | Some c -> it_mkProd_or_LetIn ccl [c] in
+  let concl_with_args = it_mkProd_or_LetIn concl_with_indarg args in
+(*   let nparams2 = Util.Intset.cardinal (Termops.free_rels concl_with_args) in *)
+  let nparams = 
+    try List.length (hyps'''@branches) - count_nonfree_rels_from 1
+      concl_with_args with Not_found -> 0 in
+  let preds,params = cut_list (List.length hyps''' - nparams) hyps''' in
+  let elimscheme = {
+    params = params;
+    predicates = preds;
+    branches = branches;
+    args = args;
+    indarg = indarg;
+    concl = conclusion;
+    indarg_in_concl = dep;
+  }
+  in
+  elimscheme
+
+let get_params elimt = 
+  (compute_elim_sig elimt).params
+(************************************************) 
+(* end of Should be removed latter              *)
+(* Comes from new induction  (cf Pierre)        *)
+(************************************************) 
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 639063faf6..c784dd5dde 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -37,3 +37,17 @@ val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
 val refl_equal : Term.constr Lazy.t
 val const_of_id: identifier -> constant
+
+
+type elim_scheme = { (* lists are in reverse order! *)
+  params: Sign.rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  predicates: Sign.rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  branches: Sign.rel_context;    (* branchr,...,branch1 *)
+  args: Sign.rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
+  indarg: Term.rel_declaration option; (* Some (H,I prm1..prmp x1...xni) if present, None otherwise *)
+  concl: Term.types;            (* Qi x1...xni HI, some prmis may not be present *)
+  indarg_in_concl:bool;    (* true if HI appears at the end of conclusion (dependent scheme) *)
+}
+
+
+val compute_elim_sig : Term.types ->  elim_scheme
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index ec417411a5..55f67b5b8a 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -33,9 +33,7 @@ open G_vernac
 open Indfun
 open Topconstr
 
-open Tacinterp;;
-
-let _ = ref 0;;
+open Tacinterp
 
 
 TACTIC EXTEND newfuninv
@@ -59,21 +57,41 @@ TACTIC EXTEND newfunind
        let princ_name = 
 	   (
 	     Indrec.make_elimination_ident
-	       ( id_of_string ((string_of_id fname)^"_2"))
+	       fname
 	       (Tacticals.elimination_sort_of_goal g)
 	   )
        in
-       let princ = 
-	 let _,princ_ref = 
-	   qualid_of_reference (Libnames.Ident (Util.dummy_loc,princ_name))
+       let princ = const_of_id princ_name in
+       let princ_info = 
+	 let princ_type = 
+	(try (match (Global.lookup_constant princ) with
+		  {Declarations.const_type=t} -> t
+	     )
+	 with _ -> assert false)
 	 in
-	 try Nametab.locate_constant princ_ref
-	 with Not_found -> Util.error "Don't know the induction scheme to use"
+	 compute_elim_sig princ_type
+       in
+       let frealargs = 
+	 try
+	   snd (Util.list_chop (List.length princ_info.params) args)
+	 with _ -> 
+	   msg_warning
+	     (str "computing non parameters argument for " ++
+		Ppconstr.pr_id princ_name ++ fnl () ++
+		str " detected params number is : " ++
+		str (string_of_int (List.length princ_info.params)) ++ fnl ()++
+		str  " while number of arguments is " ++
+		str (string_of_int (List.length args)) ++ fnl () 
+(* 		str " number of predicates " ++  *)
+(* 		str (string_of_int (List.length princ_info.predicates))++ fnl () ++ *)
+(* 		str " number of branches " ++  *)
+(* 		str (string_of_int (List.length princ_info.branches)) *)
+	     );args
+	     
        in
-       
        Tacticals.tclTHEN 
 	 (Hiddentac.h_reduce 
-	    (Rawterm.Pattern (List.map (fun e -> ([],e)) (args@[c])))
+	    (Rawterm.Pattern (List.map (fun e -> ([],e)) (frealargs@[c])))
 	    Tacticals.onConcl
 	 )
 	 ((Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings)))
@@ -82,7 +100,8 @@ TACTIC EXTEND newfunind
 END
 
 VERNAC ARGUMENT EXTEND rec_annotation2
-  [ "{"  "struct" ident(id)  "}"] -> [ id ]
+  [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
+| [ "{" "wf" constr(r) ident(id) "}" ] -> [ Wf(r,id) ]
 END
 
 
@@ -104,7 +123,8 @@ VERNAC ARGUMENT EXTEND rec_definition2
                  (Util.dummy_loc,"GenFixpoint",
                   Pp.str "the recursive argument needs to be specified");
 	   in
-	   let check_exists_args id =
+	   let check_exists_args an =
+	     let id = match an with Struct id -> id | Wf(_,id) -> id in 
 	     (try ignore(Util.list_index (Name id) names - 1); annot
 	      with Not_found ->  Util.user_err_loc
                 (Util.dummy_loc,"GenFixpoint",
@@ -117,7 +137,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
 		  check_one_name ();
                   annot
 	      | Some an ->
-			check_exists_args an
+		  check_exists_args an
 	  in
 	  (id, ni, bl, type_, def) ]
 END
@@ -133,4 +153,20 @@ VERNAC COMMAND EXTEND GenFixpoint
    ["GenFixpoint" rec_definitions2(recsl)] ->
 	[ do_generate_principle recsl]
       END
-
+(*
+
+VERNAC COMMAND EXTEND RecursiveDefinition
+  [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
+     constr(proof) integer_opt(rec_arg_num) constr(eq) ] ->
+  [ ignore(proof);ignore(wf);
+    let rec_arg_num = 
+      match rec_arg_num with 
+	| None -> 1
+	| Some n -> n 
+    in
+    recursive_definition f type_of_f r rec_arg_num eq ]
+| [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
+     "[" ne_constr_list(proof) "]" constr(eq) ] ->
+  [ ignore(proof);ignore(wf);recursive_definition f type_of_f r 1 eq ]
+END
+*)
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 963621bf71..a8429d3c47 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -1,13 +1,14 @@
 open Util
 open Names
 open Term
-
+open Tacinvutils
 open Pp
 open Indfun_common
 open Libnames
 open Tacticals
 open Tactics
 open Tacmach
+open Sign
 
 
 let tac_pattern l =
@@ -36,7 +37,7 @@ let intro_discr_until n tac : tactic =
 	(fun g' ->
 	  let id,_,t = pf_last_hyp g' in
 	  tclORELSE
-	     (Extratactics.h_discrHyp (Rawterm.NamedHyp id))
+	     (tclABSTRACT None (Extratactics.h_discrHyp (Rawterm.NamedHyp id)))
 	    (intro_discr_until ((id,t)::acc))
 	    g'
 	) 
@@ -47,7 +48,7 @@ let intro_discr_until n tac : tactic =
 
 let rec discr_rew_in_H hypname idl : tactic =
   match idl with 
-    | [] -> Extratactics.h_discrHyp (Rawterm.NamedHyp hypname)
+    | [] -> (Extratactics.h_discrHyp (Rawterm.NamedHyp hypname))
     | ((id,t)::idl') ->
        match kind_of_term t with 
 	 | App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) -> 
@@ -64,69 +65,27 @@ let rec discr_rew_in_H hypname idl : tactic =
 	 | _ -> discr_rew_in_H hypname idl'
 
 let finalize fname hypname idl : tactic = 
-  tclTRY 
+  tclTRY (
     (tclTHEN 
       (Hiddentac.h_reduce
 	(Rawterm.Unfold [[],EvalConstRef fname])
 	(Tacticals.onHyp hypname)
       )
       (discr_rew_in_H hypname idl)
-    )
-      
+    ))
 
-let invfun (hypname:identifier) (fid:identifier) : tactic=
+let gen_fargs fargs : tactic = 
   fun g -> 
-    let nprod_goal = nb_prod (pf_concl g) in
-    let f_ind_id =  
-      (
-	Indrec.make_elimination_ident
-	  ( id_of_string ((string_of_id fid)^"_2"))
-	  (Tacticals.elimination_sort_of_goal g)
-      )
-    in
-    let fname = const_of_id fid in
-    let princ = const_of_id f_ind_id in
-    let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
-    match kind_of_term typhyp with
-      | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) -> 
-(* 	  let valf = def_of_const (mkConst fname) in *)
-	  let eq_arg1 , eq_arg2 , tac, fargs = 
-	    match kind_of_term arg1 , kind_of_term arg2 with
-	      | App(f, args),_ when eq_constr f (mkConst fname) -> 
-		  arg1 , arg2 , tclIDTAC , args
-	      | _,App(f, args) when eq_constr f (mkConst fname) -> 
-		  arg2 , arg1 , symmetry_in hypname , args
-	      | _ , _  -> error "inversion impossible" 
-	  in
-	  let gen_fargs : tactic = 
-	    fun g -> 
-	      generalize
-		(List.map
-		  (fun arg -> 
-		    let targ = pf_type_of g arg in
-		    let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
-		    refl_arg
-		  )
-		  (Array.to_list fargs)
-		) g 
-	  in
-	  let pat_args = 
-	    (List.map (fun e -> ([-1],e)) (Array.to_list fargs)) @ [[],eq_arg1] in
-	 
-  	  tclTHENSEQ 
-	    [
-	    tac;
-	    gen_fargs;
-	    tac_pattern pat_args;
-	    Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
-	    intro_discr_until nprod_goal (finalize fname hypname) 
-	      
-	    ]
-	    g
-
-
-      | _ -> error "inversion impossible"
-
+    generalize
+      (List.map
+	 (fun arg -> 
+	    let targ = pf_type_of g arg in
+	    let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
+	    refl_arg
+	 )
+	 (Array.to_list fargs)
+      ) 
+      g 
       
 
 let invfun (hypname:identifier) (fid:identifier) : tactic=
@@ -135,17 +94,41 @@ let invfun (hypname:identifier) (fid:identifier) : tactic=
     let f_ind_id =  
       (
 	Indrec.make_elimination_ident
-	  ( id_of_string ((string_of_id fid)^"_2"))
+	  fid 
 	  (Tacticals.elimination_sort_of_goal g)
       )
     in
     let fname = const_of_id fid in
     let princ = const_of_id f_ind_id in
+    let princ_info = 
+      let princ_type = 
+	(try (match (Global.lookup_constant princ) with
+		  {Declarations.const_type=t} -> t
+	     )
+	 with _ -> assert false)
+      in
+      compute_elim_sig princ_type
+    in
     let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
+    let do_invert  fargs  appf : tactic = 
+      let frealargs = (snd (array_chop (List.length princ_info.params) fargs))  
+      in
+      let pat_args = 
+	(List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf] 
+      in
+      tclTHENSEQ 
+	[
+	  gen_fargs frealargs;
+	  tac_pattern pat_args;
+	  Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
+	  intro_discr_until nprod_goal (finalize fname hypname) 
+	    
+	]
+    in
     match kind_of_term typhyp with
       | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) -> 
 (* 	  let valf = def_of_const (mkConst fname) in *)
-	  let eq_arg1 , eq_arg2 , tac, fargs = 
+	  let eq_arg1 , eq_arg2 , good_eq_form , fargs = 
 	    match kind_of_term arg1 , kind_of_term arg2 with
 	      | App(f, args),_ when eq_constr f (mkConst fname) -> 
 		  arg1 , arg2 , tclIDTAC , args
@@ -153,32 +136,13 @@ let invfun (hypname:identifier) (fid:identifier) : tactic=
 		  arg2 , arg1 , symmetry_in hypname , args
 	      | _ , _  -> error "inversion impossible" 
 	  in
-	  let gen_fargs : tactic = 
-	    fun g -> 
-	      generalize
-		(List.map
-		  (fun arg -> 
-		    let targ = pf_type_of g arg in
-		    let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
-		    refl_arg
-		  )
-		  (Array.to_list fargs)
-		) g 
-	  in
-	  let pat_args = 
-	    (List.map (fun e -> ([-1],e)) (Array.to_list fargs)) @ [[],eq_arg1] in
-	 
-  	  tclTHENSEQ 
-	    [
-	    tac;
-	    gen_fargs;
-	    tac_pattern pat_args;
-	    Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
-	    intro_discr_until nprod_goal (finalize fname hypname) 
-	      
-	    ]
+	  tclTHEN
+	    good_eq_form
+	    (do_invert fargs eq_arg1)
 	    g
-
+      | App(f',fargs) when eq_constr f' (mkConst fname) -> 
+	  do_invert fargs typhyp g
+	  
 
       | _ -> error "inversion impossible"
 
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
index f0106d91fb..a33f0f6c54 100644
--- a/contrib/funind/new_arg_principle.ml
+++ b/contrib/funind/new_arg_principle.ml
@@ -185,9 +185,6 @@ let compute_new_princ_type_from_rel with_concl replace
 	    compute_new_princ_type_for_letin env x v t b
 	| _ -> pre_princ,[]
     in 
-(*     let _tim2 = Sys.time() in *)
-
-
 (*     if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
 (*     then *)
 (*       msgnl (str "compute_new_princ_type for "++ *)
@@ -333,16 +330,7 @@ let exactify_proof rec_pos ptes_to_fix : tactic =
   let eq_or = eq_constr or_as_ind in
   let tac_res tac: tactic = 
     fun g -> 
-(*       let concl = pf_concl g in  *)
-(*       if eq_constr concl (Coqlib.build_coq_True ())  *)
-(*       then exact_no_check (Coqlib.build_coq_I ()) g *)
-(*       else *)
       match kind_of_term (pf_concl g) with
-(* 	| LetIn _ | Case _ ->  *)
-(* 	    tclTHEN    *)
-(* 	      (tclPROGRESS (h_reduce (Rawterm.Simpl None) onConcl)) *)
-(* 	      tac *)
-(* 	      g *)
 	| Prod _ -> tclTHEN intro tac g
 	| App(f,_) -> 
 	    if eq_not f 
@@ -385,7 +373,7 @@ let exactify_proof rec_pos ptes_to_fix : tactic =
   let rec exactify_proof g = 
     tclFIRST
       [
-	tclSOLVE [my_reflexivity(* Tactics.reflexivity *)];
+	tclSOLVE [my_reflexivity];
 	tclSOLVE [Eauto.e_assumption];
 	tclSOLVE [Tactics.reflexivity ];
 	tac_res exactify_proof
@@ -486,10 +474,6 @@ let finalize_proof rec_pos fixes (hyps:identifier list) =
 		tclTHENS
 		  (try Equality.replace (args.(nargs -1)) t
 		   with _ ->
-(* 		     Pp.msgnl (str "Cannot replace " ++ *)
-(* 				 pr_lconstr_env (pf_env g) args.(nargs - 1) ++ *)
-(* 				 str " with " ++ pr_lconstr_env (pf_env g) t *)
-(* 			      ); *)
 		     tclFAIL 0 (str "")
 		  )
 		[tac;
@@ -517,7 +501,6 @@ let do_prove_princ_for_struct
     finalize_proof rec_pos fixes hyps with_concl fnames term
   in
   let rec do_prove_princ_for_struct do_finalize term g =
-(*     Pp.msgnl (str "Proving with body : " ++ pr_lconstr_env (pf_env g) term); *)
 (*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
 (*      then msgnl (str "Proving with body : " ++ pr_lconstr_env (pf_env g) term); *)
     let tac = 
@@ -618,7 +601,6 @@ let prove_princ_for_struct with_concl f_names fun_num nparams : tactic =
 	  begin Some (idxs.(fix_num) - nparams),substl (List.rev fnames_as_constr) ca.(fix_num) end
       | b -> None,fbody
   in
-(*   msgnl (str "fbody : " ++ Printer.pr_lconstr fbody); *)
   let f_real_args = nb_lam fbody - nparams in
   let test_goal_for_hyps g = 
     let goal_nb_prod = nb_prod (pf_concl g) in 
@@ -626,7 +608,7 @@ let prove_princ_for_struct with_concl f_names fun_num nparams : tactic =
   in
   let test_goal_for_args g = 
     let goal_nb_prod = nb_prod (pf_concl g) in 
-    (with_concl && goal_nb_prod <= 1)||
+    (with_concl && goal_nb_prod < 1 )||
       ((not with_concl) && goal_nb_prod = 0 )
   in
   let rec intro_params tac params n : tactic =  
@@ -719,8 +701,8 @@ let prove_princ_for_struct with_concl f_names fun_num nparams : tactic =
 (* 			  msgnl (str "introducing args"); *)
 			  intro_args
 			    (fun args ->  
-			       tclTHEN 
-				 (reduce_fname (Array.to_list f_names))
+(* 			       tclTHEN  *)
+(* 				 (reduce_fname (Array.to_list f_names)) *)
 				 (tac params ptes ptes_to_fix hyps args))
 			    []
 		       )
@@ -748,10 +730,41 @@ let prove_princ_for_struct with_concl f_names fun_num nparams : tactic =
       (fun  params ptes ptes_to_fix hyps args g -> 
 	 let app_f = apply_fbody g params args in 
 (* 	 msgnl (str "proving"); *)
-	 tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f g
+	 match rec_arg_num with 
+	     Some rec_arg_num -> 
+	       let actual_args = 
+		 List.fold_left (fun  y x -> x::y) 
+		   (List.rev args)
+		   params
+	       in
+	       let to_replace = applist(mkConst f_names.(fun_num),List.map mkVar actual_args) in 
+	       
+	       tclTHENS
+		 (Equality.replace 
+		    to_replace
+		    app_f
+		 )
+		 [
+		   tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f;
+		   let id = List.nth (List.rev args) (rec_arg_num ) in
+		   (tclTHENSEQ
+		      [(h_simplest_case (mkVar id));
+		       tclTRY Tactics.intros_reflexivity
+		      ]
+		   )
+(* 		     Tactics.reflexivity) *)
+		 ]
+		 g
+	   | None -> 
+	       tclTHEN
+		 (reduce_fname (Array.to_list f_names))
+		 (tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f)
+		 g
+
+(* 	 tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f g *)
       )
   in
-  prepare_goal_tac (fun g ->   (* Pp.msgnl (str "starting proof real .... "); *)do_prove_princ_for_struct rec_arg_num with_concl g) 
+  prepare_goal_tac (fun g -> do_prove_princ_for_struct rec_arg_num with_concl g) 
     
   
 
@@ -871,25 +884,17 @@ let generate_new_structural_principle
     match new_princ_name with 
       | Some (id) -> id
       | None -> 
-	  let id_of_f = 
-	    let id = id_of_label (con_label f) in 
-	    if with_concl 
-	    then id_of_string ((string_of_id id)^"_2") 
-	    else id 
-	  in
-	  Indrec.make_elimination_ident (id_of_f) (family_of_sort toSort)
+	  let id_of_f = id_of_label (con_label f) in
+	  Indrec.make_elimination_ident id_of_f (family_of_sort toSort)
   in
   let hook _ _  = 
-    let id_of_f = 
-      let id = id_of_label (con_label f) in 
-      if with_concl 
-      then id_of_string ((string_of_id id)^"_2") 
-      else id 
-    in
+    let id_of_f = id_of_label (con_label f) in
     let register_with_sort fam_sort = 
       let s = Termops.new_sort_in_family  fam_sort in 
       let name = Indrec.make_elimination_ident id_of_f fam_sort in 
-      let value = change_property_sort mutr_nparams s new_principle_type new_princ_name in 
+      let value = 
+	change_property_sort mutr_nparams s new_principle_type new_princ_name 
+      in 
       let ce = 
 	{ const_entry_body = value;
 	  const_entry_type = None;
@@ -907,7 +912,7 @@ let generate_new_structural_principle
     in
     register_with_sort InProp;
     register_with_sort InSet
-    in
+  in
   begin
     Command.start_proof 
       new_princ_name
@@ -941,3 +946,249 @@ let generate_new_structural_principle
 	      )
 
   end
+
+
+
+
+
+
+(*************************************************)
+let next_ident_away = Nameops.next_ident_away
+
+
+(* let base_leaf_eq eqs f_id g = *)
+(*   let ids = ids_of_named_context (pf_hyps g) in *)
+(*   let k = next_ident_away (id_of_string "k") ids in *)
+(*   let p = next_ident_away (id_of_string "p") (k::ids) in *)
+(*   let v = next_ident_away (id_of_string "v") (p::k::ids) in *)
+(*   let heq = next_ident_away (id_of_string "heq") (v::p::k::ids) in *)
+(*   let heq1 = next_ident_away (id_of_string "heq") (heq::v::p::k::ids) in *)
+(*   let hex = next_ident_away (id_of_string "hex") (heq1::heq::v::p::k::ids) in *)
+(*     tclTHENLIST [ *)
+(*       intros_using [v; hex]; *)
+(*       simplest_elim (mkVar hex); *)
+(*       intros_using [p;heq1]; *)
+(*       tclTRY *)
+(* 	(Equality.rewriteRL *)
+(* 	   (mkApp(mkVar heq1, *)
+(* 		  [|mkApp (Lazy.force Recdef.coq_S, [|mkVar p|]); *)
+(* 		    mkApp(Lazy.force Recdef.lt_n_Sn, [|mkVar p|]); f_id|]))); *)
+(*       Recdef.list_rewrite true eqs; *)
+(*       apply (Lazy.force refl_equal)] g;; *)
+
+(* let f_S t = mkApp(Lazy.force Recdef.coq_S, [|t|]);; *)
+
+(* let rec introduce_all_values_eq cont_tac f p heq1 pmax *)
+(*     bounds le_proofs eqs ids = *)
+(*   function *)
+(*       [] -> *)
+(* 	tclTHENLIST *)
+(* 	  [tclTHENS *)
+(* 	     (Equality.general_rewrite_bindings false *)
+(* 		(mkVar heq1, *)
+(* 		 Rawterm.ExplicitBindings[dummy_loc,Rawterm.NamedHyp (id_of_string "k"), *)
+(* 				  f_S(f_S(mkVar pmax)); *)
+(* 				  dummy_loc,Rawterm.NamedHyp (id_of_string "def"), *)
+(* 				  f])) *)
+(*    [tclTHENLIST *)
+(*    [Recdef.list_rewrite true eqs; cont_tac pmax le_proofs]; *)
+(*    tclTHENLIST[apply (Lazy.force Recdef.le_lt_SS); *)
+(* 			Recdef.compute_le_proofs le_proofs]]] *)
+(*     | arg::args -> *)
+(* 	let v' = next_ident_away (id_of_string "v") ids in *)
+(*         let ids = v'::ids in *)
+(* 	let hex' = next_ident_away Recdef.hex_id ids in *)
+(*         let ids = hex'::ids in *)
+(* 	let p' = next_ident_away Recdef.p_id ids in *)
+(*         let ids = p'::ids in *)
+(* 	let new_pmax = next_ident_away Recdef.pmax_id ids in *)
+(*         let ids = pmax::ids in *)
+(* 	let hle1 = next_ident_away Recdef.hle_id ids in *)
+(*         let ids = hle1::ids in *)
+(* 	let hle2 = next_ident_away Recdef.hle_id ids in *)
+(*         let ids = hle2::ids in *)
+(* 	let heq = next_ident_away Recdef.heq_id ids in *)
+(*         let ids = heq::ids in *)
+(* 	let heq2 = *)
+(* 	  next_ident_away Recdef.heq_id ids in *)
+(*         let ids = heq2::ids in *)
+(* 	tclTHENLIST *)
+(* 	  [Recdef.mkCaseEq(mkApp(termine, Array.of_list arg)); *)
+(* 	   intros_using [v'; hex']; *)
+(* 	   simplest_elim(mkVar hex'); *)
+(* 	   intros_using [p']; *)
+(* 	   simplest_elim(mkApp(Lazy.force max_constr, [|mkVar pmax; *)
+(* 							mkVar p'|])); *)
+(* 	   intros_using [new_pmax;hle1;hle2]; *)
+(*            introduce_all_values_eq *)
+(*               (fun pmax' le_proofs'-> *)
+(* 		tclTHENLIST *)
+(* 		  [cont_tac pmax' le_proofs'; *)
+(* 		   intros_using [heq;heq2]; *)
+(* 		   rewriteLR (mkVar heq2); *)
+(* 		   tclTHENS *)
+(* 		     (general_rewrite_bindings false *)
+(* 			(mkVar heq, *)
+(* 			 ExplicitBindings *)
+(* 			   [dummy_loc, NamedHyp k_id, *)
+(* 			    f_S(mkVar pmax'); *)
+(* 			    dummy_loc, NamedHyp def_id, f])) *)
+(* 		     [tclIDTAC; *)
+(* 		      tclTHENLIST *)
+(* 			[apply (Lazy.force le_lt_n_Sm); *)
+(* 			 compute_le_proofs le_proofs']]]) *)
+(* 	     functional termine f p heq1 new_pmax *)
+(* 	     (p'::bounds)((mkVar pmax)::le_proofs) eqs *)
+(*              (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args] *)
+  
+
+(* let rec_leaf_eq  f ids eqs expr fn args = *)
+(*   let p = next_ident_away (id_of_string "id") ids in *)
+(*   let ids = p::ids in *)
+(*   let v = next_ident_away (id_of_string "v") ids in *)
+(*   let ids = v::ids in *)
+(*   let hex = next_ident_away (id_of_string "hex") ids in *)
+(*   let ids = hex::ids in *)
+(*   let heq1 = next_ident_away (id_of_string "heq") ids in *)
+(*   let ids = heq1::ids in *)
+(*   let hle1 = next_ident_away (id_of_string "hle") ids in *)
+(*   let ids = hle1::ids in *)
+(*     tclTHENLIST *)
+(*       [intros_using [v;hex]; *)
+(*        simplest_elim (mkVar hex); *)
+(*        intros_using [p;heq1]; *)
+(*        generalize [mkApp(Lazy.force Recdef.le_n,[|mkVar p|])]; *)
+(*        intros_using [hle1]; *)
+(* (\*        introduce_all_values_eq (fun _ _ -> tclIDTAC) *\) *)
+(* (\* 	  f p heq1 p [] [] eqs ids args; *\) *)
+(* (\*        apply (Lazy.force refl_equal) *\)] *)
+
+open Libnames
+let rec nthtl = function
+    l, 0 -> l  | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];;
+let  mkCaseEq a =
+     (fun g ->
+(* commentaire de Yves: on pourra avoir des problemes si
+   a n'est pas bien type dans l'environnement du but *)
+       let type_of_a = pf_type_of g a in
+       (tclTHEN (generalize [mkApp(Lazy.force refl_equal, [| type_of_a; a|])])
+	  (tclTHEN 
+	     (fun g2 ->
+	       change_in_concl None 
+		 (Tacred.pattern_occs [([2], a)] (pf_env g2) Evd.empty (pf_concl g2))
+		 g2)
+	     (simplest_case a))) g);;
+
+let rec (find_call_occs:
+	   constr -> constr -> (constr list ->constr)*(constr  list list)) =
+ fun f expr ->
+  match (kind_of_term expr) with
+    App (g, args) when g = f -> 
+      (* For now we suppose that the function takes only one argument. *)
+      (fun l -> List.hd l), [Array.to_list args]
+  | App (g, args) ->
+     let (largs: constr list) = Array.to_list args in
+     let rec find_aux = function
+	 []    -> (fun x -> []), []
+       | a::tl ->
+         (match find_aux tl with
+          (cf, ((arg1::args) as opt_args)) -> 
+           (match find_call_occs f a with
+             cf2, (_ :: _ as other_args) ->
+	       let len1 = List.length other_args in
+                 (fun l ->
+                   cf2 l::(cf (nthtl(l,len1)))), other_args@opt_args
+           | _, [] -> (fun x -> a::cf x), opt_args)
+	 | _, [] ->
+	   (match find_call_occs f a with
+	     cf, (arg1::args) -> (fun l -> cf l::tl), (arg1::args)
+	   | _, [] -> (fun x -> a::tl), [])) in
+     begin
+       match (find_aux largs) with
+	   cf, [] -> (fun l -> mkApp(g, args)), []
+	 | cf, args ->
+	     (fun l -> mkApp (g, Array.of_list (cf l))), args
+     end
+  | Rel(_) -> error "find_call_occs : Rel"
+  | Var(id) -> (fun l -> expr), []
+  | Meta(_) -> error "find_call_occs : Meta"
+  | Evar(_) -> error "find_call_occs : Evar"
+  | Sort(_)  -> error "find_call_occs : Sort"
+  | Cast(_,_,_) -> error "find_call_occs : cast"
+  | Prod(_,_,_) -> error "find_call_occs : Prod"
+  | Lambda(_,_,_) -> error "find_call_occs : Lambda"
+  | LetIn(_,_,_,_) -> error "find_call_occs : let in"
+  | Const(_) -> (fun l -> expr), []
+  | Ind(_) -> (fun l -> expr), []
+  | Construct (_, _) -> (fun l -> expr), []
+  | Case(i,t,a,r) ->
+      (match find_call_occs f a with
+	cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
+      | _ -> (fun l -> mkCase(i, t, a, r)),[])
+  | Fix(_) -> error "find_call_occs : Fix"
+  | CoFix(_) -> error "find_call_occs : CoFix";;
+
+let rec  mk_intros_and_continue (extra_eqn:bool)
+    cont_function (eqs:constr list) (expr:constr) g =
+  let ids=ids_of_named_context (pf_hyps g) in
+  match kind_of_term expr with
+      Lambda (n, _, b) -> 
+     	let n1 = (match n with
+      	              Name x -> x
+                    | Anonymous -> (id_of_string "anonymous") ) in
+     	let new_n = next_ident_away n1 ids in
+	  tclTHEN (intro_using new_n)
+	    (mk_intros_and_continue extra_eqn cont_function eqs 
+	       (subst1 (mkVar new_n) b)) g
+    | _ -> 
+ 	if extra_eqn then
+	  let teq = next_ident_away (id_of_string "teq") ids in
+	    tclTHENSEQ
+	      [(intro_using teq); Equality.rewriteLR (mkVar teq); 
+	      (cont_function (mkVar teq::eqs) expr)] g
+	else
+	  cont_function eqs expr g;;
+
+let base_leaf_eq eqs f = tclTRY reflexivity 
+
+let rec_leaf_eq f ids eqs expr fn args = tclTRY reflexivity
+
+
+let rec prove_eq (f:constr)
+    (eqs:constr list)
+    (expr:constr) =
+  tclTRY
+    (match kind_of_term expr with
+	 Case(_,t,a,l) ->
+	   (match find_call_occs f a with
+		_,[] -> 
+		  tclTHENS(mkCaseEq a)(* (simplest_case a) *)
+	  	    (List.map
+		       (mk_intros_and_continue true
+			  (prove_eq  f) eqs)
+		       (Array.to_list l))
+	      | _,_::_ ->
+               	  (match find_call_occs f expr with
+		       _,[] -> base_leaf_eq eqs f
+		     | fn,args ->
+			 fun g ->
+			   let ids = pf_ids_of_hyps g in
+			   rec_leaf_eq f ids eqs expr fn args g
+		  )
+	   )
+       | _ -> 
+	   (match find_call_occs f expr with
+		_,[] -> base_leaf_eq eqs f
+	      | fn,args ->
+		  fun g ->
+		    let ids = pf_ids_of_hyps g in
+		    rec_leaf_eq f ids eqs expr fn args g
+	   )
+    )
+    
+
+let prove_eq f expr = 
+  let fname = destConst f in 
+  tclTHEN
+    (Tactics.unfold_constr (ConstRef fname))
+    (mk_intros_and_continue false (prove_eq f)  [] expr)
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 2f52e86d2f..48cc2ce3a5 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -568,19 +568,22 @@ let is_res id =
 (* rebuild the raw constructors expression. 
    eliminates some meaningless equality, applies some rewrites......
 *)
-let rec rebuild_cons relname args rt = 
+let rec rebuild_cons relname args crossed_types rt = 
   match rt with 
     | RProd(_,n,t,b) -> 
+	let not_free_in_t id = not (is_free_in id t) in 
+	let new_crossed_types = t::crossed_types in 
 	begin
 	  match t with 
 	    | RApp(_,(RVar(_,res_id) as res_rt),args') when is_res res_id ->
 		begin
 		  match args' with 
 		    | (RVar(_,this_relname))::args' -> 
-			let new_b,id_to_exclude =  rebuild_cons relname args b in 
+			let new_b,id_to_exclude =  rebuild_cons relname args new_crossed_types b in 
 			let new_t = 
 			  mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) 
-			in mkRProd(n,new_t,new_b),id_to_exclude
+			in mkRProd(n,new_t,new_b),
+			Idset.filter not_free_in_t id_to_exclude
 		    | _ -> (* the first args is the name of the function! *)
 			assert false 
 		end
@@ -588,36 +591,46 @@ let rec rebuild_cons relname args rt =
 		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  
 		  -> 
 		let is_in_b = is_free_in id b in
-		let keep_eq = not (List.exists (is_free_in id) args) || is_in_b in 
+		let keep_eq = 
+		  not (List.exists (is_free_in id) args) || is_in_b  || 
+		    List.exists (is_free_in id) crossed_types 
+		in 
 		let new_args = List.map (replace_var_by_term id rt) args in 
 		let subst_b = 
 		  if is_in_b then b else  replace_var_by_term id rt b 
 		in 
-		let new_b,id_to_exclude =  rebuild_cons relname new_args subst_b in 
+		let new_b,id_to_exclude =  rebuild_cons relname new_args new_crossed_types subst_b in 
 		if keep_eq then mkRProd(n,t,new_b),id_to_exclude 
 		else new_b, Idset.add id id_to_exclude
 	    | _ -> 
-		let new_b,id_to_exclude =  rebuild_cons relname args b in 
+		let new_b,id_to_exclude =  rebuild_cons relname args new_crossed_types b in 
 		match n with
 		  | Name id when Idset.mem id id_to_exclude ->
-		      new_b,Idset.remove id id_to_exclude
-		  | _ -> mkRProd(n,t,new_b),id_to_exclude
+		      new_b,Idset.remove id 
+			(Idset.filter not_free_in_t id_to_exclude)
+		  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	end
     | RLambda(_,n,t,b) ->
 	begin
-	  let new_b,id_to_exclude = rebuild_cons relname args b in
+	  let not_free_in_t id = not (is_free_in id t) in 
+	  let new_crossed_types = t :: crossed_types in 
+	  let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in
 	  match n with
 	    | Name id when Idset.mem id id_to_exclude ->
-		new_b,Idset.remove id id_to_exclude
-	    | _ -> RProd(dummy_loc,n,t,new_b),id_to_exclude
+		new_b,
+		Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+	    | _ -> 
+		RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	end
     | RLetIn(_,n,t,b) -> 
 	begin
-	  let new_b,id_to_exclude = rebuild_cons relname args b in
+	  let not_free_in_t id = not (is_free_in id t) in 
+	  let new_b,id_to_exclude = rebuild_cons relname args (t::crossed_types) b in
 	  match n with 
 	    | Name id when Idset.mem id id_to_exclude -> 
-		new_b,Idset.remove id id_to_exclude
-	    | _ -> RLetIn(dummy_loc,n,t,new_b),id_to_exclude
+		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+	    | _ -> RLetIn(dummy_loc,n,t,new_b),
+		Idset.filter not_free_in_t id_to_exclude
 	end
     | _ -> mkRApp(mkRVar  relname,args@[rt]),Idset.empty
 
@@ -699,6 +712,7 @@ let build_inductive funnames funsargs  returned_types (rtl:rawconstr list) =
 				 | Name id, _ -> mkRVar id
 			      )
 		       funsargs.(i)) 
+		    []
 		    rt 
 		)
 	     ) 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 7e62893d57..a416e3882c 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -44,12 +44,13 @@ open Eauto
 
 open Genarg
 
-let observe_tac s tac g =
- msgnl (Printer.pr_goal (sig_it g)); 
- try let v = tac g in msgnl ((str s)++(str " ")++(str "finished")); v
- with e -> 
-   msgnl (str "observation "++str s++str " raised an exception"); raise e;;
+let observe_tac s tac g = tac g
 
+(* let observe_tac s tac g = *)
+(*   begin try msgnl (Printer.pr_goal (sig_it g)) with _ -> assert false end; *)
+(*  try let v = tac g in msgnl ((str s)++(str " ")++(str "finished")); v *)
+(*  with e ->  *)
+(*    msgnl (str "observation "++str s++str " raised an exception"); raise e;; *)
 
 let hyp_ids = List.map id_of_string
     ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res";
@@ -199,27 +200,29 @@ let max_constr = lazy(constr_of_reference (Lazy.force max_ref))
 let nat = lazy(coq_constant "nat")
 let lt = lazy(coq_constant "lt")
 
-let  mkCaseEq a =
+let  mkCaseEq a  : tactic =
      (fun g ->
 (* commentaire de Yves: on pourra avoir des problemes si
    a n'est pas bien type dans l'environnement du but *)
-       let type_of_a = (type_of (pf_env g) Evd.empty a) in
+       let type_of_a = pf_type_of g a in
        (tclTHEN (generalize [mkApp(Lazy.force refl_equal, [| type_of_a; a|])])
 	  (tclTHEN 
 	     (fun g2 ->
-	       change_in_concl None 
-		 (pattern_occs [([2], a)] (pf_env g2) Evd.empty (pf_concl g2))
-		 g2)
+		change_in_concl None 
+		  (pattern_occs [([2], a)] (pf_env g2) Evd.empty (pf_concl g2))
+		  g2)
 	     (simplest_case a))) g);;
 
 let rec  mk_intros_and_continue (extra_eqn:bool)
     cont_function (eqs:constr list) (expr:constr) g =
-  let ids=ids_of_named_context (pf_hyps g) in
+  let ids = pf_ids_of_hyps g in
   match kind_of_term expr with
-      Lambda (n, _, b) -> 
-     	let n1 = (match n with
-      	              Name x -> x
-                    | Anonymous -> ano_id ) in
+    | Lambda (n, _, b) -> 
+     	let n1 = 
+	  match n with
+      	      Name x -> x
+            | Anonymous -> ano_id
+	in
      	let new_n = next_ident_away n1 ids in
 	  tclTHEN (intro_using new_n)
 	    (mk_intros_and_continue extra_eqn cont_function eqs 
@@ -230,7 +233,7 @@ let rec  mk_intros_and_continue (extra_eqn:bool)
 	    tclTHEN (intro_using teq)	
 	      (cont_function (mkVar teq::eqs) expr) g
 	else
-	  cont_function eqs expr g;;
+	  cont_function eqs expr g
 
 let const_of_ref = function
     ConstRef kn -> kn
@@ -241,8 +244,21 @@ let simpl_iter () =
     (Lazy 
        {rBeta=true;rIota=true;rZeta= true; rDelta=false;
         rConst = [ EvalConstRef (const_of_ref (Lazy.force iter_ref))]})
- onConcl;;
-
+    onConcl
+    
+let tclUSER l g = 
+  let b,l = 
+    match l with 
+	None -> true,[]
+      | Some l -> false,l
+  in
+  tclTHEN 
+    (h_clear b l)
+    (*     (tclIDTAC_MESSAGE (str "USER"++fnl()))  *)
+    tclIDTAC
+    g
+    
+    
 let list_rewrite (rev:bool) (eqs: constr list) =
   tclREPEAT
     (List.fold_right
@@ -263,7 +279,7 @@ let base_leaf (func:global_reference) eqs expr =
 		     	  (tclTHEN (simplest_elim 
 				      (mkApp (Lazy.force gt_antirefl,
 					      [| Lazy.force coq_O |])))
-		             default_auto)); tclIDTAC];
+		             default_auto)); tclIDTAC ];
                     intros;
 		    simpl_iter();
 		    unfold_constr func;
@@ -360,50 +376,27 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
 	   introduce_all_equalities func eqs values specs 
 	     (mkVar pmax) ((mkVar pmax)::le_proofs)
 	     (heq::cond_eqs)] g;;
-
-let rec introduce_all_values func context_fn
-    eqs proofs hrec args values specs =
-  match args with
-    [] -> 
-      tclTHENLIST
-	[split(ImplicitBindings
-		 [context_fn (List.map mkVar (List.rev values))]);
-	 introduce_all_equalities func eqs
-	   (List.rev values) (List.rev specs) (Lazy.force coq_O) [] []]
-  | arg::args ->
-      (fun g ->
-	let ids = ids_of_named_context (pf_hyps g) in
-	let rec_res = next_ident_away rec_res_id ids in
-        let ids = rec_res::ids in
-	let hspec = next_ident_away hspec_id ids in
-	let tac = introduce_all_values func context_fn eqs proofs
-	    hrec args
-	    (rec_res::values)(hspec::specs) in
-	    (tclTHENS
-	   (simplest_elim (mkApp(mkVar hrec, [|arg|])))
-	   [tclTHENLIST [intros_using [rec_res; hspec];
-			 tac]; tclIDTAC
-(*	    tclTHENLIST
-	      [list_rewrite true eqs;
-	       List.fold_right
-                 (fun proof tac ->
-                   tclORELSE
-                     (tclCOMPLETE
-			(tclTHENLIST
-                           [e_resolve_constr proof;
-                            tclORELSE default_full_auto e_assumption]))
-                     tac)
-                 proofs
-                 (fun g ->
-                   (msgnl (str "complete proof failed for decreasing call");
-                    msgnl (Printer.pr_goal (sig_it g)); tclFAIL 0 "" g))]*)
-]) g)
-       
+    
+let string_match  s =
+ try 
+  for i = 0 to 3  do
+    if String.get s i <> String.get "Acc_" i then failwith ""
+  done;
+ with Invalid_argument _ -> failwith ""
 	  
-
-let rec new_introduce_all_values acc_inv func context_fn
+let retrieve_acc_var g = 
+  (* Julien: I don't like this version .... *) 
+  let hyps = pf_ids_of_hyps g  in 
+  map_succeed 
+    (fun id -> 
+       try 
+	 string_match (string_of_id id);
+	 id
+       with _ -> failwith "")
+    hyps 
+
+let rec introduce_all_values acc_inv func context_fn
     eqs  hrec args values specs =
-  tclTRY 
     (match args with
     [] -> 
       tclTHENLIST
@@ -417,7 +410,7 @@ let rec new_introduce_all_values acc_inv func context_fn
 	let rec_res = next_ident_away rec_res_id ids in
         let ids = rec_res::ids in
 	let hspec = next_ident_away hspec_id ids in
-	let tac = new_introduce_all_values acc_inv func context_fn eqs 
+	let tac = introduce_all_values acc_inv func context_fn eqs 
 	  hrec args
 	  (rec_res::values)(hspec::specs) in
 	(tclTHENS
@@ -428,7 +421,9 @@ let rec new_introduce_all_values acc_inv func context_fn
 		 (apply (Lazy.force acc_inv))
 		 [ h_assumption
 		 ;
-		   tclIDTAC
+		   (fun g ->  
+		      tclUSER (Some (hrec::hspec::(retrieve_acc_var g)@specs)) g
+		   )
 		 ]
 	    )
 	   ]) g)
@@ -436,12 +431,12 @@ let rec new_introduce_all_values acc_inv func context_fn
     )
  
 	   
-let new_rec_leaf acc_inv hrec (func:global_reference) eqs expr =
+let rec_leaf acc_inv hrec (func:global_reference) eqs expr =
   match find_call_occs (mkVar (get_f (constr_of_reference func))) expr with
   | context_fn, args ->
-      new_introduce_all_values acc_inv func context_fn eqs  hrec args  [] []
+      introduce_all_values acc_inv func context_fn eqs  hrec args  [] []
 
-let rec new_proveterminate acc_inv (hrec:identifier)  (* (proofs:constr list) *)
+let rec proveterminate acc_inv (hrec:identifier)  (* (proofs:constr list) *)
   (f_constr:constr) (func:global_reference) (eqs:constr list) (expr:constr)  =
 try
 (*  let _ = msgnl (str "entering proveterminate") in *)
@@ -457,7 +452,7 @@ try
 			   v
 			)
    	         (List.map (mk_intros_and_continue true
-                              (new_proveterminate acc_inv hrec f_constr func)
+                              (proveterminate acc_inv hrec f_constr func)
                               eqs) 
 	            (Array.to_list l))
 	   | _, _::_ -> 
@@ -465,7 +460,7 @@ try
 		 match find_call_occs  f_constr expr with
 	     	     _,[] -> base_leaf func eqs expr
 		   | _, _:: _ -> 
-		       new_rec_leaf acc_inv hrec  func eqs expr
+		       rec_leaf acc_inv hrec  func eqs expr
 	       )
 	)
     | _ ->  (match find_call_occs  f_constr expr with
@@ -474,55 +469,28 @@ try
 		    base_leaf func eqs expr
 		   with e -> (msgerrnl (str "failure in base case");raise e ))
 	       | _, _::_ -> 
-		   new_rec_leaf acc_inv hrec  func eqs expr) in
+		   rec_leaf acc_inv hrec  func eqs expr) in
   (*  let _ = msgnl(str "exiting proveterminate") in *)
   v
 with e -> 
   msgerrnl(str "failure in proveterminate"); 
-(*   raise e *)
-  tclIDTAC
+  raise e
 
 let hyp_terminates func = 
-  let a_arrow_b = (arg_type (constr_of_reference func)) in
-  let (_,a,b) = destProd a_arrow_b in
-  let left=
-    mkApp (Lazy.force iter, 
-	   [|a_arrow_b ;(mkRel 3); 
-	     (constr_of_reference func); (mkRel 1); (mkRel 6)|]) in
-  let right= (mkRel 5) in
-  let equality = mkApp(Lazy.force eq, [|b; left; right|]) in
-  let result = (mkProd ((Name def_id) , a_arrow_b, equality)) in
-  let cond = mkApp(Lazy.force lt, [|(mkRel 2); (mkRel 1)|]) in
-  let nb_iter =
-    mkApp(Lazy.force ex,
-	  [|Lazy.force nat;
-	    (mkLambda 
-	       (Name
-		  p_id,
-		  Lazy.force nat, 
-		  (mkProd (Name k_id, Lazy.force nat, 
-			   mkArrow cond result))))|])in
-  let value = mkApp(Lazy.force coq_sig, 
-		    [|b;
-		      (mkLambda (Name v_id, b, nb_iter))|]) in
-  mkProd ((Name x_id), a, value)
-
-
-let new_hyp_terminates func = 
   let a_arrow_b = arg_type (constr_of_reference func) in 
   let rev_args,b = decompose_prod a_arrow_b in 
   let left = 
     mkApp(Lazy.force iter, 
 	  Array.of_list 
-	    (a_arrow_b:: mkRel 3::
+	    (lift 5 a_arrow_b:: mkRel 3::
 	       constr_of_reference func::mkRel 1::
 	       List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
 	    )
 	 )
   in
   let right = mkRel 5 in 
-  let equality = mkApp(Lazy.force eq, [|b; left; right|]) in
-  let result = (mkProd ((Name def_id) , a_arrow_b, equality)) in
+  let equality = mkApp(Lazy.force eq, [|lift 5 b; left; right|]) in
+  let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in
   let cond = mkApp(Lazy.force lt, [|(mkRel 2); (mkRel 1)|]) in
   let nb_iter =
     mkApp(Lazy.force ex,
@@ -539,10 +507,16 @@ let new_hyp_terminates func =
   compose_prod rev_args value
 	     
 
-let new_start input_type ids args_id relation rec_arg_num rec_arg_id tac : tactic = 
+let start input_type ids args_id relation rec_arg_num rec_arg_id tac : tactic = 
   begin 
     fun g -> 
       let nargs = List.length args_id in
+      let pre_rec_args = 
+	List.rev_map
+	  mkVar (fst (list_chop (rec_arg_num - 1) args_id)) 
+      in 
+      let relation = substl pre_rec_args relation in 
+      let input_type = substl pre_rec_args input_type in 
       let wf_thm = next_ident_away (id_of_string ("wf_R")) ids in 
       let wf_rec_arg = 
 	next_ident_away 
@@ -562,83 +536,67 @@ let new_start input_type ids args_id relation rec_arg_num rec_arg_id tac : tacti
       tclTHEN
 	(intros_using args_id)
 	(tclTHENS
-	(assert_tac 
-	   true (* the assert thm is in first subgoal *)
-	   (Name wf_rec_arg) 
-	   (mkApp (Lazy.force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
-	)
-	[
-	  (* accesibility proof *) 
-	  tclTHENS 
-	    (assert_tac 
-	       true 
-	       (Name wf_thm)
-	       (mkApp (Lazy.force well_founded,[|input_type;relation|]))
-	    )
-	    [ 
-	      (* interactive proof of the well_foundness of the relation *) 
-	      tclIDTAC;
-	      (* well_foundness -> Acc for any element *)
-	      h_apply ((mkApp(mkVar wf_thm,[|mkVar rec_arg_id |])),Rawterm.NoBindings)
-	    ]
-	  ;
-	  (* rest of the proof *)
-	  tclTHENSEQ 
-	    [onNLastHyps (nargs+1)
-	       (fun (id,_,_) -> 
-		  tclTHEN (generalize [mkVar id]) (h_clear false [id])
+	   (observe_tac 
+	      "first assert" 
+	      (assert_tac 
+		 true (* the assert thm is in first subgoal *)
+		 (Name wf_rec_arg) 
+		 (mkApp (Lazy.force acc_rel,
+			 [|input_type;relation;mkVar rec_arg_id|])
+		 )
+	      )
+	   )
+	   [
+	     (* accesibility proof *) 
+	     tclTHENS 
+	       (observe_tac 
+		  "second assert" 
+		  (assert_tac 
+		     true 
+		     (Name wf_thm)
+		     (mkApp (Lazy.force well_founded,[|input_type;relation|]))
+		  )
 	       )
-	    ;
-	     h_fix (Some hrec) (nargs+1);
-	     intros_using args_id;
-	     intro_using wf_rec_arg;
-	     tac hrec acc_inv
-	    ]
-	]
+	       [ 
+		 (* interactive proof of the well_foundness of the relation *) 
+		 tclUSER None;
+		 (* well_foundness -> Acc for any element *)
+		 observe_tac 
+		   "apply wf_thm" 
+		   (h_apply ((mkApp(mkVar wf_thm,
+				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+		   )
+	       ]
+	     ;
+	     (* rest of the proof *)
+	     tclTHENSEQ 
+	       [observe_tac "generalize" 
+		  (onNLastHyps (nargs+1)
+		     (fun (id,_,_) -> 
+			tclTHEN (generalize [mkVar id]) (h_clear false [id])
+		     ))
+	       ;
+		observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
+		intros_using args_id;
+		intro_using wf_rec_arg;
+		observe_tac "tac" (tac hrec acc_inv)
+	       ]
+	   ]
 	) g  
   end
 
 
-let start n_name input_type relation wf_thm = 
-  (fun g ->
-try
-  let ids = ids_of_named_context (pf_hyps g) in
-  let hrec = next_ident_away hrec_id (n_name::ids) in
-  let wf_c = mkApp(Lazy.force well_founded_induction,
-		   [|input_type; relation; wf_thm|]) in
-  let x = next_ident_away x_id (hrec::n_name::ids) in
-  let v =
-    (fun g ->
-      let v = 
-	tclTHENLIST
-	  [intro_using x;
-	   general_elim (mkVar x, ImplicitBindings[]) (wf_c, ImplicitBindings[]);
-	   clear [x];
-	   intros_using [n_name; hrec]] g in
-	v), hrec in 
-      v
-with e -> msgerrnl(str "error in start"); raise e);;
-
-(* let rec instantiate_lambda t = function *)
-(*   | [] -> t *)
-(*   | a::l -> let (bound_name, _, body) = destLambda t in *)
-(*       (match bound_name with *)
-(* 	   Name id -> instantiate_lambda (subst1 a body) l *)
-(* 	 | Anonymous -> body) ;; *)
 
 let rec instantiate_lambda t l = 
   match l with
   | [] -> t
   | a::l -> 
       let (bound_name, _, body) = destLambda t in
-(*       (match bound_name with *)
-(* 	   Name id -> instantiate_lambda (subst1 a body) l *)
-(* 	 | Anonymous -> body)*)
       instantiate_lambda (subst1 a body) l
 ;;
 
 
-let new_whole_start func input_type relation rec_arg_num  : tactic = 
+let whole_start func input_type relation rec_arg_num  : tactic = 
   begin 
     fun g -> 
       let ids = ids_of_named_context (pf_hyps g) in
@@ -664,7 +622,7 @@ let new_whole_start func input_type relation rec_arg_num  : tactic =
       in
       let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
       let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in 
-      new_start 
+      start 
 	input_type
 	ids
 	n_ids
@@ -672,56 +630,35 @@ let new_whole_start func input_type relation rec_arg_num  : tactic =
 	rec_arg_num
 	rec_arg_id
 	(fun hrec acc_inv g ->  
-	   try
-             (new_proveterminate 
-		acc_inv 
-		hrec
-		(mkVar f_id)
-		func
-		[]
-		expr
-	     )
-	       g 
-	   with e -> msgnl (str "debug : found an exception");raise e
+           (proveterminate 
+	      acc_inv 
+	      hrec
+	      (mkVar f_id)
+	      func
+	      []
+	      expr
+	   )
+	     g 
 	)
 	g 
   end
 
 
 
-let new_com_terminate fonctional_ref input_type relation_ast rec_arg_num
+let com_terminate fonctional_ref input_type relation rec_arg_num
     thm_name hook =
   let (evmap, env) = Command.get_current_context() in
-  let (relation:constr)= interp_constr evmap env relation_ast in
-    (start_proof thm_name
-       (Global, Proof Lemma) (Environ.named_context_val env)
-         (new_hyp_terminates fonctional_ref) hook;
-     by (new_whole_start fonctional_ref
-	   input_type relation rec_arg_num ));;
+  start_proof thm_name
+    (Global, Proof Lemma) (Environ.named_context_val env)
+    (hyp_terminates fonctional_ref) hook;
+  by (whole_start fonctional_ref
+	input_type relation rec_arg_num )
+    
 
 let ind_of_ref = function 
   | IndRef (ind,i) -> (ind,i)
   | _ -> anomaly "IndRef expected"
 
-let (value_f:constr -> global_reference -> constr) =
-  fun a fterm ->
-    let d0 = dummy_loc in 
-    let x_id =  x_id in
-    let v_id = v_id in
-    let value =
-      RLambda
-      	(d0, Name x_id, RDynamic(d0, constr_in a),
-	 RCases
-	   (d0,None,
-	   [RApp(d0, RRef(d0,fterm), [RVar(d0, x_id)]),(Anonymous,None)],
-	    [d0, [v_id], [PatCstr(d0,(ind_of_ref 
-					(Lazy.force coq_sig_ref),1),
-				  [PatVar(d0, Name v_id);
-				   PatVar(d0, Anonymous)],
-				  Anonymous)],
-	     RVar(d0,v_id)])) in
-      understand Evd.empty (Global.env()) value;;
-
 let (value_f:constr list -> global_reference -> constr) =
   fun al fterm ->
     let d0 = dummy_loc in 
@@ -967,25 +904,37 @@ let recursive_definition f type_of_f r  rec_arg_num eq =
   let env = push_rel (Name f,None,function_type) (Global.env()) in
   let res_vars,eq' = decompose_prod (interp_constr Evd.empty env eq) in 
   let res = 
+(*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
+(*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
+(*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
     match kind_of_term eq' with 
       | App(e,[|_;_;eq_fix|]) -> 
 		  mkLambda (Name f,function_type,compose_lam res_vars eq_fix)
-      | _ -> failwith "Recursive Definition"
+      | _ -> failwith "Recursive Definition (res not eq)"
   in
-  let _,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in 
+  let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in 
   let (_, rec_arg_type, _) = destProd function_type_before_rec_arg in
   let arg_types = List.rev_map snd (fst (decompose_prod_n (List.length res_vars) function_type)) in
   let equation_id = add_suffix f "_equation" in
   let functional_id =  add_suffix f "_F" in
   let term_id = add_suffix f "_terminate" in
   let functional_ref = declare_fun functional_id (IsDefinition Definition) res in
+(*   let _ = Pp.msgnl (str "res := " ++ Printer.pr_lconstr res) in  *)
+  let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in 
+  let relation = 
+    interp_constr
+      Evd.empty 
+      env_with_pre_rec_args
+      r
+  in 
+(*   let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook _ _ =   
     let term_ref = Nametab.locate (make_short_qualid term_id) in
     let f_ref = declare_f f (IsProof Lemma) arg_types term_ref in
 (*     let _ = message "start second proof" in *)
     com_eqn equation_id functional_ref f_ref term_ref eq
   in
-  new_com_terminate functional_ref rec_arg_type r  rec_arg_num term_id  hook 
+  com_terminate functional_ref rec_arg_type relation  rec_arg_num term_id  hook 
 ;;
 
 VERNAC COMMAND EXTEND RecursiveDefinition