Julien:

+ Compatibility with new induction
+ Induction principle for general recursion preparation still continuing
+ Cleaning dead code ...


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

12 files changed, 806 insertions, 644 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 86a67866c..56855f5da 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -62,68 +62,8 @@ let build_newrecursive
     States.unfreeze fs; def
   in
   recdef
-
-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
-  lookup 
-
-    
-let register 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 generate_correction_proof_struct  ind_kn  newfixpoint_exprl =
-  let fname_kn (fname,_,_,_,_) =
-    let f_ref = Ident (dummy_loc,fname) in
-    locate_with_msg
-      (pr_reference f_ref++str ": Not an inductive type!")
-      locate_constant
-      f_ref
-  in
-  let funs_kn = Array.of_list (List.map fname_kn newfixpoint_exprl) in 
-  ignore
-    (Util.list_map_i
-       (fun i x ->
-(* 	  let f_kn = fname_kn x in *)
-	  New_arg_principle.generate_new_structural_principle
-	    (destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)))
-	    (Termops.new_sort_in_family InType)
-	    None
-	    true
-	    funs_kn
-	    i
-       )
-       0
-       newfixpoint_exprl
-    );
-    ()
- 
 let compute_annot (name,annot,args,types,body) =
   let names = List.map snd (Topconstr.names_of_local_assums args) in
   match annot with
@@ -147,8 +87,7 @@ let rec is_rec names =
     | 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) -> 
+    | RLetIn(_,_,t,b) | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
 	lookup t || lookup b
     | RApp(_,f,args) -> List.exists lookup (f::args)
     | RCases(_,_,el,brl) -> 
@@ -157,7 +96,54 @@ let rec is_rec names =
   in
   lookup 
 
-    
+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 generate_principle fix_rec_l recdefs  interactive_proof parametrize continue_proof   =
+  let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
+  let fun_bodies = List.map2 prepare_body fix_rec_l 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 parametrize names funs_args funs_types recdefs;
+    let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
+    let ind_kn =
+      fst (locate_with_msg
+	(pr_reference f_R_mut++str ": Not an inductive type!")
+	locate_ind
+	f_R_mut)
+    in
+    let fname_kn (fname,_,_,_,_) =
+      let f_ref = Ident (dummy_loc,fname) in
+      locate_with_msg
+	(pr_reference f_ref++str ": Not an inductive type!")
+	locate_constant
+	f_ref
+    in
+  let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in 
+  let _ = 
+    Util.list_map_i
+      (fun i x ->
+	 New_arg_principle.generate_new_structural_principle
+	   interactive_proof 
+	   (destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)))
+	   None
+	   funs_kn
+	   i
+	  (continue_proof i funs_kn)
+      )
+      0
+      fix_rec_l
+  in 
+  ()
+  with e -> 
+(*     Pp.msg_warning (Cerrors.explain_exn e) *)
+    ()
+
+
 let register_struct is_rec fixpoint_exprl = 
   match fixpoint_exprl with 
     | [(fname,_,bl,ret_type,body),_] when not is_rec -> 
@@ -172,7 +158,17 @@ let register_struct is_rec fixpoint_exprl =
     | _ -> 
 	Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
 
-let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body =  
+
+let generate_correction_proof_wf  
+    is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+    (_: int) (_:Names.constant array) (_:int) : Tacmach.tactic = 
+  Recdef.prove_principle 
+    is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+
+
+let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
+    pre_hook 
+    =  
   let type_of_f = Command.generalize_constr_expr ret_type args in 
   let rec_arg_num = 
     let names = 
@@ -205,7 +201,20 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body =
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Command.generalize_constr_expr unbounded_eq args in 
-  Recdef.recursive_definition is_mes fname type_of_f wf_rel_expr rec_arg_num eq
+  let hook f_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
+    pre_hook 
+      (generate_correction_proof_wf is_mes
+	 f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+      )
+  in 
+  Recdef.recursive_definition 
+    is_mes fname 
+    type_of_f
+    wf_rel_expr
+    rec_arg_num
+    eq
+    hook
+
     
 let register_mes fname wf_mes_expr wf_arg args ret_type body = 
   let wf_arg_type,wf_arg = 
@@ -222,7 +231,9 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body =
 	      List.find 
 		(function 
 		   | Topconstr.LocalRawAssum(l,t) -> 
-		       List.exists (function (_,Name id) -> id =  wf_args | _ -> false) l 
+		       List.exists 
+			 (function (_,Name id) -> id =  wf_args | _ -> false) 
+			 l 
 		   | _ -> false
 		)
 		args 
@@ -252,13 +263,28 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body =
 
 let register (fixpoint_exprl :  newfixpoint_expr list) = 
   let recdefs = build_newrecursive fixpoint_exprl in 
-  let is_struct = 
+  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;
+	  let pre_hook = 
+	    generate_principle 
+	      fixpoint_exprl 
+	      recdefs
+	      true
+	      false
+	  in 
+	  register_wf name wf_rel wf_x args types body pre_hook;
 	  false
       | [((name,Mes (wf_mes,wf_x),args,types,body))] -> 
-	  register_mes name wf_mes wf_x args types body;
+	  let pre_hook = 
+	    generate_principle 
+	      fixpoint_exprl 
+	      recdefs
+	      true
+	      false
+	  in 
+	  register_mes name wf_mes wf_x args types body pre_hook;
+
 	  false
       | _ -> 
 	  
@@ -285,14 +311,17 @@ let register (fixpoint_exprl :  newfixpoint_expr list) =
 	  in
 	  let is_rec = List.exists (is_rec fix_names) recdefs in
 	  register_struct is_rec old_fixpoint_exprl;
+	  generate_principle 
+	    fixpoint_exprl
+	    recdefs 
+	    false
+	    true
+	    (New_arg_principle.prove_princ_for_struct);
 	  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 
@@ -300,89 +329,4 @@ let do_generate_principle fix_rec_l =
   *)
   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 *)
+  register newfixpoint_exprl 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index c2c23f418..96d0df5cc 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -157,157 +157,160 @@ 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 
+(* (\************************************************\)  *)
+(* (\* 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)        *)
-(************************************************) 
+(*      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 c784dd5dd..03805ddef 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -39,15 +39,3 @@ 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 fca784b46..bbaa8b5a0 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -15,26 +15,31 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-open Indfun_common
-open Pp
-open Libnames
-open Names
-open Term
+(* open Indfun_common *)
+(* open Pp *)
+(* open Libnames *)
+(* open Names *)
+(* open Term *)
 
 
-open Pcoq
+(* open Pcoq *)
 
-open Genarg
-open Vernac_
-open Prim
-open Constr
-open G_constr
-open G_vernac
-open Indfun
-open Topconstr
-
-open Tacinterp
+(* open Genarg *)
+(* open Vernac_ *)
+(* open Prim *)
+(* open Constr *)
+(* open G_constr *)
+(* open G_vernac *)
+(* open Indfun *)
+(* open Topconstr *)
 
+(* open Tacinterp *)
+open Term
+open Names
+open Pp
+open Topconstr
+open Indfun_common 
+open Indfun
 
 TACTIC EXTEND newfuninv
    [ "functional" "inversion" ident(hyp) ident(fname) ] -> 
@@ -69,17 +74,30 @@ TACTIC EXTEND newfunind
 	     )
 	 with _ -> assert false)
 	 in
-	 compute_elim_sig princ_type
+	 Tactics.compute_elim_sig (mkRel 0,Rawterm.NoBindings) princ_type
        in
+(* 	   msg *)
+(* 	     (str "computing non parameters argument for " ++ *)
+(* 		Ppconstr.pr_id princ_name ++ fnl () ++ *)
+(* 		str "detected params are : " ++ *)
+(* 		Util.prlist_with_sep spc (fun (id,_,_) -> Ppconstr.pr_name id) princ_info.Tactics.params ++ fnl ()++ *)
+(* 		str  "detected arguments are " ++ *)
+(* 		Util.prlist_with_sep spc (Printer.pr_lconstr_env (Tacmach.pf_env g))  args ++ fnl ()  *)
+(* 	      ++ str " number of predicates " ++ *)
+(* 		str (string_of_int (List.length princ_info.Tactics.predicates))++ fnl () ++ *)
+(* 		str " number of branches " ++ *)
+(* 		str (string_of_int (List.length princ_info.Tactics.branches)) *)
+(* 	     ); *)
+
        let frealargs = 
 	 try
-	   snd (Util.list_chop (List.length princ_info.params) args)
+	   snd (Util.list_chop (List.length princ_info.Tactics.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 (string_of_int (List.length princ_info.Tactics.params)) ++ fnl ()++
 		str  " while number of arguments is " ++
 		str (string_of_int (List.length args)) ++ fnl () 
 (* 		str " number of predicates " ++  *)
@@ -94,8 +112,8 @@ TACTIC EXTEND newfunind
 	    (Rawterm.Pattern (List.map (fun e -> ([],e)) (frealargs@[c])))
 	    Tacticals.onConcl
 	 )
-	 ((Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings)))
-	 g
+	 (Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings))
+     	 g
      ]
 END
 
@@ -115,7 +133,7 @@ END
 
 VERNAC ARGUMENT EXTEND rec_definition2
  [ ident(id)  binder2_list( bl)
-     rec_annotation2_opt(annot) ":" constr( type_)
+     rec_annotation2_opt(annot) ":" lconstr( type_)
 	":=" lconstr(def)] ->
           [let names = List.map snd (Topconstr.names_of_local_assums bl) in
 	   let check_one_name () =
@@ -156,20 +174,3 @@ 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 4e87c4c95..767974c3a 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -107,7 +107,7 @@ let invfun (hypname:identifier) (fid:identifier) : tactic=
 	     )
 	 with _ -> assert false)
       in
-      Indfun_common.compute_elim_sig princ_type
+      Tactics.compute_elim_sig (mkRel 0,Rawterm.NoBindings) princ_type
     in
     let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
     let do_invert  fargs  appf : tactic = 
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
index eea603e18..56d0473d9 100644
--- a/contrib/funind/new_arg_principle.ml
+++ b/contrib/funind/new_arg_principle.ml
@@ -130,7 +130,7 @@ let is_pte_id =
   function  id -> 
     String.sub (string_of_id id) 0 pref_length = prov_pte_prefix
 
-let compute_new_princ_type_from_rel with_concl replace
+let compute_new_princ_type_from_rel  replace
     (rel_as_kn:mutual_inductive)  =
   let is_dom c =
     match kind_of_term c with
@@ -464,10 +464,8 @@ let finalize_proof rec_pos fixes (hyps:identifier list) =
 	 )
       ))
   in
-  let finalize_proof with_concl fnames t  : tactic = 
+  let finalize_proof fnames t  : tactic = 
     let change_tac  tac g =
-      if with_concl
-      then
 	match kind_of_term ( pf_concl g) with
 	  | App(p,args) ->
 	      let nargs = Array.length args in
@@ -483,7 +481,6 @@ let finalize_proof rec_pos fixes (hyps:identifier list) =
 		  g
 	      end
 	  | _ -> assert false
-      else tac g
     in
   fun g -> 
 (*     if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
@@ -495,11 +492,11 @@ let finalize_proof rec_pos fixes (hyps:identifier list) =
   finalize_proof
 
 let do_prove_princ_for_struct
-    (rec_pos:int option) (with_concl:bool) (fnames:constant list)
+    (rec_pos:int option)  (fnames:constant list)
     (ptes:identifier list) (fixes:identifier Idmap.t) (hyps: identifier list)
       (term:constr) : tactic =
   let finalize_proof term = 
-    finalize_proof rec_pos fixes hyps with_concl fnames term
+    finalize_proof rec_pos fixes hyps fnames term
   in
   let rec do_prove_princ_for_struct do_finalize term g =
 (*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
@@ -583,7 +580,7 @@ let do_prove_princ_for_struct
     term
 
 
-let prove_princ_for_struct with_concl f_names fun_num nparams : tactic = 
+let prove_princ_for_struct fun_num f_names  nparams : tactic = 
   let fnames_as_constr = Array.to_list (Array.map mkConst f_names) in 
   let fbody = 
     match (Global.lookup_constant f_names.(fun_num)).const_body with 
@@ -609,8 +606,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 )||
-      ((not with_concl) && goal_nb_prod = 0 )
+    goal_nb_prod < 1 
   in
   let rec intro_params tac params n : tactic =  
     if n = 0 
@@ -765,7 +761,7 @@ let prove_princ_for_struct with_concl f_names fun_num nparams : tactic =
 (* 	 tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f g *)
       )
   in
-  prepare_goal_tac (fun g -> do_prove_princ_for_struct rec_arg_num with_concl g) 
+  prepare_goal_tac (fun g -> do_prove_princ_for_struct rec_arg_num g) 
     
   
 
@@ -807,8 +803,10 @@ let change_property_sort nparam toSort princ princName =
   res
 
 let generate_new_structural_principle 
-    old_princ toSort new_princ_name with_concl funs i  
+    interactive_proof
+    old_princ new_princ_name funs i proof_tac 
     = 
+  let type_sort = (Termops.new_sort_in_family InType) in 
   let f = funs.(i) in 
   (* First we get the type of the old graph principle *)
   let old_princ_type =  (Global.lookup_constant old_princ).const_type
@@ -851,11 +849,7 @@ let generate_new_structural_principle
 	if is_pte_type t 
 	then 
 	  let t' = 
-	    if with_concl 
-	    then let args,concl = decompose_prod t in compose_prod args (mkSort toSort)
-	    else 
-	      let pte_args,pte_concl = decompose_prod t in 
-	      compose_prod (List.tl pte_args) (* (pop pte_concl) *) (mkSort toSort)
+	    let args,concl = decompose_prod t in compose_prod args (mkSort type_sort)
 	  in
 	  let pte_id = fresh_id avoid prov_pte_prefix in 
 	  f ((Name pte_id,None,t)::acc_context,(n,t')::acc_prod) (pte_id::avoid) c'
@@ -868,7 +862,6 @@ let generate_new_structural_principle
 (*   let tim1 = Sys.time ()  in *)
   let new_principle_type,_ = 
     compute_new_princ_type_from_rel 
-      with_concl
       (Array.map mkConst funs)
       mutr_as_kn
       env_with_ptes
@@ -886,7 +879,7 @@ let generate_new_structural_principle
       | Some (id) -> id
       | None -> 
 	  let id_of_f = id_of_label (con_label f) in
-	  Indrec.make_elimination_ident id_of_f (family_of_sort toSort)
+	  Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
   in
   let hook _ _  = 
     let id_of_f = id_of_label (con_label f) in
@@ -923,12 +916,11 @@ let generate_new_structural_principle
     ;
     try 
 (*       let tim1 = Sys.time ()  in *)
-      Pfedit.by  
-	((prove_princ_for_struct with_concl funs i  mutr_nparams));
+      Pfedit.by  (proof_tac mutr_nparams);
 (*       let tim2 = Sys.time ()  in *)
 (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float (tim2 -. tim1))); *)
 
-      if Tacinterp.get_debug () = Tactic_debug.DebugOff 
+      if Tacinterp.get_debug () = Tactic_debug.DebugOff && not interactive_proof 
       then
 	Options.silently Command.save_named false;
 
diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli
index dd3630a0d..18e2af7bc 100644
--- a/contrib/funind/new_arg_principle.mli
+++ b/contrib/funind/new_arg_principle.mli
@@ -1,18 +1,23 @@
 
 val generate_new_structural_principle : 
+  (* do we accept interactive proving *)
+  bool ->
   (* induction principle on rel *) 
   Names.constant ->
-  (* the elimination sort *)
-  Term.sorts -> 
   (* Name of the new principle *) 
   (Names.identifier) option -> 
-  (* do we want to use a principle with conclusion *)
-  bool -> 
   (* the compute functions to use   *)
   Names.constant array -> 
+  (* We prove the nth- principle *)
   int  ->
+  (* The tactic to use to make the proof w.r
+     the number of params
+  *)
+  (int -> Tacmach.tactic) -> 
   unit
 
 
 
 val my_reflexivity : Tacmach.tactic 
+
+val prove_princ_for_struct : int -> Names.constant array -> int -> Tacmach.tactic
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 48cc2ce3a..6b3590dd6 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -9,12 +9,21 @@ open Util
 open Rawtermops
 
 
-type binder_type = 
-  | Lambda 
-  | Prod 
-  | LetIn
+(* type binder_type =  *)
+(*   | Lambda  *)
+(*   | Prod  *)
+(*   | LetIn *)
+  
+(* type raw_context = (binder_type*name*rawconstr) list *)
+
+type binder_type =
+  | Lambda of name 
+  | Prod of name 
+  | LetIn of name
+(*   | LetTuple of name list * name  *)
+
+type raw_context = (binder_type*rawconstr) list
 
-type raw_context = (binder_type*name*rawconstr) list
 
 (* 
    compose_raw_context [(bt_1,n_1,t_1);......] rt returns 
@@ -22,11 +31,13 @@ type raw_context = (binder_type*name*rawconstr) list
    binders corresponding to the bt_i's
 *)
 let compose_raw_context = 
-  let compose_binder  (bt,n,t) acc =
+  let compose_binder  (bt,t) acc =
     match bt with 
-      | Lambda -> mkRLambda(n,t,acc)
-      | Prod -> mkRProd(n,t,acc)
-      | LetIn -> mkRLetIn(n,t,acc)
+      | Lambda n -> mkRLambda(n,t,acc)
+      | Prod n -> mkRProd(n,t,acc)
+      | LetIn n -> mkRLetIn(n,t,acc)
+(*       | LetTuple (nal,na) ->  *)
+(* 	  RLetTuple(dummy_loc,nal,(na,None),t,acc) *)
   in
   List.fold_right compose_binder
   
@@ -100,27 +111,104 @@ let combine_args arg args =
   }
 
 
+let ids_of_binder =  function 
+  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
+  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> [id]
+(*   | LetTuple(nal,_) ->  *)
+(*       map_succeed (function Name id -> id | _ -> failwith "ids_of_binder") nal *)
+
+let rec change_vars_in_binder mapping = function 
+    [] -> []
+  | (bt,t)::l ->
+      let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in 
+      (bt,change_vars mapping t)::
+	(if Idmap.is_empty new_mapping
+	 then l 
+	 else change_vars_in_binder new_mapping l
+	)
+
+let rec replace_var_by_term_in_binder x_id term = function
+  | [] -> []
+  | (bt,t)::l -> 
+      (bt,replace_var_by_term x_id term t)::
+	if List.mem x_id (ids_of_binder bt) 
+	then l
+	else replace_var_by_term_in_binder x_id term l
+
+let add_bt_names bt = List.append (ids_of_binder bt)
+
+(* let rec replace_var_by_term_in_binder x_id term = function  *)
+(*   | [] -> []  *)
+(*   | (bt,Name id,t)::l when id_ord id x_id = 0 ->  *)
+(*       (bt,Name id,replace_var_by_term x_id term t)::l *)
+(*   | (bt,na,t)::l ->  *)
+(*       (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l) *)
+
+(* let rec change_vars_in_binder mapping = function *)
+(*   | [] -> [] *)
+(*   | (bt,(Name id as na),t)::l when Idmap.mem id mapping -> *)
+(*       (bt,na,change_vars mapping t):: l *)
+(*   | (bt,na,t)::l -> *)
+(*       (bt,na,change_vars mapping t):: *)
+(* 	(change_vars_in_binder mapping l) *)
 
    
+(* let alpha_ctxt avoid b = *)
+(*   let rec alpha_ctxt = function *)
+(*     | [] -> [],b *)
+(*     | (bt,n,t)::ctxt -> *)
+(* 	let new_ctxt,new_b = alpha_ctxt ctxt in *)
+(* 	match n with *)
+(* 	  | Name id when List.mem id avoid -> *)
+(* 	      let new_id = Nameops.next_ident_away id avoid in *)
+(* 	      let mapping = Idmap.add id new_id Idmap.empty in *)
+(* 	      (bt,Name new_id,t):: *)
+(* 		(change_vars_in_binder mapping new_ctxt), *)
+(* 	      change_vars mapping new_b *)
+(* 	  | _ -> (bt,n,t)::new_ctxt,new_b *)
+(*   in *)
+(*   alpha_ctxt *)
 let apply_args ctxt body args = 
   let need_convert_id avoid id = 
     List.exists (is_free_in id) args || List.mem id avoid 
   in 
-  let need_convert avoid  =  function
-    | Anonymous -> false 
-    | Name id -> need_convert_id avoid id 
+  let need_convert avoid  bt =  
+    List.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let add_name na avoid = 
+(*   let add_name na avoid =  *)
+(*     match na with  *)
+(*       | Anonymous -> avoid  *)
+(*       | Name id -> id::avoid  *)
+(*   in *)
+  let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = 
     match na with 
-      | Anonymous -> avoid 
-      | Name id -> id::avoid 
+       | Name id when List.mem id avoid -> 
+	   let new_id = Nameops.next_ident_away id avoid in 
+	   Name new_id,Idmap.add id new_id mapping,new_id::avoid
+       | _ -> na,mapping,avoid
   in
-  let next_name_away na avoid = 
-    match na with 
-      | Anonymous -> anomaly "next_name_away"
-      | Name id -> 
-	  let new_id = Nameops.next_ident_away id avoid in 
-	  Name new_id,Idmap.add id new_id Idmap.empty,new_id::avoid
+  let next_bt_away bt (avoid:identifier list) = 
+    match bt with 
+      | LetIn na -> 
+	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in 
+	  LetIn new_na,mapping,new_avoid
+      | Prod na -> 
+	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in 
+	  Prod new_na,mapping,new_avoid
+      | Lambda na -> 
+	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in 
+	  Lambda new_na,mapping,new_avoid
+(*       | LetTuple (nal,na) ->  *)
+(* 	  let rev_new_nal,mapping,new_avoid =  *)
+(* 	    List.fold_left *)
+(* 	      (fun (nal,mapping,(avoid:identifier list)) na ->  *)
+(* 		 let new_na,new_mapping,new_avoid = next_name_away na mapping avoid in *)
+(* 		 (new_na::nal,new_mapping,new_avoid) *)
+(* 	      ) *)
+(* 	      ([],Idmap.empty,avoid) *)
+(* 	      nal *)
+(* 	  in  *)
+(* 	  (LetTuple(List.rev rev_new_nal,na),mapping,new_avoid) *)
   in
   let rec do_apply avoid ctxt body args = 
     match ctxt,args with  
@@ -129,9 +217,9 @@ let apply_args ctxt body args =
       | [],_ -> (* no more fun *)
 	  let f,args' = raw_decompose_app body in
 	  (ctxt,mkRApp(f,args'@args))
-      | (Lambda,Anonymous,t)::ctxt',arg::args' -> 
+      | (Lambda Anonymous,t)::ctxt',arg::args' -> 
 	  do_apply avoid ctxt' body args'
-      | (Lambda,Name id,t)::ctxt',arg::args' -> 
+      | (Lambda (Name id),t)::ctxt',arg::args' -> 
 	  let new_avoid,new_ctxt',new_body,new_id = 
 	    if need_convert_id avoid id 
 	    then 
@@ -139,12 +227,8 @@ let apply_args ctxt body args =
 	      let new_id = Nameops.next_ident_away id new_avoid in 
 	      let new_avoid' = new_id :: new_avoid in 
 	      let mapping = Idmap.add id new_id Idmap.empty in 
-	      let new_ctxt' = 
-		(change_vars_in_binder mapping ctxt')
-	      in 
-	      let new_body = 
-		(change_vars mapping body) 
-	      in 
+	      let new_ctxt' = change_vars_in_binder mapping ctxt' in 
+	      let new_body = change_vars mapping body in 
 	      new_avoid',new_ctxt',new_body,new_id
 	    else 
 	      id::avoid,ctxt',body,id 
@@ -152,24 +236,24 @@ let apply_args ctxt body args =
 	  let new_body = replace_var_by_term new_id arg new_body in
 	  let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
 	  do_apply avoid new_ctxt' new_body args'
-      | (bt,na,t)::ctxt',_ -> 
-	  let new_avoid,new_ctxt',new_body,new_na = 
-	    let new_avoid = add_name na avoid in 
-	    if need_convert avoid na 
+      | (bt,t)::ctxt',_ -> 
+	  let new_avoid,new_ctxt',new_body,new_bt = 
+	    let new_avoid = add_bt_names bt avoid in 
+	    if need_convert avoid bt 
 	    then 
-	      let new_na,mapping,new_avoid = next_name_away na new_avoid in 
-	     (
-	       new_avoid,
-	       change_vars_in_binder mapping ctxt',
-	       change_vars mapping body,
-	       new_na
+	      let new_bt,mapping,new_avoid = next_bt_away bt new_avoid in 
+	      (
+		new_avoid,
+		change_vars_in_binder mapping ctxt',
+		change_vars mapping body,
+		new_bt
 	     )
-	    else new_avoid,ctxt',body,na
+	    else new_avoid,ctxt',body,bt
 	  in
 	  let new_ctxt',new_body = 
 	    do_apply new_avoid new_ctxt' new_body args 
 	  in
-	  (bt,new_na,t)::new_ctxt',new_body
+	  (new_bt,t)::new_ctxt',new_body
   in 
   do_apply []  ctxt body args
 
@@ -195,10 +279,16 @@ let combine_lam n t b =
 
 
 let combine_prod n t b = 
-  { context = t.context@((Prod,n,t.value)::b.context); value = b.value}
+  { context = t.context@((Prod n,t.value)::b.context); value = b.value}
 
 let combine_letin n t b = 
-  { context = t.context@((LetIn,n,t.value)::b.context); value = b.value}
+  { context = t.context@((LetIn n,t.value)::b.context); value = b.value}
+
+(* let combine_tuple nal na b in_e =  *)
+(*   {  *)
+(*     context = b.context@(LetTuple(nal,na),b.value)::in_e.context;  *)
+(*     value = in_e.value *)
+(*   } *)
 
 let mk_result ctxt value avoid = 
   { 
@@ -235,7 +325,8 @@ let make_discr_match brl =
 	   make_discr_match_brl i brl)
   
 
-let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return (* (raw_context*rawconstr) list  *)= 
+let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return = 
+(*   Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *)
   match rt with 
     | RRef _ | RVar _ | REvar _ | RPatVar _     | RSort _  | RHole _  -> 
 	mk_result [] rt avoid
@@ -260,8 +351,8 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return (* (raw
 		  List.map 
 		    (fun arg_res -> 
 		       let new_hyps = 
-			 [Prod,Name res,mkRHole ();
-			  Prod,Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
+			 [Prod (Name res),mkRHole ();
+			  Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
 		       in
 		       {context =  arg_res.context@new_hyps; value = res_rt } 
 		    )
@@ -323,8 +414,8 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return (* (raw
     | RCases(_,_,el,brl) -> 
 	let make_discr = make_discr_match brl in 
 	build_entry_lc_from_case funnames make_discr el brl avoid
-    | RLetTuple _ -> error "Not handled RLetTuple"
     | RIf _ -> error "Not handled RIf"
+    | RLetTuple _ -> error "Not handled RLetTuple"
     | RRec _ -> error "Not handled RRec"
     | RCast _ -> error "Not handled RCast"
     | RDynamic _ -> error "Not handled RDynamic"
@@ -394,13 +485,13 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 	    avoid
 	    matched_expr
 	in
-	let ids = List.map (fun id -> Prod,Name id,mkRHole ()) idl in 
+	let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in 
       	let those_pattern_preconds =
 	  (
 	    List.map2
 	      (fun pat e -> 
 		 let pat_as_term = pattern_to_term pat in 
-		 (Prod,Anonymous,raw_make_eq pat_as_term e)
+		 (Prod Anonymous,raw_make_eq pat_as_term e)
 	      )
 	      patl
 	      matched_expr.value
@@ -413,42 +504,10 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 		List.for_all (fun x -> x) unif) patterns_to_prevent
 	      then 
 		let i = List.length patterns_to_prevent in 
-		[(Prod,Anonymous,make_discr (List.map pattern_to_term patl) i  )]
+		[(Prod Anonymous,make_discr (List.map pattern_to_term patl) i  )]
 	      else 
 		[]
 	      )
-(* 	    List.fold_right *)
-(* 	    (fun (unifl,neql) acc -> *)
-(* 	       let unif,eqs : bool list * bool list =  *)
-(* 		 List.split (List.map2 (fun x y -> x y) unifl patl) *)
-(* 	       in *)
-(* 	       (\* all the pattern must be unifiables *\) *)
-(* 	       if List.for_all (fun x -> x) unif (\* List.for_all2 (fun unif pat -> unif pat) unifl patl *\) *)
-(* 	       then *)
-(* 		 let precond = *)
-(* 		   List.map2 *)
-(* 		     (fun neq pat -> *)
-(* 			let pat_as_term = pattern_to_term pat in  *)
-(* 			(neq new_avoid pat_as_term) *)
-(* 		     ) *)
-(* 		     neql patl *)
-(* 		 in *)
-(* 		 let precond =  *)
-(* 		   List.fold_right2  *)
-(* 		     (fun precond eq acc ->  *)
-(* 			if not eq then precond::acc else acc *)
-(* 		     ) *)
-(* 		     precond  *)
-(* 		     eqs *)
-(* 		     [] *)
-(* 		 in				        *)
-(* 		 try *)
-(* 		   (Prod,Anonymous,raw_make_or_list precond)::acc *)
-(* 		 with Invalid_argument "mk_or" -> acc *)
-(* 	       else acc *)
-(* 	    ) *)
-(* 	    patterns_to_prevent *)
-(* 	    [] *)
 	in
 	let return_res = build_entry_lc funname new_avoid return in
 	let this_branch_res =
@@ -462,103 +521,6 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 	in
 	{ brl'_res with result = this_branch_res@brl'_res.result }
 
-
-
-(* and build_entry_lc_from_case_term funname patterns_to_prevent brl avoid *)
-(*     matched_expr = *)
-(*   match brl with *)
-(*     | [] -> (\* computed_branches  *\) {result = [];to_avoid = avoid} *)
-(*     | br::brl' -> *)
-(* 	let _,idl,patl,return = alpha_br avoid br in *)
-(* 	let new_avoid  = idl@avoid in  *)
-(* 	let e_ctxt,el = (matched_expr.context,matched_expr.value) in *)
-(* 	if  (List.length patl) <> (List.length el) *)
-(* 	then error ("Pattern matching on product: not yet implemented"); *)
-(* 	let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list =  *)
-(* 	  List.map  *)
-(* 	    (fun pat ->  *)
-(* 	       fun avoid pat'_as_term ->  *)
-(* 		 let renamed_pat,_,_ = alpha_pat avoid pat in *)
-(* 		 let pat_ids = get_pattern_id renamed_pat  in  *)
-(* 		 List.fold_right  *)
-(* 		   (fun id acc -> mkRProd (Name id,mkRHole (),acc)) *)
-(* 		   pat_ids *)
-(* 		   (raw_make_neq pat'_as_term (pattern_to_term renamed_pat)) *)
-(* 	    ) *)
-(* 	    patl *)
-(* 	in *)
-(* 	let unify_with_those_patterns : (cases_pattern -> bool*bool) list = *)
-(* 	  List.map (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat') patl *)
-(* 	in *)
-(* 	let brl'_res = *)
-(* 	  build_entry_lc_from_case_term *)
-(* 	    funname *)
-(* 	    ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent) *)
-(* 	    brl' *)
-(* 	    avoid *)
-(* 	    matched_expr *)
-(* 	in *)
-(* 	let ids = List.map (fun id -> Prod,Name id,mkRHole ()) idl in  *)
-(*       	let those_pattern_preconds = *)
-(* 	  ( *)
-(* 	    List.map2 *)
-(* 	      (fun pat e ->  *)
-(* 		 let pat_as_term = pattern_to_term pat in  *)
-(* 		 (Prod,Anonymous,raw_make_eq pat_as_term e) *)
-(* 	      ) *)
-(* 	      patl *)
-(* 	      el *)
-(* 	  ) *)
-(* 	  @ *)
-(* 	    List.fold_right *)
-(* 	    (fun (unifl,neql) acc -> *)
-(* 	       let unif,eqs : bool list * bool list =  *)
-(* 		 List.split (List.map2 (fun x y -> x y) unifl patl) *)
-(* 	       in *)
-(* 	       (\* all the pattern must be unifiables *\) *)
-(* 	       if List.for_all (fun x -> x) unif (\* List.for_all2 (fun unif pat -> unif pat) unifl patl *\) *)
-(* 	       then *)
-(* 		 let precond = *)
-(* 		   List.map2 *)
-(* 		     (fun neq pat -> *)
-(* 			let pat_as_term = pattern_to_term pat in  *)
-(* 			(neq new_avoid pat_as_term) *)
-(* 		     ) *)
-(* 		     neql patl *)
-(* 		 in *)
-(* 		 let precond =  *)
-(* 		   List.fold_right2  *)
-(* 		     (fun precond eq acc ->  *)
-(* 			if not eq then precond::acc else acc *)
-(* 		     ) *)
-(* 		     precond  *)
-(* 		     eqs *)
-(* 		     [] *)
-(* 		 in				        *)
-(* 		 try *)
-(* 		   (Prod,Anonymous,raw_make_or_list precond)::acc *)
-(* 		 with Invalid_argument "mk_or" -> acc *)
-(* 	       else acc *)
-(* 	    ) *)
-(* 	    patterns_to_prevent *)
-(* 	    [] *)
-(* 	in *)
-(* 	let return_res = build_entry_lc funname new_avoid return in *)
-(* 	let this_branch_res = *)
-(* 	  List.map *)
-(* 	    (fun res  -> *)
-(* 	       { context = e_ctxt@ids@those_pattern_preconds@res.context ; *)
-(* 		 value=res.value} *)
-(* 	    ) *)
-(* 	    return_res.result *)
-(* 	in *)
-(* 	{ brl'_res with result = this_branch_res@brl'_res.result } *)
-
-
-
-
-
-
 	  
 let is_res id = 
   try
@@ -625,13 +587,33 @@ let rec rebuild_cons relname args crossed_types rt =
     | RLetIn(_,n,t,b) -> 
 	begin
 	  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
+	  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 (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
+    | RLetTuple(_,nal,(na,rto),t,b) -> 
+	assert (rto=None);
+	begin
+	  let not_free_in_t id = not (is_free_in id t) in 
+	  let new_t,id_to_exclude' = 
+	    rebuild_cons relname args (crossed_types) 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 (Idset.filter not_free_in_t id_to_exclude) *)
+(* 	    | _ -> *)
+	  RLetTuple(dummy_loc,nal,(na,None),t,new_b),
+		Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
+
+	end
+
     | _ -> mkRApp(mkRVar  relname,args@[rt]),Idset.empty
 
 
@@ -642,14 +624,14 @@ let rec compute_cst_params relnames params = function
       compute_cst_params_from_app [] (params,rtl)
   | RApp(_,f,args) -> 
       List.fold_left (compute_cst_params relnames) params (f::args)
-  | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) -> 
+  | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
       let t_params = compute_cst_params relnames params t in 
       compute_cst_params relnames t_params b
   | RCases _ -> params  (* If there is still cases at this point they can only be 
 			discriminitation ones *)
   | RSort _ -> params
   | RHole _ -> params
-  | RLetTuple _ | RIf _ | RRec _ | RCast _ | RDynamic _  ->
+  | RIf _ | RRec _ | RCast _ | RDynamic _  ->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) = 
   match params,rtl with 
@@ -691,7 +673,7 @@ let compute_params_name relnames args csts =
 
 
 
-let build_inductive funnames funsargs  returned_types (rtl:rawconstr list) =
+let build_inductive parametrize funnames funsargs  returned_types (rtl:rawconstr list) =
   let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
   let funnames = Array.of_list funnames in  
   let funsargs = Array.of_list funsargs in 
@@ -702,20 +684,21 @@ let build_inductive funnames funsargs  returned_types (rtl:rawconstr list) =
   let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in 
   let resa = Array.map (build_entry_lc funnames_as_set []) rta in 
   let constr i res = 
-    List.map (function result (* (args',concl') *) -> 
-		let rt = compose_raw_context result.context result.value in 
-(* 		Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
-		fst (
-		  rebuild_cons relnames.(i)
-		    (List.map (function 
-				   (Anonymous,_) -> mkRVar(fresh_id res.to_avoid "x__") 
-				 | Name id, _ -> mkRVar id
-			      )
-		       funsargs.(i)) 
-		    []
-		    rt 
-		)
-	     ) 
+    List.map 
+      (function result (* (args',concl') *) -> 
+	 let rt = compose_raw_context result.context result.value in 
+(* 	 Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+	 fst (
+	   rebuild_cons relnames.(i)
+	     (List.map (function 
+			    (Anonymous,_) -> mkRVar(fresh_id res.to_avoid "x__") 
+			  | Name id, _ -> mkRVar id
+		       )
+		funsargs.(i)) 
+	     []
+	     rt 
+	 )
+      ) 
       res.result 
   in 
   let next_constructor_id = ref (-1) in 
@@ -728,7 +711,10 @@ let build_inductive funnames funsargs  returned_types (rtl:rawconstr list) =
   in
   let rel_constructors = Array.mapi rel_constructors resa in
   let rels_params = 
-     compute_params_name relnames_as_set funsargs  rel_constructors 
+    if parametrize 
+    then
+      compute_params_name relnames_as_set funsargs  rel_constructors 
+    else []
   in
   let nrel_params = List.length rels_params in
   let rel_constructors = 
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 51977e33d..8119cd674 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -7,6 +7,7 @@
 (*   unit  *)
 
 val build_inductive :
+  bool -> 
   Names.identifier list ->
   (Names.name*Rawterm.rawconstr) list list ->
   Topconstr.constr_expr list ->
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index dbcbb9fbb..f5eda3a7b 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -106,13 +106,20 @@ let change_vars =
 		 change_vars mapping def,
 		 change_vars mapping b
 		)
+      | RLetTuple(_,nal,(na,_),_,_) when List.exists (function Name id -> Idmap.mem id mapping | _ -> false) (na::nal) -> rt 
+      | RLetTuple(loc,nal,(na,rto),b,e) -> 
+	  RLetTuple(loc,
+		    nal, 
+		    (na, option_app (change_vars mapping) rto), 
+		    change_vars mapping b,
+		    change_vars mapping e
+		   )
       | RCases(loc,infos,el,brl) -> 
 	  RCases(loc,
 		 infos,
 		 List.map (fun (e,x) -> (change_vars mapping e,x)) el, 
 		 List.map (change_vars_br mapping) brl
 		)
-      | RLetTuple _ ->error "Not handled RLetTuple"
       | RIf _ -> error "Not handled RIf"
       | RRec _ -> error "Not handled RRec"
       | RSort _ -> rt 
@@ -129,14 +136,6 @@ let change_vars =
   change_vars 
 
 
-let rec change_vars_in_binder mapping = function 
-  | [] -> []
-  | (bt,(Name id as na),t)::l when Idmap.mem id mapping -> 
-      (bt,na,change_vars mapping t):: l 
-  | (bt,na,t)::l -> 
-      (bt,na,change_vars mapping t)::
-	(change_vars_in_binder mapping l)
-
 
 let rec alpha_pat excluded pat = 
   match pat with 
@@ -258,12 +257,41 @@ let rec alpha_rt excluded rt =
 	let new_t = alpha_rt new_excluded t in 
 	let new_b = alpha_rt new_excluded b in 
 	RLetIn(loc,Name new_id,new_t,new_b)
+
+
+    | RLetTuple(loc,nal,(na,rto),t,b) -> 
+	let rev_new_nal,new_excluded,mapping = 
+	  List.fold_left 
+	    (fun (nal,excluded,mapping) na -> 
+	       match na with 
+		 | Anonymous -> (na::nal,excluded,mapping)
+		 | Name id ->  
+		     let new_id = Nameops.next_ident_away id excluded in 
+		     if new_id = id 
+		     then 
+		       na::nal,id::excluded,mapping 
+		     else 
+		       (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping)
+	    )
+	    ([],excluded,Idmap.empty)
+	    nal
+	in
+	let new_nal = List.rev rev_new_nal in 
+	let new_rto,new_t,new_b = 
+	  if Idmap.is_empty mapping
+	  then rto,t,b
+	  else let replace = change_vars mapping in 
+	  (option_app replace rto,replace t,replace b)
+	in
+	let new_t = alpha_rt new_excluded new_t in 
+	let new_b = alpha_rt new_excluded new_b in 
+	let new_rto = option_app (alpha_rt new_excluded) new_rto  in
+	RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
     | RCases(loc,infos,el,brl) -> 
 	let new_el = 
 	  List.map (function (rt,i) -> alpha_rt excluded rt, i) el 
 	in 
 	RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) 
-    | RLetTuple _ -> error "Not handled RLetTuple"
     | RIf _ -> error "Not handled RIf"
     | RRec _ -> error "Not handled RRec"
     | RSort _ -> rt 
@@ -301,22 +329,6 @@ and alpha_br excluded (loc,ids,patl,res) =
 
 
 
-let alpha_ctxt avoid b =
-  let rec alpha_ctxt = function
-    | [] -> [],b
-    | (bt,n,t)::ctxt ->
-	let new_ctxt,new_b = alpha_ctxt ctxt in
-	match n with
-	  | Name id when List.mem id avoid ->
-	      let new_id = Nameops.next_ident_away id avoid in
-	      let mapping = Idmap.add id new_id Idmap.empty in
-	      (bt,Name new_id,t)::
-		(change_vars_in_binder mapping new_ctxt),
-	      change_vars mapping new_b
-	  | _ -> (bt,n,t)::new_ctxt,new_b
-  in
-  alpha_ctxt
-
 (* 
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
@@ -337,10 +349,16 @@ let is_free_in id =
     | RCases(_,_,el,brl) ->
 	(List.exists (fun (e,_) -> is_free_in e) el) ||
 	  List.exists is_free_in_br brl
-    | RLetTuple _ -> raise (UserError("",str "Not handled RLetTuple"))
+
+    | RLetTuple(_,nal,_,b,t) -> 
+	let check_in_nal = 
+	  not (List.exists (function Name id' -> id'= id | _ -> false) nal) 
+	in 
+	is_free_in t  || (check_in_nal && is_free_in b)
+	  
     | RIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
-    | RRec _ -> raise (UserError("",str "Not handled RLetTuple"))
+    | RRec _ -> raise (UserError("",str "Not handled RRec"))
     | RSort _ -> false
     | RHole _ -> false
     | RCast (_,b,_,t) -> is_free_in b || is_free_in t
@@ -410,13 +428,22 @@ let replace_var_by_term x_id term =
 		 replace_var_by_pattern def,
 		 replace_var_by_pattern b
 		)
+      | RLetTuple(_,nal,_,_,_) 
+	  when List.exists (function Name id -> id = x_id | _ -> false) nal  ->  
+	  rt
+      | RLetTuple(loc,nal,(na,rto),def,b) -> 
+	  RLetTuple(loc,
+		    nal,
+		    (na,option_app replace_var_by_pattern rto),
+		    replace_var_by_pattern def,
+		    replace_var_by_pattern b
+		   )
       | RCases(loc,infos,el,brl) -> 
 	  RCases(loc,
 		 infos,
 		 List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, 
 		 List.map replace_var_by_pattern_br brl
 		)
-      | RLetTuple _ -> raise (UserError("",str "Not handled RLetTuple"))
       | RIf _ -> raise (UserError("",str "Not handled RIf"))
       | RRec _ -> raise (UserError("",str "Not handled RRec"))
       | RSort _ -> rt 
@@ -431,13 +458,6 @@ let replace_var_by_term x_id term =
   in
   replace_var_by_pattern 
 
-let rec replace_var_by_term_in_binder x_id term = function 
-  | [] -> [] 
-  | (bt,Name id,t)::l when id_ord id x_id = 0 -> 
-      (bt,Name id,replace_var_by_term x_id term t)::l
-  | (bt,na,t)::l -> 
-      (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l)
-
 
 
 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index fe8a4b6ce..f4bf64613 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -54,9 +54,6 @@ val  raw_make_or_list : rawconstr list -> rawconstr
 (* Replace the var mapped in the rawconstr/context *)
 val change_vars : Names.identifier Names.Idmap.t -> rawconstr -> rawconstr
 
-val change_vars_in_binder :
-  Names.identifier Names.Idmap.t -> ('a*Names.name*rawconstr) list -> 
-  ('a*Names.name*rawconstr) list
 
 
 (* [alpha_pat avoid pat] rename all the variables present in [pat] s.t. 
@@ -89,11 +86,6 @@ val alpha_br : Names.identifier list ->
 val replace_var_by_term  :     
   Names.identifier ->
   Rawterm.rawconstr -> Rawterm.rawconstr -> Rawterm.rawconstr
-val replace_var_by_term_in_binder :
-  Names.identifier ->
-  Rawterm.rawconstr ->
-  ('a * Names.name * Rawterm.rawconstr) list ->
-  ('a * Names.name * Rawterm.rawconstr) list
 
 
 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 43977de32..b07a587d1 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -48,13 +48,15 @@ open Genarg
 let h_intros l = 
   tclMAP h_intro l
 
+let do_observe_tac s tac g =
+  let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+ try let v = tac g in msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); v
+ with e ->
+   msgnl (str "observation "++str s++str " raised exception " ++ 	Cerrors.explain_exn e ++ str "on goal " ++ goal ); raise e;;
+
+
 let observe_tac s tac g = tac g
 
-(* let observe_tac s tac g = *)
-(*   let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in  *)
-(*  try let v = tac g in msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); v *)
-(*  with e -> *)
-(*    msgnl (str "observation "++str s++str " raised an exception on goal " ++ goal ); raise e;; *)
 
 let hyp_ids = List.map id_of_string
     ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res";
@@ -282,7 +284,7 @@ let list_rewrite (rev:bool) (eqs: constr list) =
        (fun eq i -> tclORELSE (rewriteLR eq) i)
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
-let base_leaf (func:global_reference) eqs expr =
+let base_leaf_terminate (func:global_reference) eqs expr =
 (*  let _ = msgnl (str "entering base_leaf") in *)
   (fun g ->
      let ids = pf_ids_of_hyps g in
@@ -454,12 +456,13 @@ let rec introduce_all_values is_mes acc_inv func context_fn
     )
  
 	   
-let rec_leaf is_mes acc_inv hrec (func:global_reference) eqs expr =
+let rec_leaf_terminate is_mes acc_inv hrec (func:global_reference) eqs expr =
   match find_call_occs (mkVar (get_f (constr_of_reference func))) expr with
   | context_fn, args ->
       observe_tac "introduce_all_values" 
 	(introduce_all_values is_mes acc_inv func context_fn eqs  hrec args  [] [])
 
+(* 
 let rec proveterminate is_mes acc_inv (hrec:identifier)  
   (f_constr:constr) (func:global_reference) (eqs:constr list) (expr:constr)  =
 try
@@ -500,6 +503,54 @@ try
 with e -> 
   msgerrnl(str "failure in proveterminate"); 
   raise e
+*)
+let proveterminate is_mes acc_inv (hrec:identifier)  
+  (f_constr:constr) (func:global_reference) base_leaf rec_leaf = 
+  let rec proveterminate (eqs:constr list) (expr:constr)  =
+    try
+      (*  let _ = msgnl (str "entering proveterminate") in *)
+      let v =
+	match (kind_of_term expr) with
+	    Case (_, t, a, l) -> 
+	      (match find_call_occs f_constr a with
+		   _,[] ->
+      		     tclTHENS 
+		       (fun g ->
+			  (* let _ = msgnl(str "entering mkCaseEq") in *)
+			  let v = (mkCaseEq a) g in 
+			  (* let _ = msgnl (str "exiting mkCaseEq") in *)
+			  v
+		       )
+   	               (List.map 
+			  (mk_intros_and_continue true proveterminate eqs)
+			  (Array.to_list l)
+		       )
+		 | _, _::_ -> 
+		     (
+		       match find_call_occs  f_constr expr with
+	     		   _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr)
+			 | _, _:: _ -> 
+			     observe_tac "rec_leaf" 
+			       (rec_leaf is_mes acc_inv hrec  func eqs expr)
+		     )
+	      )
+	  | _ ->  (match find_call_occs  f_constr expr with
+	     	       _,[] -> 
+			 (try 
+			    observe_tac "base_leaf" (base_leaf func eqs expr)
+			  with e -> 
+			    (msgerrnl (str "failure in base case");raise e ))
+		     | _, _::_ -> 
+			 observe_tac "rec_leaf" 
+			   (rec_leaf is_mes acc_inv hrec  func eqs expr)
+		  ) in
+      (*  let _ = msgnl(str "exiting proveterminate") in *)
+      v
+    with e -> 
+      msgerrnl(str "failure in proveterminate"); 
+      raise e
+  in 
+  proveterminate 
 
 let hyp_terminates func = 
   let a_arrow_b = arg_type (constr_of_reference func) in 
@@ -668,6 +719,8 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
 	      hrec
 	      (mkVar f_id)
 	      func
+	      base_leaf_terminate 
+	      rec_leaf_terminate
 	      []
 	      expr
 	   )
@@ -935,7 +988,7 @@ let (com_eqn : identifier ->
      Command.save_named true);;
 
 
-let recursive_definition is_mes f type_of_f r  rec_arg_num eq =
+let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_principle =
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   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 
@@ -969,11 +1022,185 @@ let recursive_definition is_mes f type_of_f r  rec_arg_num eq =
     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;
-      ()
+    let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+    generate_induction_principle
+      functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
+    ()
+
   in
-  com_terminate is_mes functional_ref rec_arg_type relation  rec_arg_num term_id  hook 
+  com_terminate is_mes functional_ref rec_arg_type relation rec_arg_num term_id  hook 
 ;;
 
+
+
+(* let observe_tac = do_observe_tac  *)
+
+let base_leaf_princ eq_cst functional_ref eqs expr = 
+  tclTHENSEQ 
+    [rewriteLR (mkConst eq_cst);
+     list_rewrite true eqs;
+     gen_eauto(* default_eauto *) false (false,5) [] (Some [])
+    ]
+
+
+
+let finalize_rec_leaf_princ_with is_mes hrec acc_inv br = 
+  tclTHENSEQ [
+    Eauto.e_resolve_constr (mkVar br);
+    tclFIRST
+      [
+	e_assumption;
+	reflexivity;
+	tclTHEN (apply (mkVar hrec))
+	  (tclTHENS
+	     (* (try *) (observe_tac "applying inversion" (apply (Lazy.force acc_inv))) 
+(* 	      with e -> Pp.msgnl (Printer.pr_lconstr (Lazy.force acc_inv));raise e *)
+(* 	     ) *)
+	     [ h_assumption
+	     ;
+	       (fun g ->
+	       tclUSER
+		 is_mes
+		 (Some (hrec::(retrieve_acc_var g)))
+		 g
+	       )
+	     ]
+	  );
+	(fun g -> tclIDTAC_MESSAGE (str "here" ++ Printer.pr_goal (sig_it g)) g)
+      ]
+  ]
+    
+let rec_leaf_princ
+    eq_cst
+    branches_names 
+    is_mes
+    acc_inv
+    hrec
+    (functional_ref:global_reference) 
+    eqs
+    expr
+    = 
+  
+  tclTHENSEQ 
+    [ rewriteLR (mkConst eq_cst);
+      list_rewrite true eqs;
+      tclFIRST 
+	(List.map (finalize_rec_leaf_princ_with is_mes hrec acc_inv) branches_names)
+    ]
+
+
+let fresh_id avoid na = 
+  let id =  
+    match na with 
+      | Name id -> id 
+      | Anonymous -> h_id 
+  in 
+  next_global_ident_away true id avoid
+
+
+
+let prove_principle is_mes functional_ref 
+    eq_ref rec_arg_num rec_arg_type nb_args relation = 
+(*  f_ref eq_ref rec_arg_num rec_arg_type nb_args relation *)
+  let eq_cst =   
+    match eq_ref with 
+	ConstRef sp -> sp 
+      | _ -> assert false 
+  in
+  fun g -> 
+    let type_of_goal = pf_concl g in 
+    let goal_ids = pf_ids_of_hyps g in 
+    let goal_elim_infos = compute_elim_sig  (mkRel 0,Rawterm.NoBindings) type_of_goal in 
+    let params_names,ids = List.fold_left 
+      (fun (params_names,avoid) (na,_,_) -> 
+	 let new_id = fresh_id avoid na in 
+	 (new_id::params_names,new_id::avoid)
+      )
+      ([],goal_ids)
+      goal_elim_infos.params
+    in
+    let predicates_names,ids = 
+      List.fold_left 
+	(fun (predicates_names,avoid) (na,_,_) -> 
+	   let new_id = fresh_id avoid na in 
+	   (new_id::predicates_names,new_id::avoid)
+	)
+	([],ids)
+	goal_elim_infos.predicates
+    in
+    let branches_names,ids = 
+      List.fold_left 
+	(fun (branches_names,avoid) (na,_,_) -> 
+	   let new_id = fresh_id avoid na in 
+	   (new_id::branches_names,new_id::avoid)
+	)
+	([],ids)
+	goal_elim_infos.branches
+    in
+    let to_intro = params_names@predicates_names@branches_names in 
+    let nparams = List.length params_names in 
+    let rec_arg_num = rec_arg_num - nparams in 
+    begin 
+      tclTHEN 
+	(h_intros to_intro)
+	(observe_tac (string_of_int (rec_arg_num)) 
+	   (fun g -> 
+	      let ids = ids_of_named_context (pf_hyps g) in
+	      let func_body = (def_of_const (constr_of_reference functional_ref)) in
+(* 	      let _ = Pp.msgnl (Printer.pr_lconstr func_body) in  *)
+	      let (f_name, _, body1) = destLambda func_body in
+	      let f_id =
+		match f_name with
+		  | Name f_id -> next_global_ident_away true f_id ids
+		  | Anonymous -> assert false 
+	      in
+	      let n_names_types,_ = decompose_lam body1 in 
+	      let n_ids,ids = 
+		List.fold_left 
+		  (fun (n_ids,ids) (n_name,_) -> 
+		     match n_name with 
+		       | Name id -> 
+			   let n_id = next_global_ident_away true id ids in 
+			   n_id::n_ids,n_id::ids
+		       | _ -> assert false
+		  )
+		  ([],(f_id::ids))
+		  n_names_types
+	      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 
+	      start 
+		is_mes
+		rec_arg_type
+		ids
+		(snd (list_chop nparams n_ids))
+		(substl (List.map mkVar params_names) relation)
+		(rec_arg_num)
+		rec_arg_id
+		(fun hrec acc_inv g ->  
+		   (proveterminate 
+		      is_mes
+		      acc_inv 
+		      hrec
+		      (mkVar f_id)
+		      functional_ref
+		      (base_leaf_princ eq_cst)
+		      (rec_leaf_princ eq_cst branches_names)
+		      []
+		      expr
+		   )
+		     g 
+		)
+		g )
+	)
+    end
+      g
+
+
+
 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) ] ->
@@ -983,8 +1210,11 @@ VERNAC COMMAND EXTEND RecursiveDefinition
 	| None -> 1
 	| Some n -> n 
     in
-    recursive_definition false f type_of_f r rec_arg_num eq ]
+    recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _  _ -> ())]
 | [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
      "[" ne_constr_list(proof) "]" constr(eq) ] ->
-  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq ]
+  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq  (fun  _ _  _ _ _ _ -> ())]
 END
+
+
+