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

7 files changed, 799 insertions, 212 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 
 		)
 	     )