Cleanning and factorizing code in funind. Spliting new_arg_principles into to files.

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

10 files changed, 2055 insertions, 1837 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
new file mode 100644
index 000000000..0ee8a7e75
--- /dev/null
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -0,0 +1,1435 @@
+open Printer
+open Util
+open Term
+open Termops 
+open Names 
+open Declarations
+open Pp
+open Entries
+open Hiddentac
+open Evd
+open Tacmach
+open Proof_type
+open Tacticals
+open Tactics
+open Indfun_common
+open Libnames
+
+let msgnl = Pp.msgnl
+
+let do_observe () = 
+  Tacinterp.get_debug () <> Tactic_debug.DebugOff  
+
+
+let observe strm =
+  if do_observe ()
+  then Pp.msgnl strm
+  else ()
+
+let observennl strm =
+  if do_observe ()
+  then begin Pp.msg strm;Pp.pp_flush () end
+  else ()
+
+
+
+
+let do_observe_tac s tac g =
+ try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
+ with e ->
+   let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+   msgnl (str "observation "++ s++str " raised exception " ++ 
+	    Cerrors.explain_exn e ++ str " on goal " ++ goal ); 
+   raise e;;
+
+
+let observe_tac s tac g =
+  if do_observe ()
+  then do_observe_tac (str s) tac g
+  else tac g
+
+(* let observe_stream_tac s tac g = *)
+(*   if do_observe () *)
+(*   then do_observe_tac s tac g *)
+(*   else tac g *)
+
+
+
+let tclTRYD tac = 
+  if  !Options.debug  || do_observe ()
+  then (fun g -> try (* do_observe_tac ""  *)tac g with _ -> tclIDTAC g)
+  else tac
+
+
+let list_chop ?(msg="") n l = 
+  try 
+    list_chop n l 
+  with Failure (msg') -> 
+    failwith (msg ^ msg')
+  
+
+let make_refl_eq type_of_t t  =
+  let refl_equal_term = Lazy.force refl_equal in
+  mkApp(refl_equal_term,[|type_of_t;t|])
+
+
+type pte_info = 
+    { 
+      proving_tac : (identifier list ->  Tacmach.tactic);
+      is_valid : constr -> bool
+    }
+
+type ptes_info = pte_info Idmap.t
+
+type 'a dynamic_info = 
+    { 
+      nb_rec_hyps : int;
+      rec_hyps : identifier list ; 
+      eq_hyps : identifier list;
+      info : 'a
+    }
+
+type body_info = constr dynamic_info 
+      
+
+let finish_proof dynamic_infos g = 
+  observe_tac "finish" 
+    ( h_assumption)
+    g
+	  
+
+let refine c = 
+  Tacmach.refine_no_check c
+
+let thin l = 
+  Tacmach.thin_no_check l
+  
+
+let cut_replacing id t tac :tactic= 
+  tclTHENS (cut t)
+    [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
+      tac 
+    ]
+
+let intro_erasing id = tclTHEN (thin [id]) (introduction id)
+
+
+
+let rec_hyp_id = id_of_string "rec_hyp"
+
+let is_trivial_eq t = 
+  match kind_of_term t with 
+    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+	eq_constr t1 t2
+    | _ -> false 
+
+
+let rec incompatible_constructor_terms t1 t2 = 
+  let c1,arg1 = decompose_app t1 
+  and c2,arg2 = decompose_app t2 
+  in 
+  (not (eq_constr t1 t2)) &&
+    isConstruct c1 && isConstruct c2 && 
+    (
+      not (eq_constr c1 c2) || 
+	List.exists2 incompatible_constructor_terms arg1 arg2
+    )
+
+let is_incompatible_eq t = 
+  match kind_of_term t with 
+    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
+	incompatible_constructor_terms t1 t2
+    | _ -> false 
+
+let change_hyp_with_using msg hyp_id t tac : tactic = 
+  fun g -> 
+    let prov_id = pf_get_new_id hyp_id g in 
+    tclTHENS
+      (observe_tac msg (forward (Some  (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
+      [tclTHENLIST 
+      [	
+	observe_tac "change_hyp_with_using thin" (thin [hyp_id]);
+	observe_tac "change_hyp_with_using rename " (h_rename prov_id hyp_id)
+      ]] g
+
+exception TOREMOVE
+
+
+let prove_trivial_eq h_id context (type_of_term,term) = 
+  let nb_intros = List.length context in 
+  tclTHENLIST
+    [
+      tclDO nb_intros intro; (* introducing context *)
+      (fun g -> 
+	 let context_hyps =  
+	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) 
+	 in
+	 let context_hyps' = 
+	   (mkApp(Lazy.force refl_equal,[|type_of_term;term|]))::
+	     (List.map mkVar context_hyps)
+	 in
+	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in 
+	 refine to_refine g
+      )
+    ]
+
+
+let isAppConstruct t = 
+  if isApp t 
+  then isConstruct (fst (destApp t))
+  else false 
+
+
+let nf_betaiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta 
+  
+
+let rec subst_rel_map sub t = 
+  match kind_of_term t with
+  | Rel k -> 
+      begin 
+	try 
+	  Intmap.find (k+1) sub
+	with Not_found -> 
+	  t
+      end
+  | _ -> map_constr (subst_rel_map sub) t
+     
+
+let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
+  let nochange msg  = 
+    begin 
+(*       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    ); *)
+      failwith "NoChange"; 
+    end
+  in    
+  if not (noccurn 1 end_of_type)
+  then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
+    if not (isApp t) then nochange "not an equality";
+    let f_eq,args = destApp t in
+    if not (eq_constr f_eq (Lazy.force eq)) then nochange "not an equality";
+    let t1 = args.(1) 
+    and t2 = args.(2) 
+    and t1_typ = args.(0)
+    in 
+    if not (closed0 t1) then nochange "not a closed lhs";    
+    let rec compute_substitution sub t1 t2 = 
+      if isRel t2 
+      then 
+	let t2 = destRel t2  in 
+	begin 
+	  try 
+	    let t1' = Intmap.find t2 sub in 
+	    if not (eq_constr t1 t1') then nochange "twice bound variable";
+	    sub
+	  with Not_found -> 
+	    assert (closed0 t1);
+	    Intmap.add t2 t1 sub
+	end
+      else if isAppConstruct t1 && isAppConstruct t2 
+      then 
+	begin
+	  let c1,args1 = destApp t1 
+	  and c2,args2 = destApp t2 
+	  in 
+	  if not (eq_constr c1 c2) then anomaly "deconstructing equation";
+	  array_fold_left2 compute_substitution sub args1 args2
+	end
+      else 
+	if (eq_constr t1 t2) then sub else nochange "cannot solve"
+    in
+    let sub = compute_substitution Intmap.empty t1 t2 in 
+    let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) 
+    let new_end_of_type =
+      Intmap.fold
+	(fun i t end_of_type -> lift 1 (substnl  [t] (i-1) end_of_type))
+	sub
+	end_of_type_with_pop
+    in
+    let old_context_length = List.length context + 1 in
+    let witness_fun = 
+      mkLetIn(Anonymous,make_refl_eq t1_typ t1,t,
+	       mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
+	      )
+    in
+    let new_type_of_hyp,ctxt_size,witness_fun = 
+      list_fold_left_i 
+	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> 
+	   try 
+	     let witness = Intmap.find i sub in 
+	     if b' <> None then anomaly "can not redefine a rel!";
+	     (pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
+	   with Not_found  -> 
+	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
+	)
+	1 
+	(new_end_of_type,0,witness_fun)
+	context
+    in
+    let new_type_of_hyp = Reductionops.nf_betaiota  new_type_of_hyp in 
+    let new_ctxt,new_end_of_type = 
+      Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp 
+    in 
+    let prove_new_hyp : tactic = 
+      tclTHEN
+	(tclDO ctxt_size intro)
+	(fun g ->
+	   let all_ids = pf_ids_of_hyps g in 
+	   let new_ids,_  = list_chop ctxt_size all_ids in 
+	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in 
+	   refine to_refine g
+	)
+    in
+    let simpl_eq_tac = 
+      change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp prove_new_hyp
+    in
+(*     observe (str "In " ++ Ppconstr.pr_id hyp_id ++  *)
+(* 	       str "removing an equation " ++ fnl ()++  *)
+(* 	       str "old_typ_of_hyp :=" ++ *)
+(* 	       Printer.pr_lconstr_env *)
+(* 	       env *)
+(* 	       (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) *)
+(* 	     ++ fnl () ++ *)
+(* 	       str "new_typ_of_hyp := "++  *)
+(* 	       Printer.pr_lconstr_env env new_type_of_hyp ++ fnl () *)
+(* 	     ++ str "old context := " ++ pr_rel_context env context ++ fnl ()  *)
+(* 	     ++ str "new context := " ++ pr_rel_context env new_ctxt ++ fnl ()  *)
+(* 	     ++ str "old type  := " ++ pr_lconstr end_of_type ++ fnl ()  *)
+(* 	     ++ str "new type := " ++ pr_lconstr new_end_of_type ++ fnl ()  *)
+(* ); *)
+    new_ctxt,new_end_of_type,simpl_eq_tac
+
+
+let is_property ptes_info t_x full_type_of_hyp = 
+  if isApp t_x 
+  then 
+    let pte,args = destApp t_x in 
+    if isVar pte && array_for_all closed0 args 
+    then 
+      try 
+	let info = Idmap.find (destVar pte) ptes_info in 
+	info.is_valid full_type_of_hyp	  
+      with Not_found -> false 
+    else false 
+  else false 
+
+let isLetIn t = 
+  match kind_of_term t with 
+    | LetIn _ -> true 
+    | _ -> false 
+
+
+let h_reduce_with_zeta = 	 
+  h_reduce 
+    (Rawterm.Cbv
+       {Rawterm.all_flags 
+	with Rawterm.rDelta = false; 		 
+       })
+  
+
+
+let rewrite_until_var arg_num eq_ids : tactic =
+  let test_var g = 
+    let _,args = destApp (pf_concl g) in 
+    isVar args.(arg_num)
+  in
+  let rec do_rewrite eq_ids g  = 
+    if test_var g 
+    then tclIDTAC g
+    else
+      match eq_ids with 
+	| [] -> anomaly "Cannot find a way to prove recursive property";
+	| eq_id::eq_ids -> 
+	    tclTHEN 
+	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+	      (do_rewrite eq_ids)
+	      g
+  in
+  do_rewrite eq_ids
+
+
+let rec_pte_id = id_of_string "Hrec" 
+let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = 
+  let coq_False = Coqlib.build_coq_False () in 
+  let coq_True = Coqlib.build_coq_True () in 
+  let coq_I = Coqlib.build_coq_I () in 
+  let rec scan_type  context type_of_hyp : tactic = 
+    if isLetIn type_of_hyp then 
+      let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
+      let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in 
+      (* length of context didn't change ? *)
+      let new_context,new_typ_of_hyp = 
+	 Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
+      in
+        tclTHENLIST 
+	[
+	  h_reduce_with_zeta
+	    (Tacticals.onHyp hyp_id)
+	  ;
+	  scan_type new_context new_typ_of_hyp 
+	  
+	]
+    else if isProd type_of_hyp 
+    then 
+      begin 
+	let (x,t_x,t') = destProd type_of_hyp in	
+	let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in 
+	if is_property ptes_infos t_x actual_real_type_of_hyp then
+	  begin
+	    let pte,pte_args =  (destApp t_x) in 
+	    let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in 
+	    let popped_t' = pop t' in 
+	    let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in 
+	    let prove_new_type_of_hyp = 
+	      let context_length = List.length context in 
+	      tclTHENLIST
+		[ 
+		  tclDO context_length intro; 
+		  (fun g ->  
+		     let context_hyps_ids = 
+		       fst (list_chop ~msg:"rec hyp : context_hyps"
+			      context_length (pf_ids_of_hyps g))
+		     in
+		     let rec_pte_id = pf_get_new_id rec_pte_id g in 
+		     let to_refine = 
+		       applist(mkVar hyp_id,
+			       List.rev_map mkVar (rec_pte_id::context_hyps_ids)
+			      )
+		     in
+		     observe_tac "rec hyp "
+		       (tclTHENS
+		       (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x)
+		       [observe_tac "prove rec hyp" (prove_rec_hyp eq_hyps);
+			observe_tac "prove rec hyp"
+			  (refine to_refine)
+		       ])
+		       g
+		  )
+		]
+	    in
+	    tclTHENLIST 
+	      [
+		observe_tac "hyp rec" 
+		  (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp);
+		scan_type context popped_t'
+	      ]
+	  end
+	else if eq_constr t_x coq_False then 
+	  begin
+(* 	    observe (str "Removing : "++ Ppconstr.pr_id hyp_id++  *)
+(* 		       str " since it has False in its preconds " *)
+(* 		    ); *)
+	    raise TOREMOVE;  (* False -> .. useless *)
+	  end
+	else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *) 
+	else if eq_constr t_x coq_True  (* Trivial => we remove this precons *)
+	then 
+(* 	    observe (str "In "++Ppconstr.pr_id hyp_id++  *)
+(* 		       str " removing useless precond True" *)
+(* 		    );  *)
+	  let popped_t' = pop t' in
+	  let real_type_of_hyp = 
+	    it_mkProd_or_LetIn ~init:popped_t' context 
+	  in 
+	  let prove_trivial =  
+	    let nb_intro = List.length context in 
+	    tclTHENLIST [
+	      tclDO nb_intro intro;
+	      (fun g -> 
+		 let context_hyps = 
+		   fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
+		 in
+		 let to_refine = 
+		   applist (mkVar hyp_id,
+			    List.rev (coq_I::List.map mkVar context_hyps)
+			   )
+		 in
+		 refine to_refine g
+	      )
+	    ]
+	  in
+	  tclTHENLIST[
+	    change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp 
+	      (observe_tac "prove_trivial" prove_trivial);
+	    scan_type context popped_t'
+	  ]
+	else if is_trivial_eq t_x 
+	then (*  t_x :=  t = t   => we remove this precond *) 
+	  let popped_t' = pop t' in
+	  let real_type_of_hyp =
+	    it_mkProd_or_LetIn ~init:popped_t' context
+	  in
+	  let _,args = destApp t_x in
+	  tclTHENLIST
+	    [
+	      change_hyp_with_using
+		"prove_trivial_eq"
+		hyp_id
+		real_type_of_hyp
+		(observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1))));
+	      scan_type context popped_t'
+	    ] 
+	else 
+	  begin
+	    try 
+	      let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in 
+	      tclTHEN
+		tac 
+		(scan_type new_context new_t')
+	    with Failure "NoChange" -> 
+	      (* Last thing todo : push the rel in the context and continue *) 
+	      scan_type ((x,None,t_x)::context) t'
+	  end
+      end
+    else
+      tclIDTAC
+  in 
+  try 
+    scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
+  with TOREMOVE -> 
+    thin [hyp_id],[]
+
+
+let clean_goal_with_heq ptes_infos continue_tac dyn_infos  = 
+  fun g -> 
+    let env = pf_env g 
+    and sigma = project g 
+    in
+    let tac,new_hyps = 
+      List.fold_left ( 
+	fun (hyps_tac,new_hyps) hyp_id ->
+	  let hyp_tac,new_hyp = 
+	    clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma 
+	  in
+	  (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps
+      )
+	(tclIDTAC,[])
+	dyn_infos.rec_hyps
+    in
+    let new_infos = 
+      { dyn_infos with 
+	  rec_hyps = new_hyps; 
+	  nb_rec_hyps  = List.length new_hyps
+      }
+    in
+    tclTHENLIST 
+      [
+	tac ;
+	(continue_tac new_infos)
+      ]
+      g    
+
+let heq_id = id_of_string "Heq"
+
+let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = 
+  fun g -> 
+    let heq_id = pf_get_new_id heq_id g in 
+    let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
+    tclTHENLIST
+      [ 
+	(* We first introduce the variables *) 
+	tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
+	(* Then the equation itself *)
+	introduction_no_check heq_id;
+	(* Then the new hypothesis *) 
+	tclMAP introduction_no_check dyn_infos.rec_hyps;
+	observe_tac "after_introduction" (fun g' -> 
+	   (* We get infos on the equations introduced*)
+	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in 
+	   (* compute the new value of the body *)
+	   let new_term_value =
+	     match kind_of_term new_term_value_eq with
+	       | App(f,[| _;_;args2 |]) -> args2
+	       | _ ->
+(* 		   observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++ *)
+(* 			      pr_lconstr_env (pf_env g') new_term_value_eq *)
+(* 			   ); *)
+		   anomaly "cannot compute new term value"
+	   in
+	 let fun_body =
+	   mkLambda(Anonymous,
+		    pf_type_of g' term,
+		    replace_term term (mkRel 1) dyn_infos.info
+		   )
+	 in
+	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
+	 let new_infos = 
+	   {dyn_infos with 
+	      info = new_body;
+	      eq_hyps = heq_id::dyn_infos.eq_hyps
+	   }
+	 in 
+	 clean_goal_with_heq ptes_infos continue_tac new_infos  g'
+      )
+    ]
+      g
+
+
+let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = 
+  let args = Array.of_list (List.map mkVar  args_id) in 
+  let instanciate_one_hyp hid = 
+    tclORELSE
+      ( (* we instanciate the hyp if possible  *)
+	fun g -> 
+	  let prov_hid = pf_get_new_id hid g in
+	  tclTHENLIST[
+	    forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+	    thin [hid];
+	    h_rename prov_hid hid
+	  ] g
+      )
+      ( (*
+	  if not then we are in a mutual function block 
+	  and this hyp is a recursive hyp on an other function.
+	  
+	  We are not supposed to use it while proving this 
+	  principle so that we can trash it 
+	  
+	*)
+	(fun g -> 
+(* 	   observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *)
+	   thin [hid] g
+	)
+      )
+  in
+  if args_id = []  
+  then 
+    tclTHENLIST [
+      tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+      do_prove hyps
+    ]
+  else
+    tclTHENLIST
+      [
+	tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+	tclMAP instanciate_one_hyp hyps;
+	(fun g ->  
+	   let all_g_hyps_id = 
+	     List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
+	   in 
+	   let remaining_hyps = 
+	     List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
+	   in
+	   do_prove remaining_hyps g
+	  )
+      ]
+
+let build_proof 
+    (interactive_proof:bool)
+    (fnames:constant list)
+    ptes_infos
+    dyn_infos
+    : tactic =
+  let rec build_proof_aux do_finalize dyn_infos : tactic = 
+    fun g -> 
+      
+(*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
+	match kind_of_term dyn_infos.info with 
+	  | Case(_,_,t,_) -> 
+	      let g_nb_prod = nb_prod (pf_concl g) in
+	      let type_of_term = pf_type_of g t in
+	      let term_eq =
+		make_refl_eq type_of_term t
+	      in
+  	      tclTHENSEQ
+		[
+		  h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps);
+		  thin dyn_infos.rec_hyps;
+		  pattern_option [[-1],t] None;
+		  h_simplest_case t;
+		  (fun g' -> 
+		     let g'_nb_prod = nb_prod (pf_concl g') in 
+		     let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
+		     observe_tac "treat_new_case" 
+		       (treat_new_case  
+		       ptes_infos
+		       nb_instanciate_partial 
+		       (build_proof do_finalize) 
+		       t 
+		       dyn_infos)
+		       g'
+		  )
+		  
+		] g
+	  | Lambda(n,t,b) ->
+	      begin
+		match kind_of_term( pf_concl g) with
+		  | Prod _ ->
+		      tclTHEN
+			intro
+			(fun g' ->
+			   let (id,_,_) = pf_last_hyp g' in
+			   let new_term = 
+			     pf_nf_betaiota g' 
+			       (mkApp(dyn_infos.info,[|mkVar id|])) 
+			   in
+			   let new_infos = {dyn_infos with info = new_term} in
+			   let do_prove new_hyps = 
+			     build_proof do_finalize 
+			       {new_infos with
+			       	  rec_hyps = new_hyps; 
+				  nb_rec_hyps  = List.length new_hyps
+			       }
+			   in 
+			   observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
+			     (* 			   build_proof do_finalize new_infos g' *)
+			) g
+		  | _ ->
+		      do_finalize dyn_infos g 
+	      end
+	  | Cast(t,_,_) -> 
+	      build_proof do_finalize {dyn_infos with info = t} g
+	  | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+	      do_finalize dyn_infos g
+	  | App(_,_) ->
+	      let f,args = decompose_app dyn_infos.info in
+	      begin
+		match kind_of_term f with
+		  | App _ -> assert false (* we have collected all the app in decompose_app *)
+		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
+		      let new_infos = 
+			{ dyn_infos with 
+			    info = (f,args)
+			}
+		      in
+		      build_proof_args do_finalize new_infos  g
+		  | Const c when not (List.mem c fnames) ->
+		      let new_infos = 
+			{ dyn_infos with 
+			    info = (f,args)
+			}
+		      in
+(* 		      Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
+		      build_proof_args do_finalize new_infos g
+		  | Const _ ->
+		      do_finalize dyn_infos  g
+		  | Lambda _ -> 
+		      let new_term = Reductionops.nf_beta dyn_infos.info in 
+		      build_proof do_finalize {dyn_infos with info = new_term} 
+			g
+		  | LetIn _ -> 
+		      let new_infos = 
+			{ dyn_infos with info = nf_betaiotazeta dyn_infos.info } 
+		      in 
+
+		      tclTHENLIST 
+			[tclMAP 
+			   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
+			   dyn_infos.rec_hyps;
+			 h_reduce_with_zeta Tacticals.onConcl;
+			 build_proof do_finalize new_infos
+			] 
+			g
+		  | Cast(b,_,_) -> 
+		      build_proof do_finalize {dyn_infos with info = b } g
+		  | Case _ | Fix _ | CoFix _ ->
+		      let new_finalize dyn_infos = 
+			let new_infos = 
+			  { dyn_infos with 
+			      info = dyn_infos.info,args
+			  }
+			in 
+			build_proof_args do_finalize new_infos 
+		      in 
+		      build_proof new_finalize {dyn_infos  with info = f } g
+	      end
+	  | Fix _ | CoFix _ ->
+	      error ( "Anonymous local (co)fixpoints are not handled yet")
+
+	  | Prod _ -> error "Prod" 
+	  | LetIn _ -> 
+	      let new_infos = 
+		{ dyn_infos with 
+		    info = nf_betaiotazeta dyn_infos.info 
+		}
+	      in 
+
+	      tclTHENLIST 
+		[tclMAP 
+		   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
+		   dyn_infos.rec_hyps;
+		 h_reduce_with_zeta Tacticals.onConcl;
+		 build_proof do_finalize new_infos
+		] g
+	  | Rel _ -> anomaly "Free var in goal conclusion !" 
+  and build_proof do_finalize dyn_infos g =
+(*     observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *)
+     (build_proof_aux do_finalize dyn_infos) g
+  and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
+    fun g ->
+(*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
+(*      then msgnl (str "build_proof_args with "  ++  *)
+(* 		   pr_lconstr_env (pf_env g) f_args' *)
+(* 		); *)
+      let (f_args',args) = dyn_infos.info in 
+      let tac : tactic =
+	fun g -> 
+	match args with
+	  | []  ->
+	      do_finalize {dyn_infos with info = f_args'} g 
+	  | arg::args ->
+(* 		observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
+(* 			fnl () ++  *)
+(* 			pr_goal (Tacmach.sig_it g) *)
+(* 			); *)
+	      let do_finalize dyn_infos =
+		let new_arg = dyn_infos.info in 
+		(* 		tclTRYD *)
+		(build_proof_args
+		   do_finalize
+		   {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
+		)
+	      in
+	      build_proof do_finalize 
+		{dyn_infos with info = arg }
+		g
+      in
+      observe_tac "build_proof_args" (tac ) g
+   in
+   let do_finish_proof dyn_infos = 
+     (* tclTRYD *) (clean_goal_with_heq 
+      ptes_infos
+      finish_proof dyn_infos)
+  in
+  observe_tac "build_proof"
+    (build_proof do_finish_proof dyn_infos) 
+
+
+
+
+
+
+
+
+
+
+
+
+(* Proof of principles from structural functions *) 
+let is_pte_type t =
+  isSort (snd (decompose_prod t))
+    
+let is_pte (_,_,t) = is_pte_type t
+
+
+
+
+type static_fix_info = 
+    {
+      idx : int;
+      name : identifier;
+      types : types;
+      nb_realargs : int
+    }
+
+let prove_rec_hyp fix_info  =
+  { proving_tac = 
+      (fun  eq_hyps -> tclTHEN 
+	(rewrite_until_var (fix_info.idx - 1) eq_hyps)
+	(fun g -> 
+	   let _,pte_args = destApp (pf_concl g) in 
+	   let rec_hyp_proof = 
+	     mkApp(mkVar fix_info.name,array_get_start pte_args) 
+	   in
+	   refine rec_hyp_proof g
+	))
+  ;
+    is_valid = fun _ -> true 
+  }
+
+
+exception Not_Rec
+    
+
+let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic =
+   fun goal ->
+(*      observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++  *)
+(* 		pr_lconstr (mkConst fnames.(fun_num))); *)
+     let princ_type = pf_concl goal in
+     let princ_info = compute_elim_sig princ_type in
+     let get_body const =
+       match (Global.lookup_constant const ).const_body with
+	 | Some b ->
+	     let body = force b in
+	     Tacred.cbv_norm_flags
+	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+	       (Global.env ())
+	       (Evd.empty)
+	       body
+	 | None -> error ( "Cannot define a principle over an axiom ")
+     in
+     let fbody = get_body fnames.(fun_num) in
+     let params : identifier list ref = ref [] in
+     let predicates : identifier list ref = ref [] in
+     let args : identifier list ref = ref [] in
+     let branches : identifier list ref = ref [] in
+     let pte_to_fix = ref Idmap.empty in
+     let fbody_with_params = ref None in
+     let intro_with_remembrance  ref number : tactic =
+       tclTHEN
+	 ( tclDO number intro )
+	 (fun g ->
+	    let last_n = list_chop number (pf_hyps g) in
+	    ref :=  List.map (fun (id,_,_) -> id) (fst last_n)@ !ref;
+	    tclIDTAC g
+	 )
+     in
+     let rec partial_combine body params =
+       match kind_of_term body,params with
+	 | Lambda (x,t,b),param::params ->
+	     partial_combine (subst1 param b) params
+	 | Fix(infos),_ ->
+	     body,params, Some (infos)
+	 | _ -> body,params,None
+     in
+     let build_pte_to_fix (offset:int) params predicates
+	 ((idxs,fix_num),(na,typearray,ca))  (avoid,_) =
+(*        let true_params,_ =  list_chop offset params  in  *)
+       let true_params = List.rev params in
+       let avoid = ref avoid in
+       let res = list_fold_left_i
+	 (fun i acc pte_id  ->
+	    let this_fix_id = fresh_id !avoid "fix___" in
+	    avoid := this_fix_id::!avoid;
+(* 	    let this_body = substl (List.rev fnames_as_constr) ca.(i) in  *)
+	    let realargs,_ = decompose_lam ca.(i) in 
+	    let n_realargs = List.length realargs - List.length params in 
+(* 	    observe (str "n_realargs := " ++ str (string_of_int n_realargs)); *)
+(* 	    observe (str "n_fix := " ++ str (string_of_int(Array.length ca))); *)
+(* 	    observe (str "body := " ++ pr_lconstr ca.(i)); *)
+
+	    let new_type = prod_applist typearray.(i) true_params in
+	    let new_type_args,_ = decompose_prod new_type in
+	    let nargs = List.length new_type_args in
+	    let pte_args =
+	      (* 	      let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in  *)
+	      let f = applist((* all_funs *)mkConst fnames.(i),true_params) in
+	      let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in
+	      (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f]
+	    in
+	    let app_pte = applist(mkVar pte_id,pte_args) in
+	    let new_type = compose_prod new_type_args app_pte in
+	    
+	    let fix_info = 
+	      {
+		idx = idxs.(i) - offset + 1;
+		name = this_fix_id; 
+		types = new_type;
+		nb_realargs = n_realargs
+	      }
+	    in
+	    pte_to_fix := Idmap.add  pte_id fix_info !pte_to_fix;
+	    fix_info::acc
+	 )
+	 0
+	 []
+	 predicates
+       in
+       !avoid,List.rev res
+     in
+     let mk_fixes : tactic =
+       fun g ->
+	 let body_p,params',fix_infos =
+	   partial_combine fbody (List.rev_map mkVar  !params)
+	 in
+	 fbody_with_params := Some body_p;
+	 let offset  = List.length params' in
+	 let not_real_param,true_params =
+	   list_chop
+	     ((List.length !params ) - offset)
+	     !params
+	 in
+	 params := true_params; args := not_real_param;
+(* 	 observe (str "mk_fixes : params are "++  *)
+(* 		    prlist_with_sep spc *)
+(* 		    (fun id -> pr_lconstr (mkVar id)) *)
+(* 		    !params *)
+(* 		 ); *)
+	 let new_avoid,infos =
+	   option_fold_right
+	     (build_pte_to_fix
+		offset
+		(List.map mkVar !params)
+		(List.rev !predicates)
+	     )
+	     fix_infos
+	     ((pf_ids_of_hyps g),[])
+	 in
+	 let pre_info,infos = list_chop fun_num infos in
+	 match pre_info,infos with
+	   | [],[] -> tclIDTAC g
+	   | _,this_fix_info::infos' ->
+	       let other_fix_info =
+		 List.map 
+		   (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types) 
+		   (pre_info@infos')
+	       in
+	       if other_fix_info = []
+		  then h_fix (Some this_fix_info.name) this_fix_info.idx g
+		  else h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info g
+	   | _,[] -> anomaly "Not a valid information"
+     in
+     let do_prove ptes_to_fixes args branches : tactic =
+       fun g ->
+	 let nb_intros_to_do = List.length (fst (Sign.decompose_prod_assum (pf_concl g))) in 
+(* 	 observe (str "nb_intros_to_do " ++ str (string_of_int nb_intros_to_do)); *)
+	 tclTHEN 
+	   (tclDO nb_intros_to_do intro)
+	   (fun g -> 
+	      match kind_of_term (pf_concl g) with
+		| App(pte,pte_args) when isVar pte ->
+		    begin
+		      let pte = destVar pte in
+		      try
+			if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec;
+			let nparams = List.length !params in
+			let args_as_constr = List.map mkVar  args in
+			let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in 
+			let other_args_as_constr = List.map mkVar  other_args in 
+			let rec_num,new_body =
+			  let idx' = list_index pte (List.rev !predicates)  - 1 in
+			  let f = fnames.(idx') in
+			  let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly ""
+			  in
+			  let name_of_f = Name ( id_of_label (con_label f)) in
+			  let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in
+			  let idx'' = list_index name_of_f (Array.to_list na) - 1 in
+			  let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in
+			  let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in
+			  rec_nums.(idx'') - nparams ,body
+			in
+			let applied_body_with_real_args =
+			  Reductionops.nf_betaiota
+			    (applist(new_body,List.rev args_as_constr))
+			in
+			let applied_body = 
+(* 			  Reductionops.nf_beta *)
+			  Reductionops.nf_betaiota 
+			    (applist(applied_body_with_real_args,List.rev other_args_as_constr))
+			in
+(* 			observe (str "applied_body_with_real_args := "++ pr_lconstr_env (pf_env g) applied_body_with_real_args); *)
+(* 			observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body); *)
+			let do_prove branches applied_body =
+			  build_proof
+			    interactive_proof
+			    (Array.to_list fnames)
+			    (Idmap.map prove_rec_hyp ptes_to_fixes)
+			    branches
+			    applied_body
+			in
+			let replace_and_prove =
+			  tclTHENS
+			    (fun g -> (Equality.replace (array_last pte_args) applied_body) g)
+			    [
+			      tclTHENLIST 
+				[
+				  generalize other_args_as_constr;
+				  thin other_args;
+				  clean_goal_with_heq 
+				    (Idmap.map prove_rec_hyp ptes_to_fixes)
+				    do_prove 
+				    {
+				      nb_rec_hyps = List.length branches;
+				      rec_hyps = branches;
+				      info = applied_body_with_real_args;
+				      eq_hyps = [];
+				    } ];
+			      let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in
+			      let id_as_induction_constr = Tacexpr.ElimOnConstr id in 
+			      (tclTHENSEQ
+				 [Tactics.new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *)
+				  Tactics.intros_reflexivity
+				 ])
+			    ]
+			in
+			(observe_tac "doing replacement" ( replace_and_prove)) g
+		      with Not_Rec ->
+			let fname = destConst (fst (decompose_app (array_last pte_args))) in
+			tclTHEN
+		     (unfold_in_concl [([],Names.EvalConstRef fname)])
+			  (observe_tac "" 
+			     (fun g' ->
+				let body = array_last (snd (destApp (pf_concl g'))) in 
+				let dyn_infos = 
+				  { nb_rec_hyps = List.length branches;
+				    rec_hyps = branches;
+				    info = body;
+				    eq_hyps = []
+				  }
+				in
+				let do_prove = 
+				  build_proof
+				    interactive_proof
+				    (Array.to_list fnames)
+				    (Idmap.map prove_rec_hyp ptes_to_fixes)
+				in
+				clean_goal_with_heq (Idmap.map prove_rec_hyp ptes_to_fixes)
+				  do_prove dyn_infos g'
+			     )
+			  )
+			  g
+		    end
+		| _ -> assert false
+	   ) g
+     in
+     tclTHENSEQ
+       [
+	 (fun g -> observe_tac "introducing params" (intro_with_remembrance  params princ_info.nparams) g);
+	 (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates  princ_info.npredicates) g);
+	 (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g);
+	 (fun g -> observe_tac "declaring fix(es)" mk_fixes g);
+	 (fun g -> 
+	    let nb_real_args = 
+	      let pte_app = snd (Sign.decompose_prod_assum (pf_concl g)) in 
+	      let pte = fst (decompose_app pte_app) in
+	      try 
+		let fix_info = Idmap.find (destVar pte) !pte_to_fix in
+		fix_info.nb_realargs
+	      with Not_found -> (* Not a recursive function *) 
+		nb_prod (pf_concl g)
+	    in 
+	    observe_tac "" (tclTHEN
+	      (tclDO nb_real_args (observe_tac "intro" intro)) 
+	      (fun g' -> 
+		 let realargs_ids = fst (list_chop ~msg:"args" nb_real_args (pf_ids_of_hyps g')) in 
+		 let do_prove_on_branches branches : tactic =
+		   observe_tac "proving" (do_prove !pte_to_fix ( realargs_ids) branches)
+		 in
+		 observe_tac "instanciating rec hyps"
+		   (instanciate_hyps_with_args do_prove_on_branches !branches  (List.rev realargs_ids))
+		   g'
+	      ))
+	      g
+	 )
+       ]
+       goal
+
+
+
+(* Proof of principles of general functions *) 
+let h_id = Recdef.h_id
+and hrec_id = Recdef.hrec_id
+and acc_inv_id = Recdef.acc_inv_id
+and ltof_ref = Recdef.ltof_ref
+and acc_rel = Recdef.acc_rel
+and well_founded = Recdef.well_founded
+and delayed_force = Recdef.delayed_force
+and h_intros = Recdef.h_intros
+and list_rewrite = Recdef.list_rewrite
+and evaluable_of_global_reference = Recdef.evaluable_of_global_reference
+
+let prove_with_tcc tcc_lemma_constr eqs : tactic =
+  match !tcc_lemma_constr with
+    | None -> anomaly "No tcc proof !!"
+    | Some lemma ->
+	fun gls ->
+	  let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+	  tclTHENSEQ
+	    [
+	      generalize [lemma];
+	      h_intro hid;
+	      Elim.h_decompose_and (mkVar hid);
+	      tclTRY(list_rewrite true eqs);
+	      Eauto.gen_eauto false (false,5) [] (Some [])
+	    ]
+	    gls
+
+
+let backtrack_eqs_until_hrec hrec eqs : tactic = 
+  fun gls -> 
+    let rewrite = 
+      tclFIRST (List.map Equality.rewriteRL eqs )
+    in 
+    let _,hrec_concl  = decompose_prod (pf_type_of gls (mkVar hrec)) in 
+    let f_app = array_last (snd (destApp hrec_concl)) in 
+    let f =  (fst (destApp f_app)) in 
+    let rec backtrack : tactic = 
+      fun g -> 
+	let f_app = array_last (snd (destApp (pf_concl g))) in 
+	match kind_of_term f_app with 
+	  | App(f',_) when eq_constr f' f -> tclIDTAC g
+	  | _ -> tclTHEN rewrite backtrack g
+    in
+    backtrack gls
+
+    
+    
+  
+
+let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic = 
+  match !tcc_lemma_constr with 
+    | None -> tclIDTAC_MESSAGE (str "No tcc proof !!")
+    | Some lemma -> 
+	fun gls ->
+	  let hid = next_global_ident_away true Recdef.h_id (pf_ids_of_hyps gls) in 
+	    (tclTHENSEQ 
+	    [
+	      generalize [lemma];
+	      h_intro hid;
+	      Elim.h_decompose_and (mkVar hid); 
+	      backtrack_eqs_until_hrec hrec eqs;
+	      tclCOMPLETE (tclTHENS  (* We must have exactly ONE subgoal !*)
+		(apply (mkVar hrec))
+		[ tclTHENSEQ 
+		    [
+			 thin [hrec];
+			 apply (Lazy.force acc_inv);
+			 (fun g -> 
+			    if is_mes 
+			    then 
+			      unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g 
+			    else tclIDTAC g
+			 );
+			 tclTRY(Recdef.list_rewrite true eqs);
+			 observe_tac "finishing"  (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))
+		       ]
+		]
+			  )
+	    ])
+	    gls
+
+
+let is_valid_hypothesis predicates_name =
+  let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in
+  let is_pte typ =
+    if isApp typ
+    then
+      let pte,_ = destApp typ in
+      if isVar pte
+      then Idset.mem (destVar pte) predicates_name
+      else false
+    else false
+  in
+  let rec is_valid_hypothesis typ =
+    is_pte typ ||
+      match kind_of_term typ with 
+	| Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
+	| _ -> false 
+  in
+  is_valid_hypothesis 
+
+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_for_gen
+    (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
+    rec_arg_num rec_arg_type relation = 
+  fun g -> 
+    let type_of_goal = pf_concl g in 
+    let goal_ids = pf_ids_of_hyps g in 
+    let goal_elim_infos = Tactics.compute_elim_sig 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 
+    let tac_intro_static = h_intros to_intro in 
+    let args_info = ref None in 
+    let arg_tac g =  (* introducing args *)
+      let ids = pf_ids_of_hyps g in 
+      let func_body = def_of_const (mkConst 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 -> anomaly "anonymous function"
+      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
+	       | _ -> anomaly "anonymous argument"
+	  )
+	  ([],(f_id::ids))
+	  n_names_types
+      in
+      let rec_arg_id = List.nth n_ids (rec_arg_num - 1 ) in
+      let args_ids = snd (list_chop nparams n_ids) in
+      args_info := Some (ids,args_ids,rec_arg_id);
+      h_intros args_ids g
+    in
+    let wf_tac = 
+      if is_mes 
+      then 
+	Recdef.tclUSER_if_not_mes 
+      else fun _ -> prove_with_tcc tcc_lemma_ref []
+    in
+    let start_tac g = 
+      let ids,args_ids,rec_arg_id = out_some !args_info in
+      let nargs = List.length args_ids in 
+      let pre_rec_arg = 
+	List.rev_map 
+	  mkVar 
+	  (fst (list_chop (rec_arg_num - 1) args_ids))
+      in
+      let args_before_rec = pre_rec_arg@(List.map mkVar params_names) in
+      let relation = substl args_before_rec relation in 
+      let input_type = substl args_before_rec rec_arg_type in 
+      let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in 
+      let wf_rec_arg = 
+	next_global_ident_away true 
+	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
+	  (wf_thm::ids) 
+      in 
+      let hrec = next_global_ident_away true hrec_id (wf_rec_arg::wf_thm::ids) in 
+      let acc_inv = 
+	lazy (
+	  mkApp (
+	    delayed_force acc_inv_id,
+	    [|input_type;relation;mkVar rec_arg_id|]
+	  )
+	)
+      in
+      (tclTHENS
+	   (observe_tac 
+	      "first assert" 
+	      (assert_tac 
+		 true (* the assert thm is in first subgoal *)
+		 (Name wf_rec_arg) 
+		 (mkApp (delayed_force acc_rel,
+			 [|input_type;relation;mkVar rec_arg_id|])
+		 )
+	      )
+	   )
+	   [
+	     (* accesibility proof *) 
+	     tclTHENS 
+	       (observe_tac 
+		  "second assert" 
+		  (assert_tac 
+		     true 
+		     (Name wf_thm)
+		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
+		  )
+	       )
+	       [ 
+		 (* interactive proof of the well_foundness of the relation *) 
+		 wf_tac is_mes;
+		 (* well_foundness -> Acc for any element *)
+		 observe_tac 
+		   "apply wf_thm" 
+		   (h_apply ((mkApp(mkVar wf_thm,
+				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+		   )
+	       ]
+	     ;
+	     (* rest of the proof *)
+	     tclTHENSEQ
+	       [
+		 observe_tac "generalize" (fun g -> 
+		    let to_thin = 
+		      fst (list_chop ( nargs + 1) (pf_ids_of_hyps g))
+		    in
+		    let to_thin_c = List.rev_map mkVar to_thin in 
+		    tclTHEN (generalize to_thin_c) (observe_tac "thin" (h_clear false to_thin)) g
+		 );
+		 observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
+		h_intros args_ids;
+		h_intro wf_rec_arg;
+		Equality.rewriteLR (mkConst eq_ref);
+		(fun g' -> 
+		   let body = 
+		     let _,args = destApp (pf_concl g') in 
+		     array_last args
+		   in
+		   let body_info rec_hyps = 
+		     {
+		       nb_rec_hyps = List.length rec_hyps;
+		       rec_hyps = rec_hyps;
+		       eq_hyps = [];
+		       info = body
+		     }
+		   in 
+		   let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  wf_rec_arg|]) )  in
+		   let pte_info = 
+		     { proving_tac =
+			 (fun eqs -> 
+			    observe_tac "prove_with_tcc" 
+			      (new_prove_with_tcc is_mes acc_inv hrec  tcc_lemma_ref (List.map mkVar eqs))
+			 );
+		       is_valid = is_valid_hypothesis predicates_names 
+		     }
+		   in
+		   let ptes_info : pte_info Idmap.t = 
+		     List.fold_left
+		       (fun map pte_id -> 
+			  Idmap.add pte_id 
+			    pte_info			       
+			    map
+		       )
+		       Idmap.empty
+		       predicates_names
+		   in
+		   let make_proof rec_hyps = 
+		     build_proof 
+		       false 
+		       [f_ref]
+		       ptes_info
+		       (body_info rec_hyps)
+		   in
+		   instanciate_hyps_with_args 
+		     make_proof
+		     branches_names
+		     args_ids
+		     g'
+		     
+		) 
+	       ]
+	   ]
+	   g
+      )
+      in
+      tclTHENSEQ 
+	[tac_intro_static;
+	 arg_tac;
+	 start_tac
+	] g
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli
new file mode 100644
index 000000000..35da5d507
--- /dev/null
+++ b/contrib/funind/functional_principles_proofs.mli
@@ -0,0 +1,20 @@
+open Names
+open Term
+
+val prove_princ_for_struct :
+  bool ->
+  int -> constant array -> constr array -> int -> Tacmach.tactic
+
+
+val prove_principle_for_gen : 
+  constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *)
+  constr option ref -> (* a pointer to the obligation proofs lemma *)
+  bool -> (* is that function uses measure *)
+  int -> (* the number of recursive argument *) 
+  types -> (* the type of the recursive argument *)
+  constr -> (* the wf relation used to prove the function *)
+  Tacmach.tactic
+
+
+val is_pte  : rel_declaration -> bool 
+val do_observe : unit -> bool 
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
new file mode 100644
index 000000000..072c3d518
--- /dev/null
+++ b/contrib/funind/functional_principles_types.ml
@@ -0,0 +1,550 @@
+open Printer
+open Util
+open Term
+open Termops 
+open Names 
+open Declarations
+open Pp
+open Entries
+open Hiddentac
+open Evd
+open Tacmach
+open Proof_type
+open Tacticals
+open Tactics
+open Indfun_common
+open Functional_principles_proofs
+
+exception Toberemoved_with_rel of int*constr
+exception Toberemoved
+
+
+
+
+
+(* 
+   Transform an inductive induction principle into 
+   a functional one
+*)  
+let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
+  let princ_type_info = compute_elim_sig princ_type in 
+  let env = Global.env () in 
+  let change_predicate_sort i (x,_,t) = 
+    let new_sort = sorts.(i) in
+    let args,_ = decompose_prod t in 
+    let real_args = 
+      if princ_type_info.indarg_in_concl 
+      then List.tl args 
+      else args
+    in
+    x,None,compose_prod real_args (mkSort new_sort) 
+  in
+  let new_predicates = 
+    list_map_i
+      change_predicate_sort 
+      0
+      princ_type_info.predicates
+  in
+  let env_with_params_and_predicates = 
+    Environ.push_rel_context 
+      new_predicates
+      (Environ.push_rel_context 
+	 princ_type_info.params 
+	 env
+      )
+  in
+  let rel_as_kn = 
+    fst (match princ_type_info.indref with
+	   | Some (Libnames.IndRef ind) -> ind 
+	   | _ -> failwith "Not a valid predicate"
+	)
+  in
+  let pre_princ = 
+    it_mkProd_or_LetIn 
+      ~init:
+      (it_mkProd_or_LetIn 
+	 ~init:(option_fold_right
+			   mkProd_or_LetIn
+			   princ_type_info.indarg
+			   princ_type_info.concl
+			)
+	 princ_type_info.args
+      )
+      princ_type_info.branches
+  in
+  let is_dom c =
+    match kind_of_term c with
+      | Ind((u,_)) -> u = rel_as_kn
+      | Construct((u,_),_) -> u = rel_as_kn
+      | _ -> false
+  in
+  let get_fun_num c =
+    match kind_of_term c with
+      | Ind(_,num) -> num
+      | Construct((_,num),_) -> num
+      | _ -> assert false
+  in
+  let dummy_var = mkVar (id_of_string "________") in
+  let mk_replacement c i args =
+    let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in 
+(*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
+    res
+  in
+  let rec has_dummy_var t  =
+    fold_constr
+      (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
+      false
+      t
+  in
+  let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
+    let (new_princ_type,_) as res =
+      match kind_of_term pre_princ with
+	| Rel n ->
+	    begin
+	      try match Environ.lookup_rel n env with
+		| _,_,t when is_dom t -> raise Toberemoved
+		| _ -> pre_princ,[] with Not_found -> assert false
+	    end
+	| Prod(x,t,b) ->
+	    compute_new_princ_type_for_binder remove mkProd env x t b
+	| Lambda(x,t,b) ->
+	    compute_new_princ_type_for_binder remove mkLambda env x t b
+	| Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
+	| App(f,args) when is_dom f ->
+	    let var_to_be_removed = destRel (array_last args) in
+	    let num = get_fun_num f in
+	    raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args))
+	| App(f,args) ->
+	    let is_pte = 
+	      match kind_of_term f with 
+		| Rel n ->  
+		    is_pte (Environ.lookup_rel n env)
+		| _ -> false 
+	    in
+	    let args = 
+	      if is_pte && remove 
+	      then array_get_start args 
+	      else args 
+	    in
+	    let new_args,binders_to_remove =
+	      Array.fold_right (compute_new_princ_type_with_acc remove env)
+		args
+		([],[])
+	    in
+	    let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
+	    applist(new_f, new_args),
+	    list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+	| LetIn(x,v,t,b) ->
+	    compute_new_princ_type_for_letin remove env x v t b
+	| _ -> pre_princ,[]
+    in
+(*     observennl ( *)
+(*       match kind_of_term pre_princ with  *)
+(* 	| Prod _ ->  *)
+(* 	    str "compute_new_princ_type for "++ *)
+(* 	      pr_lconstr_env env pre_princ ++ *)
+(* 	      str" is "++ *)
+(* 	      pr_lconstr_env env new_princ_type ++ fnl () *)
+(* 	| _ -> str "" *)
+(*     ); *)
+    res
+	
+  and compute_new_princ_type_for_binder remove bind_fun env x t b =
+    begin
+      try
+	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
+	let new_x : name = get_name (ids_of_context env) x in
+	let new_env = Environ.push_rel (x,None,t) env in
+	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
+	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	else
+	  (
+	    bind_fun(new_x,new_t,new_b),
+	    list_union_eq
+	      eq_constr
+	      binders_to_remove_from_t
+	      (List.map pop binders_to_remove_from_b)
+	  )
+	
+      with
+	| Toberemoved ->
+(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = compute_new_princ_type  remove env (substnl [dummy_var] 1 b)  in
+	    new_b, List.map pop binders_to_remove_from_b
+	| Toberemoved_with_rel (n,c) ->
+(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = compute_new_princ_type  remove env (substnl [c] n b)  in
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+    end
+  and compute_new_princ_type_for_letin remove env x v t b =
+    begin
+      try
+	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
+	let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
+	let new_x : name = get_name (ids_of_context env) x in
+	let new_env = Environ.push_rel (x,Some v,t) env in
+	let new_b,binders_to_remove_from_b = compute_new_princ_type remove  new_env b in
+	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	else
+	  (
+	    mkLetIn(new_x,new_v,new_t,new_b),
+	    list_union_eq
+	      eq_constr
+	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+	      (List.map pop binders_to_remove_from_b)
+	  )
+	
+      with
+	| Toberemoved ->
+(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
+	    new_b, List.map pop binders_to_remove_from_b
+	| Toberemoved_with_rel (n,c) ->
+(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+    end
+  and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
+	      let new_e,to_remove_from_e = compute_new_princ_type remove env e
+	      in
+	      new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+  in
+(*   observe (str "Computing new principe from " ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
+  let pre_res,_ = 
+    compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in 
+  it_mkProd_or_LetIn  	 
+    ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates)
+    princ_type_info.params
+    
+  
+
+let change_property_sort toSort princ princName = 
+  let princ_info = compute_elim_sig princ in 
+  let change_sort_in_predicate (x,v,t) = 
+    (x,None,
+     let args,_ = decompose_prod t in 
+     compose_prod args (mkSort toSort)
+    )
+  in 
+  let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in 
+  let init = 
+    let nargs =  (princ_info.nparams + (List.length  princ_info.predicates)) in 
+    mkApp(princName_as_constr,
+	  Array.init nargs
+	    (fun i -> mkRel (nargs - i )))
+  in
+  it_mkLambda_or_LetIn
+    ~init: 
+    (it_mkLambda_or_LetIn ~init 
+       (List.map change_sort_in_predicate princ_info.predicates)
+    )
+    princ_info.params
+    
+
+let pp_dur time time' = 
+  str (string_of_float (System.time_difference time time'))
+
+(* End of things to be removed latter : just here to compare 
+   saving proof with and without  normalizing the proof 
+*)
+
+let qed () = Command.save_named true 
+let defined () = Command.save_named false
+let generate_functional_principle 
+    interactive_proof
+    old_princ_type sorts new_princ_name funs i proof_tac 
+    = 
+  let f = funs.(i) in 
+  let type_sort = Termops.new_sort_in_family InType in 
+  let new_sorts = 
+    match sorts with 
+      | None -> Array.make (Array.length funs) (type_sort)
+      | Some a -> a
+  in
+  (* First we get the type of the old graph principle *)
+  let mutr_nparams = (compute_elim_sig old_princ_type).nparams in 
+  (* First we get the type of the old graph principle *)
+   let new_principle_type =
+    compute_new_princ_type_from_rel
+      (Array.map mkConst funs)
+      new_sorts
+      old_princ_type
+   in
+(*    observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
+  let base_new_princ_name,new_princ_name =
+    match new_princ_name with
+      | Some (id) -> id,id
+      | None ->
+	  let id_of_f = id_of_label (con_label f) in
+	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+  in
+  let names = ref [new_princ_name] in 
+  let hook _ _  =
+    if sorts = None 
+    then
+(*     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 base_new_princ_name fam_sort in
+      let value =
+	change_property_sort s new_principle_type new_princ_name
+      in
+(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+      let ce =
+	{ const_entry_body = value;
+	  const_entry_type = None;
+	  const_entry_opaque = false;
+	  const_entry_boxed = Options.boxed_definitions()
+	}
+      in
+      ignore(
+	Declare.declare_constant
+	  name
+	  (Entries.DefinitionEntry ce,
+	   Decl_kinds.IsDefinition (Decl_kinds.Scheme)
+	  )
+      );
+      names := name :: !names
+    in
+    register_with_sort InProp;
+    register_with_sort InSet
+  in
+  begin
+    Command.start_proof
+      new_princ_name
+      (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+      new_principle_type
+      hook
+    ;
+    try
+      let _tim1 = System.get_time ()  in
+      Pfedit.by  (proof_tac (Array.map mkConst funs) mutr_nparams);
+      let _tim2 =  System.get_time ()  in
+(* 	begin *)
+(* 	  let dur1 = System.time_difference tim1 tim2 in *)
+(* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
+(* 	end; *)
+      let do_save =  not (do_observe ()) && not interactive_proof in 
+      let _ = 
+	try 
+(* 	  Vernacentries.show_script (); *)
+	  Options.silently defined ();
+	  let _dur2 = System.time_difference _tim2 (System.get_time ()) in
+(* 	  Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *)
+	  Options.if_verbose 
+	    (fun () -> 
+	       Pp.msgnl (
+		 prlist_with_sep
+		   (fun () -> str" is defined " ++ fnl ()) 
+		   Ppconstr.pr_id
+		   (List.rev !names) ++ str" is defined " 
+	       )
+	    ) 
+	       ()
+	with e when do_save -> 
+	  msg_warning
+	    (
+	      Cerrors.explain_exn e
+	    );
+	  if not (do_observe ())
+	  then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
+      in
+      ()
+
+(*       let tim3 = Sys.time ()  in *)
+(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *)
+
+    with
+      | e ->
+	  msg_warning
+	    (
+	      Cerrors.explain_exn e
+	    );
+	  if not ( do_observe ())
+	  then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
+  end
+
+
+
+
+exception Not_Rec
+
+let get_funs_constant mp dp = 
+  let rec get_funs_constant const e : (Names.constant*int) array = 
+    match kind_of_term (snd (decompose_lam e)) with 
+      | Fix((_,(na,_,_))) -> 
+	  Array.mapi 
+	    (fun i na -> 
+	       match na with 
+		 | Name id -> 
+		     let const = make_con mp dp (label_of_id id) in 
+		     const,i
+		 | Anonymous -> 
+		     anomaly "Anonymous fix" 
+	    )
+	    na
+      | _ -> [|const,0|]
+  in
+  function const -> 
+    let find_constant_body const = 
+      match (Global.lookup_constant const ).const_body with
+	| Some b ->
+	    let body = force b in
+	    let body = Tacred.cbv_norm_flags
+	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+	      (Global.env ())
+	      (Evd.empty)
+	      body
+	    in
+	    body
+	| None -> error ( "Cannot define a principle over an axiom ")
+    in
+    let f = find_constant_body const in
+    let l_const = get_funs_constant const f in 
+    (* 
+       We need to check that all the functions found are in the same block 
+       to prevent Reset stange thing
+    *) 
+    let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in 
+    let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in 
+    (* all the paremeter must be equal*) 
+    let _check_params = 
+      let first_params = List.hd l_params  in 
+      List.iter 
+	(fun params -> 
+	   if not ((=) first_params params) 
+	   then error "Not a mutal recursive block"
+	)
+	l_params
+    in
+    (* The bodies has to be very similar *) 
+    let _check_bodies = 
+      try 
+	let extract_info is_first body = 
+	  match kind_of_term body with 
+	    | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
+	    | _ -> 
+		if is_first && (List.length l_bodies = 1) 
+		then raise Not_Rec
+		else error "Not a mutal recursive block"
+	in
+	let first_infos = extract_info true (List.hd l_bodies) in 
+	let check body  = (* Hope this is correct *)
+	  if not (first_infos = (extract_info false body)) 
+	  then  error "Not a mutal recursive block"
+	in 
+	List.iter check l_bodies
+      with Not_Rec -> ()
+    in
+    l_const
+	
+let make_scheme fas = 
+  let env = Global.env () 
+  and sigma = Evd.empty in
+  let id_to_constr id = 
+    Tacinterp.constr_of_id env  id
+  in 
+  let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in 
+  let first_fun = destConst (List.hd funs) in 
+  let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in 
+  let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in 
+  let first_fun_kn = 
+    (* Fixme: take into accour funs_mp and funs_dp *)
+    fst (destInd (id_to_constr first_fun_rel_id))
+  in
+  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+  let this_block_funs = Array.map fst this_block_funs_indexes in 
+  let prop_sort = InProp in
+  let funs_indexes = 
+    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
+    List.map
+      (function const -> List.assoc (destConst const) this_block_funs_indexes)
+      funs
+  in
+  let ind_list = 
+    List.map 
+      (fun (idx) -> 
+	 let ind = first_fun_kn,idx in 
+	 let (mib,mip) = Global.lookup_inductive ind in
+	 ind,mib,mip,true,prop_sort
+      )
+      funs_indexes
+  in
+  let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in 
+  let i = ref (-1) in
+  let sorts = 
+    List.rev_map (fun (_,_,x) -> 
+		Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+	     ) 
+      fas 
+  in
+  let princ_names = List.map (fun (x,_,_) -> x) fas in 
+  let _ = List.map2
+    (fun princ_name scheme_type -> 
+       incr i;
+(*        observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
+(* 	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
+(* 	       ); *)
+       generate_functional_principle
+	 false
+	 scheme_type
+	 (Some (Array.of_list sorts))
+	 (Some princ_name)
+	 this_block_funs
+	 !i
+	 (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs)))
+    )
+    princ_names
+    l_schemes 
+  in
+  ()
+
+let make_case_scheme fa = 
+  let env = Global.env () 
+  and sigma = Evd.empty in
+  let id_to_constr id = 
+    Tacinterp.constr_of_id env  id
+  in 
+  let funs =  (fun (_,f,_) -> id_to_constr f) fa in 
+  let first_fun = destConst  funs in 
+  let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in 
+  let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in 
+  let first_fun_kn = 
+    (* Fixme: take into accour funs_mp and funs_dp *)
+    fst (destInd (id_to_constr first_fun_rel_id))
+  in
+  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+  let this_block_funs = Array.map fst this_block_funs_indexes in 
+  let prop_sort = InProp in
+  let funs_indexes = 
+    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
+    List.assoc (destConst funs) this_block_funs_indexes
+  in
+  let ind_fun = 
+	 let ind = first_fun_kn,funs_indexes in 
+	 ind,prop_sort
+  in
+  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in 
+  let sorts =
+    (fun (_,_,x) ->
+       Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+    )
+      fa
+  in
+  let princ_name =  (fun (x,_,_) -> x) fa in
+  let _ = 
+(*     observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
+(* 	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
+(* 	    ); *)
+    generate_functional_principle
+      false
+      scheme_type
+      (Some ([|sorts|]))
+      (Some princ_name)
+      this_block_funs
+      0
+      (prove_princ_for_struct false 0 [|destConst funs|])
+  in
+  ()
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
new file mode 100644
index 000000000..929c3db51
--- /dev/null
+++ b/contrib/funind/functional_principles_types.mli
@@ -0,0 +1,28 @@
+open Names
+open Term
+val generate_functional_principle : 
+  (* do we accept interactive proving *)
+  bool ->
+  (* induction principle on rel *) 
+  types ->
+  (* *)
+  sorts array option -> 
+  (* Name of the new principle *) 
+  (identifier) option -> 
+  (* the compute functions to use   *)
+  constant array -> 
+  (* We prove the nth- principle *)
+  int  ->
+  (* The tactic to use to make the proof w.r
+     the number of params
+  *)
+  (constr array -> int -> Tacmach.tactic) -> 
+  unit
+
+
+
+val compute_new_princ_type_from_rel : constr array -> sorts array -> 
+  types -> types
+
+val make_scheme : (identifier*identifier*Rawterm.rawsort) list ->  unit
+val make_case_scheme : (identifier*identifier*Rawterm.rawsort)  ->  unit
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 81527912d..f65c94752 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -1,7 +1,6 @@
 open Util
 open Names
 open Term
-
 open Pp
 open Indfun_common
 open Libnames
@@ -29,6 +28,11 @@ let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen false sigma env ~impls:([],impls) 
     ~allow_soapp:false  ~ltacvars:([],[]) c
 
+
+(* 
+   Construct a fixpoint as a Rawterm 
+   and not as a constr
+*)
 let build_newrecursive
 (lnameargsardef)  =
   let env0 = Global.env()
@@ -78,6 +82,7 @@ let compute_annot (name,annot,args,types,body) =
     | Some r -> (name,r,args,types,body)
 
 
+(* Checks whether or not the mutual bloc is recursive *) 
 let rec is_rec names = 
   let names = List.fold_right Idset.add names Idset.empty in 
   let check_id id names =  Idset.mem id names in 
@@ -85,7 +90,7 @@ let rec is_rec names =
     | RVar(_,id) -> check_id id names
     | RRef _ | REvar _ | RPatVar _ | RSort _ |  RHole _ | RDynamic _ -> false
     | RCast(_,b,_,_) -> lookup names b
-    | RRec _ -> assert false 
+    | RRec _ -> error "RRec not handled"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
     | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b)  -> 
@@ -143,7 +148,7 @@ let generate_principle
 	       let princ_type = 
 		 (Global.lookup_constant princ).Declarations.const_type
 	       in
-	       New_arg_principle.generate_functional_principle
+	       Functional_principles_types.generate_functional_principle
 		 interactive_proof 
 		 princ_type
 		 None
@@ -175,12 +180,12 @@ let register_struct is_rec fixpoint_exprl =
     | _ -> 
 	Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
 
-
-let generate_correction_proof_wf tcc_lemma_ref   
-    is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+let generate_correction_proof_wf f_ref tcc_lemma_ref   
+    is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
     (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic = 
-  Recdef.prove_principle  tcc_lemma_ref
-    is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+  Functional_principles_proofs.prove_principle_for_gen
+    (f_ref,functional_ref,eq_ref)
+    tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
 
 
 let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
@@ -218,11 +223,11 @@ 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 
-  let hook tcc_lemma_ref f_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
+  let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
     try 
       pre_hook 
-	(generate_correction_proof_wf tcc_lemma_ref is_mes
-	   f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
+	(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
+	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 	);
       Command.save_named true
     with e -> 
@@ -351,7 +356,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	    recdefs 
 	    interactive_proof
 	    true
-	    (New_arg_principle.prove_princ_for_struct interactive_proof);
+	    (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
 	  true
 						 
   in
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index a238de895..c4f0c0ad6 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -61,8 +61,7 @@ let is_rec scheme_info =
 let choose_dest_or_ind scheme_info =
     if is_rec scheme_info
     then Tactics.new_induct
-    else
-      Tactics.new_destruct
+    else Tactics.new_destruct
 
 
 TACTIC EXTEND newfunind
@@ -178,7 +177,7 @@ END
 VERNAC COMMAND EXTEND NewFunctionalScheme
    ["New" "Functional" "Scheme" fun_scheme_args(fas) ] ->
     [
-      New_arg_principle.make_scheme fas
+      Functional_principles_types.make_scheme fas
     ]
 END
 
@@ -186,7 +185,7 @@ END
 VERNAC COMMAND EXTEND NewFunctionalCase
    ["New" "Functional" "Case" fun_scheme_arg(fas) ] ->
     [
-      New_arg_principle.make_case_scheme fas
+      Functional_principles_types.make_case_scheme fas
     ]
 END
 
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
deleted file mode 100644
index 12a43b5db..000000000
--- a/contrib/funind/new_arg_principle.ml
+++ /dev/null
@@ -1,1770 +0,0 @@
-open Printer
-open Util
-open Term
-open Termops 
-open Names 
-open Declarations
-open Pp
-open Entries
-open Hiddentac
-open Evd
-open Tacmach
-open Proof_type
-open Tacticals
-open Tactics
-open Indfun_common
-
-
-let msgnl = Pp.msgnl
-
-let do_observe () = 
-  Tacinterp.get_debug () <> Tactic_debug.DebugOff  
-
-
-let observe strm =
-  if do_observe ()
-  then Pp.msgnl strm
-  else ()
-
-let observennl strm =
-  if do_observe ()
-  then begin Pp.msg strm;Pp.pp_flush () end
-  else ()
-
-
-
-
-let do_observe_tac s tac g =
- try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
- with e ->
-   let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
-   msgnl (str "observation "++str s++str " raised exception " ++ 
-	    Cerrors.explain_exn e ++ str " on goal " ++ goal ); 
-   raise e;;
-
-
-let observe_tac s tac g =
-  if do_observe ()
-  then do_observe_tac s tac g
-  else tac g
-
-
-let tclTRYD tac = 
-  if  !Options.debug  || do_observe ()
-  then (fun g -> try (* do_observe_tac ""  *)tac g with _ -> tclIDTAC g)
-  else tac
-
-
-let list_chop ?(msg="") n l = 
-  try 
-    list_chop n l 
-  with Failure (msg') -> 
-    failwith (msg ^ msg')
-  
-
-let make_refl_eq type_of_t t  =
-  let refl_equal_term = Lazy.force refl_equal in
-  mkApp(refl_equal_term,[|type_of_t;t|])
-
-
-type static_fix_info = 
-    {
-      idx : int;
-      name : identifier;
-      types : types;
-      nb_realargs : int
-    }
-
-type static_infos = 
-    {
-      fixes_ids : identifier list; 
-      ptes_to_fixes : static_fix_info Idmap.t
-    }
-
-type 'a dynamic_info = 
-    { 
-      nb_rec_hyps : int;
-      rec_hyps : identifier list ; 
-      eq_hyps : identifier list;
-      info : 'a
-    }
-
-let finish_proof dynamic_infos g = 
-  observe_tac "finish" 
-    h_assumption
-    g
-	  
-
-let refine c = 
-  Tacmach.refine_no_check c
-
-let thin l = 
-  Tacmach.thin_no_check l
-  
-
-let cut_replacing id t tac :tactic= 
-  tclTHENS (cut t)
-    [ tclTHEN (thin_no_check [id]) (introduction_no_check id);
-      tac 
-    ]
-
-let intro_erasing id = tclTHEN (thin [id]) (introduction id)
-
-
-
-let rec_hyp_id = id_of_string "rec_hyp"
-
-let is_trivial_eq t = 
-  match kind_of_term t with 
-    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
-	eq_constr t1 t2
-    | _ -> false 
-
-
-let rec incompatible_constructor_terms t1 t2 = 
-  let c1,arg1 = decompose_app t1 
-  and c2,arg2 = decompose_app t2 
-  in 
-  (not (eq_constr t1 t2)) &&
-    isConstruct c1 && isConstruct c2 && 
-    (
-      not (eq_constr c1 c2) || 
-	List.exists2 incompatible_constructor_terms arg1 arg2
-    )
-
-let is_incompatible_eq t = 
-  match kind_of_term t with 
-    | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> 
-	incompatible_constructor_terms t1 t2
-    | _ -> false 
-
-let change_hyp_with_using hyp_id t tac = 
-  fun g -> 
-    let prov_id = pf_get_new_id hyp_id g in 
-    tclTHENLIST 
-      [
-	forward (Some tac) (Genarg.IntroIdentifier prov_id) t;
-	thin [hyp_id];
-	h_rename prov_id hyp_id
-      ] g
-
-exception TOREMOVE
-
-
-let prove_trivial_eq h_id context (type_of_term,term) = 
-  let nb_intros = List.length context in 
-  tclTHENLIST
-    [
-      tclDO nb_intros intro; (* introducing context *)
-      (fun g -> 
-	 let context_hyps =  
-	   fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) 
-	 in
-	 let context_hyps' = 
-	   (mkApp(Lazy.force refl_equal,[|type_of_term;term|]))::
-	     (List.map mkVar context_hyps)
-	 in
-	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in 
-	 refine to_refine g
-      )
-    ]
-
-
-let isAppConstruct t = 
-  if isApp t 
-  then isConstruct (fst (destApp t))
-  else false 
-
-
-let nf_betaoiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta 
-
-let remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 =
-    let rel_num = destRel t2 in
-
-    let nb_kept = List.length context - rel_num 
-    and nb_popped = rel_num - 1
-    in
-
-    (* We remove the equation *) 
-    let new_end_of_type = pop end_of_type in
-    
-    let lt_relnum,ge_relnum = 
-      list_chop  
-	~msg:("removing useless variable "^(string_of_int rel_num)^" :")
-	nb_popped
-	context 
-    in
-    (* we rebuilt the type of hypothesis after the rel to remove *)
-    let hyp_type_lt_relnum = 
-      it_mkProd_or_LetIn ~init:new_end_of_type lt_relnum 
-    in 
-    (* we replace Rel 1 by t1 *) 
-    let new_hyp_type_lt_relnum = subst1 t1 hyp_type_lt_relnum in 
-    (* we resplit the type of hyp_type *)
-    let new_lt_relnum,new_end_of_type = 
-      Sign.decompose_prod_n_assum nb_popped new_hyp_type_lt_relnum 
-    in
-    (* and rebuilt new context of hyp *)
-    let new_context = new_lt_relnum@(List.tl ge_relnum) in 
-    let new_typ_of_hyp =
-      nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type new_context)
-    in
-    let prove_simpl_eq =
-      tclTHENLIST
-	[
-	  tclDO (nb_popped + nb_kept) intro;
-	  (fun g'  ->
-	     let new_hyps_ids = pf_ids_of_hyps g' in
-	     let popped_ids,others =
-	       list_chop ~msg:"removing useless variable pop :"
-		 nb_popped new_hyps_ids in
-	     let kept_ids,_ =
-	       list_chop ~msg: " removing useless variable kept : "
-		 nb_kept others
-	     in
-	     let rev_to_apply =
-	       (mkApp(Lazy.force refl_equal,[|Typing.type_of env sigma t1;t1|]))::
-		 ((List.map mkVar popped_ids)@
-		    (t1::
-		       (List.map mkVar kept_ids)))
-	       in
-	     let to_refine = applist(mkVar hyp_id,List.rev rev_to_apply) in
-	     refine to_refine g'
-	  )
-	]
-    in
-    let simpl_eq_tac = change_hyp_with_using hyp_id new_typ_of_hyp
-      (observe_tac "prove_simpl_eq" prove_simpl_eq)
-    in
-    let new_end_of_type = nf_betaoiotazeta new_end_of_type in
-    (new_context,new_end_of_type,simpl_eq_tac),new_typ_of_hyp,
-  (str " removing useless variable " ++ str (string_of_int rel_num) )
-
-
-let decompose_eq env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 = 
-    let c1,args1 = destApp t1 
-    and c2,args2 = destApp t2 
-    in
-    (* This tactic must be used after is_incompatible_eq *)
-    assert (eq_constr c1 c2); 
-    (* we remove this equation *)
-    let new_end_of_type = pop end_of_type in 
-    let new_eqs = 
-      array_map2_i 
-	(fun i arg1 arg2 -> 
-	   let new_eq = 
-	     let type_of_arg =  Typing.type_of env sigma arg1 in 
- 	     mkApp(Lazy.force eq,[|type_of_arg;arg1;arg2|])
-	   in
-	    Anonymous,None,lift i new_eq
-	)
-	args1
-	args2
-    in
-    let nb_new_eqs = Array.length new_eqs in 
-    (* we add the new equation *) 
-    let new_end_of_type = lift nb_new_eqs new_end_of_type in 
-    let local_context = 
-      List.rev (Array.to_list new_eqs) in 
-    let new_end_of_type = it_mkProd_or_LetIn ~init:new_end_of_type local_context in
-    let new_typ_of_hyp = 
-      nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type context) 
-    in 
-    let prove_pattern_simplification =
-      let context_length = List.length context in
-      tclTHENLIST 
-	[
-	  tclDO (context_length + nb_new_eqs) intro ;
-	  (fun g -> 
-	     let new_eqs,others = 
-	       list_chop ~msg:"simplifying pattern : new_eqs" nb_new_eqs (pf_hyps g)
-	     in
-	     let context_hyps,_ = list_chop ~msg:"simplifying pattern : context_hyps" 
-	       context_length others in
-	     let eq_args = 
-	       List.rev_map 
-		 (fun (_,_, eq) -> let _,args = destApp eq in   args.(1),args.(2))
-		 new_eqs 
-	     in
-	     let lhs_args,rhs_args = List.split eq_args in 
-	     let lhs_eq = applist(c1,lhs_args) 
-	     and rhs_eq = applist(c1,rhs_args) 
-	     in 
-	     let type_of_eq = pf_type_of g lhs_eq in 
-	     let eq_to_assert = 
-	       mkApp(Lazy.force eq,[|type_of_eq;lhs_eq;rhs_eq|])
-	     in
-	     let prove_new_eq = 
-	       tclTHENLIST [
-		 tclMAP 
-		   (fun (id,_,_) -> 
-		      (* The tclTRY here is used when trying to rewrite 
-			 on Set 
-			 eg (@cons A x l)=(@cons A x' l') generates 3 eqs 
-			 A=A -> x=x' -> l = l' ...
-			 
-		      *)
-		      tclTRY (Equality.rewriteLR (mkVar id))
-		   )
-		   new_eqs;
-		 reflexivity
-	       ]
-	     in
-	     let new_eq_id = pf_get_new_id  (id_of_string "H") g in 
-	     let create_new_eq = 
-	       forward         
-		 (Some (observe_tac "prove_new_eq" (prove_new_eq)))
-		 (Genarg.IntroIdentifier new_eq_id)        
-		 eq_to_assert 
-	     in
-	     let to_refine =
-	       applist (
-		 mkVar hyp_id,
-		 List.rev ((mkVar new_eq_id)::
-			     (List.map (fun (id,_,_) -> mkVar id) context_hyps)))
-	     in 
-	     tclTHEN 
-	       (observe_tac "create_new_eq" create_new_eq )
-	       (observe_tac "refine in decompose_eq " (refine to_refine))
-	       g
-	  )
-	]
-    in
-    let simpl_eq_tac = 
-      change_hyp_with_using hyp_id new_typ_of_hyp (observe_tac "prove_pattern_simplification " prove_pattern_simplification)
-    in 
-    (context,nf_betaoiotazeta new_end_of_type,simpl_eq_tac),new_typ_of_hyp,
-  str "simplifying an equation " 
-
-let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
-  if not (noccurn 1 end_of_type)
-  then (* if end_of_type depends on this term we don't touch it  *)
-    begin 
-      observe (str "Not treating " ++ pr_lconstr t    );
-      failwith "NoChange"; 
-    end;
-  let res,new_typ_of_hyp,msg = 
-    if not (isApp t) then failwith "NoChange";
-    let f,args = destApp t in 
-    if not (eq_constr f (Lazy.force eq)) then failwith "NoChange"; 
-      let t1 = args.(1) 
-      and t2 = args.(2)
-      in 
-      if isRel t2 && closed0 t1 then (* closed_term = x with x bound in context *)
-	begin
-	  remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2
-	end 
-      else if isAppConstruct t1 && isAppConstruct t2 (* C .... = C .... *) 
-      then decompose_eq env sigma hyp_id context t end_of_type t1 t2
-      else failwith "NoChange"
-  in 
-  observe (str "In " ++ Ppconstr.pr_id hyp_id ++ 
-	     msg ++ fnl ()++ 
-	     str "old_typ_of_hyp :=" ++
-	     Printer.pr_lconstr_env
-	     env
-	       (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context))
-	   ++ fnl () ++
-	     str "new_typ_of_hyp := "++ 
-	     Printer.pr_lconstr_env env new_typ_of_hyp ++ fnl ());
-  (res:'a*'b*'c)
-  
-
-
-
-let is_property static_info t_x = 
-  if isApp t_x 
-  then 
-    let pte,args = destApp t_x in 
-    if isVar pte && array_for_all closed0 args 
-    then Idmap.mem (destVar pte) static_info.ptes_to_fixes
-    else false 
-  else false 
-
-let isLetIn t = 
-  match kind_of_term t with 
-    | LetIn _ -> true 
-    | _ -> false 
-
-
-let h_reduce_with_zeta = 	 
-  h_reduce 
-    (Rawterm.Cbv
-       {Rawterm.all_flags 
-	with Rawterm.rDelta = false; 		 
-       })
-  
-
-
-let rewrite_until_var arg_num eq_ids : tactic =
-  let test_var g = 
-    let _,args = destApp (pf_concl g) in 
-    isVar args.(arg_num)
-  in
-  let rec do_rewrite eq_ids g  = 
-    if test_var g 
-    then tclIDTAC g
-    else
-      match eq_ids with 
-	| [] -> anomaly "Cannot find a way to prove recursive property";
-	| eq_id::eq_ids -> 
-	    tclTHEN 
-	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
-	      (do_rewrite eq_ids)
-	      g
-  in
-  do_rewrite eq_ids
-
-let prove_rec_hyp eq_hyps fix_info =
-  tclTHEN 
-    (rewrite_until_var (fix_info.idx - 1) eq_hyps)
-    (fun g -> 
-       let _,pte_args = destApp (pf_concl g) in 
-       let rec_hyp_proof = 
-	 mkApp(mkVar fix_info.name,array_get_start pte_args) 
-       in
-       refine rec_hyp_proof g
-    )
-
-	 
-
-
-
-let rec_pte_id = id_of_string "Hrec" 
-let clean_hyp_with_heq static_infos eq_hyps hyp_id env sigma = 
-  let coq_False = Coqlib.build_coq_False () in 
-  let coq_True = Coqlib.build_coq_True () in 
-  let coq_I = Coqlib.build_coq_I () in 
-  let rec scan_type  context type_of_hyp : tactic = 
-    if isLetIn type_of_hyp then 
-      let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
-      let reduced_type_of_hyp = nf_betaoiotazeta real_type_of_hyp in 
-      (* length of context didn't change ? *)
-      let new_context,new_typ_of_hyp = 
-	 Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
-      in
-        tclTHENLIST 
-	[
-	  h_reduce_with_zeta
-	    (Tacticals.onHyp hyp_id)
-	  ;
-	  scan_type new_context new_typ_of_hyp 
-	  
-	]
-    else if isProd type_of_hyp 
-    then 
-      begin 
-	let (x,t_x,t') = destProd type_of_hyp in
-	if is_property static_infos t_x then
-	  begin
-	    let pte,pte_args =  (destApp t_x) in 
-	    let fix_info = Idmap.find (destVar pte) static_infos.ptes_to_fixes in 
-	    let popped_t' = pop t' in 
-	    let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in 
-	    let prove_new_type_of_hyp = 
-	      let context_length = List.length context in 
-	      tclTHENLIST
-		[ 
-		  tclDO context_length intro; 
-		  (fun g ->  
-		     let context_hyps_ids = 
-		       fst (list_chop ~msg:"rec hyp : context_hyps"
-			      context_length (pf_ids_of_hyps g))
-		     in
-		     let rec_pte_id = pf_get_new_id rec_pte_id g in 
-		     let to_refine = 
-		       applist(mkVar hyp_id,
-			       List.rev_map mkVar (rec_pte_id::context_hyps_ids)
-			      )
-		     in
-		     tclTHENLIST
-		       [ 
-			 forward 
-			   (Some (prove_rec_hyp eq_hyps fix_info))
-			   (Genarg.IntroIdentifier rec_pte_id)
-			   t_x;
-			 refine to_refine
-		       ]
-		       g
-		  )
-		]
-	    in
-	    tclTHENLIST 
-	      [
-		observe_tac "hyp rec" 
-		  (change_hyp_with_using hyp_id real_type_of_hyp prove_new_type_of_hyp);
-		scan_type context popped_t'
-	      ]
-	  end
-	else if eq_constr t_x coq_False then 
-	  begin
-	    observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ 
-		       str " since it has False in its preconds "
-		    );
-	    raise TOREMOVE;  (* False -> .. useless *)
-	  end
-	else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *) 
-	else if eq_constr t_x coq_True  (* Trivial => we remove this precons *)
-	then 
-	  let _ = 
-	    observe (str "In "++Ppconstr.pr_id hyp_id++ 
-		       str " removing useless precond True"
-		    ) 
-	  in 
-	  let popped_t' = pop t' in
-	  let real_type_of_hyp = 
-	    it_mkProd_or_LetIn ~init:popped_t' context 
-	  in 
-	  let prove_trivial =  
-	    let nb_intro = List.length context in 
-	    tclTHENLIST [
-	      tclDO nb_intro intro;
-	      (fun g -> 
-		 let context_hyps = 
-		   fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g))
-		 in
-		 let to_refine = 
-		   applist (mkVar hyp_id,
-			    List.rev (coq_I::List.map mkVar context_hyps)
-			   )
-		 in
-		 refine to_refine g
-	      )
-	    ]
-	  in
-	  tclTHENLIST[
-	    change_hyp_with_using hyp_id real_type_of_hyp (observe_tac "prove_trivial" prove_trivial);
-	    scan_type context popped_t'
-	  ]
-	else if is_trivial_eq t_x 
-	then (*  t_x :=  t = t   => we remove this precond *) 
-	  let popped_t' = pop t' in
-	  let real_type_of_hyp =
-	    it_mkProd_or_LetIn ~init:popped_t' context
-	  in
-	  let _,args = destApp t_x in
-	  tclTHENLIST
-	    [
-	      change_hyp_with_using
-		hyp_id
-		real_type_of_hyp
-		(observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1))));
-	      scan_type context popped_t'
-	    ] 
-	else 
-	  begin
-	    try 
-	      let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in 
-	      tclTHEN
-		tac 
-		(scan_type new_context new_t')
-	    with Failure "NoChange" -> 
-	      (* Last thing todo : push the rel in the context and continue *) 
-	      scan_type ((x,None,t_x)::context) t'
-	  end
-      end
-    else
-      tclIDTAC
-  in 
-  try 
-    scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
-  with TOREMOVE -> 
-    thin [hyp_id],[]
-
-
-let clean_goal_with_heq static_infos continue_tac dyn_infos  = 
-  fun g -> 
-    let env = pf_env g 
-    and sigma = project g 
-    in
-    let tac,new_hyps = 
-      List.fold_left ( 
-	fun (hyps_tac,new_hyps) hyp_id ->
-	  let hyp_tac,new_hyp = 
-	    clean_hyp_with_heq static_infos dyn_infos.eq_hyps hyp_id env sigma 
-	  in
-	  (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps
-      )
-	(tclIDTAC,[])
-	dyn_infos.rec_hyps
-    in
-    let new_infos = 
-      { dyn_infos with 
-	  rec_hyps = new_hyps; 
-	  nb_rec_hyps  = List.length new_hyps
-      }
-    in
-    tclTHENLIST 
-      [
-	tac ;
-	(continue_tac new_infos)
-      ]
-      g    
-
-let heq_id = id_of_string "Heq"
-
-let treat_new_case static_infos nb_prod continue_tac term dyn_infos = 
-  fun g -> 
-    let heq_id = pf_get_new_id heq_id g in 
-    let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
-    tclTHENLIST
-      [ 
-	(* We first introduce the variables *) 
-	tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps);
-	(* Then the equation itself *)
-	introduction_no_check heq_id;
-	(* Then the new hypothesis *) 
-	tclMAP introduction_no_check dyn_infos.rec_hyps;
-	observe_tac "after_introduction" (fun g' -> 
-	   (* We get infos on the equations introduced*)
-	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in 
-	   (* compute the new value of the body *)
-	   let new_term_value =
-	     match kind_of_term new_term_value_eq with
-	       | App(f,[| _;_;args2 |]) -> args2
-	       | _ ->
-		   observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++
-			      pr_lconstr_env (pf_env g') new_term_value_eq
-			   );
-		   assert false
-	   in
-	 let fun_body =
-	   mkLambda(Anonymous,
-		    pf_type_of g' term,
-		    replace_term term (mkRel 1) dyn_infos.info
-		   )
-	 in
-	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
-	 let new_infos = 
-	   {dyn_infos with 
-	      info = new_body;
-	      eq_hyps = heq_id::dyn_infos.eq_hyps
-	   }
-	 in 
-	 clean_goal_with_heq static_infos continue_tac new_infos  g'
-      )
-    ]
-      g
-
-
-let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = 
-  let args = Array.of_list (List.map mkVar  args_id) in 
-  let instanciate_one_hyp hid = 
-    tclORELSE
-      ( (* we instanciate the hyp if possible  *)
-	fun g -> 
-	  let prov_hid = pf_get_new_id hid g in
-	  tclTHENLIST[
-	    forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
-	    thin [hid];
-	    h_rename prov_hid hid
-	  ] g
-      )
-      ( (*
-	  if not then we are in a mutual function block 
-	  and this hyp is a recursive hyp on an other function.
-	  
-	  We are not supposed to use it while proving this 
-	  principle so that we can trash it 
-	  
-	*)
-	(fun g -> 
-	   observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid);
-	   thin [hid] g
-	)
-      )
-  in
-  if args_id = []  
-  then 
-    tclTHENLIST [
-      tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
-      do_prove hyps
-    ]
-  else
-    tclTHENLIST
-      [
-	tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
-	tclMAP instanciate_one_hyp hyps;
-	(fun g ->  
-	   let all_g_hyps_id = 
-	     List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
-	   in 
-	   let remaining_hyps = 
-	     List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
-	   in
-	   do_prove remaining_hyps g
-	  )
-      ]
-
-
-let do_prove_princ_for_struct 
-    (interactive_proof:bool)
-    (fnames:constant list)
-    static_infos
-(*     (ptes:identifier list)  *)
-(*     (fixes:(int*constr*identifier*constr) Idmap.t) *)
-(*     (hyps: identifier list) *)
-(*     (term:constr) *)
-    dyn_infos
-    : tactic =
-(*   let fixes_ids = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in *)
-  let rec do_prove_princ_for_struct_aux do_finalize dyn_infos : tactic = 
-    fun g -> 
-(*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
-	match kind_of_term dyn_infos.info with 
-	  | Case(_,_,t,_) -> 
-	      let g_nb_prod = nb_prod (pf_concl g) in
-	      let type_of_term = pf_type_of g t in
-	      let term_eq =
-		make_refl_eq type_of_term t
-	      in
-  	      tclTHENSEQ
-		[
-		  h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps);
-		  thin dyn_infos.rec_hyps;
-		  pattern_option [[-1],t] None;
-		  h_simplest_case t;
-		  (fun g' -> 
-		     let g'_nb_prod = nb_prod (pf_concl g') in 
-		     let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
-		     observe_tac "treat_new_case" 
-		       (treat_new_case  
-		       static_infos
-		       nb_instanciate_partial 
-		       (do_prove_princ_for_struct do_finalize) 
-		       t 
-		       dyn_infos)
-		       g'
-		  )
-		  
-		] g
-	  | Lambda(n,t,b) ->
-	      begin
-		match kind_of_term( pf_concl g) with
-		  | Prod _ ->
-		      tclTHEN
-			intro
-			(fun g' ->
-			   let (id,_,_) = pf_last_hyp g' in
-			   let new_term = 
-			     pf_nf_betaiota g' 
-			       (mkApp(dyn_infos.info,[|mkVar id|])) 
-			   in
-			   let new_infos = {dyn_infos with info = new_term} in
-			   let do_prove new_hyps = 
-			     do_prove_princ_for_struct do_finalize 
-			       {new_infos with
-			       	  rec_hyps = new_hyps; 
-				  nb_rec_hyps  = List.length new_hyps
-			       }
-			   in 
-			   observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
-			     (* 			   do_prove_princ_for_struct do_finalize new_infos g' *)
-			) g
-		  | _ ->
-		      do_finalize dyn_infos g 
-	      end
-	  | Cast(t,_,_) -> 
-	      do_prove_princ_for_struct do_finalize {dyn_infos with info = t} g
-	  | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
-	      do_finalize dyn_infos g
-	  | App(_,_) ->
-	      let f,args = decompose_app dyn_infos.info in
-	      begin
-		match kind_of_term f with
-		  | App _ -> assert false (* we have collected all the app in decompose_app *)
-		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
-		      let new_infos = 
-			{ dyn_infos with 
-			    info = (f,args)
-			}
-		      in
-		      do_prove_princ_for_struct_args do_finalize new_infos  g
-		  | Const c when not (List.mem c fnames) ->
-		      let new_infos = 
-			{ dyn_infos with 
-			    info = (f,args)
-			}
-		      in
-(* 		      Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
-		      do_prove_princ_for_struct_args do_finalize new_infos g
-		  | Const _ ->
-		      do_finalize dyn_infos  g
-		  | Lambda _ -> 
-		      let new_term = Reductionops.nf_beta dyn_infos.info in 
-		      do_prove_princ_for_struct do_finalize {dyn_infos with info = new_term} 
-			g
-		  | LetIn _ -> 
-		      let new_infos = 
-			{ dyn_infos with info = nf_betaoiotazeta dyn_infos.info } 
-		      in 
-
-		      tclTHENLIST 
-			[tclMAP 
-			   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
-			   dyn_infos.rec_hyps;
-			 h_reduce_with_zeta Tacticals.onConcl;
-			 do_prove_princ_for_struct do_finalize new_infos
-			] 
-			g
-		  | Cast(b,_,_) -> 
-		      do_prove_princ_for_struct do_finalize {dyn_infos with info = b } g
-		  | Case _ | Fix _ | CoFix _ ->
-		      let new_finalize dyn_infos = 
-			let new_infos = 
-			  { dyn_infos with 
-			      info = dyn_infos.info,args
-			  }
-			in 
-			do_prove_princ_for_struct_args do_finalize new_infos 
-		      in 
-		      do_prove_princ_for_struct new_finalize {dyn_infos  with info = f } g
-	      end
-	  | Fix _ | CoFix _ ->
-	      error ( "Anonymous local (co)fixpoints are not handled yet")
-
-	  | Prod _ -> assert false
-	  | LetIn _ -> 
-	      let new_infos = 
-		{ dyn_infos with 
-		    info = nf_betaoiotazeta dyn_infos.info 
-		}
-	      in 
-
-	      tclTHENLIST 
-		[tclMAP 
-		   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) 
-		   dyn_infos.rec_hyps;
-		 h_reduce_with_zeta Tacticals.onConcl;
-		 do_prove_princ_for_struct do_finalize new_infos
-		] g
-	  | Rel _ -> anomaly "Free var in goal conclusion !" 
-  and do_prove_princ_for_struct do_finalize dyn_infos g =
-(*     observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *)
-     (do_prove_princ_for_struct_aux do_finalize dyn_infos) g
-  and do_prove_princ_for_struct_args do_finalize dyn_infos (* f_args'  args *) :tactic =
-    fun g ->
-(*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
-(*      then msgnl (str "do_prove_princ_for_struct_args with "  ++  *)
-(* 		   pr_lconstr_env (pf_env g) f_args' *)
-(* 		); *)
-      let (f_args',args) = dyn_infos.info in 
-      let tac : tactic =
-	fun g -> 
-	match args with
-	  | []  ->
-	      do_finalize {dyn_infos with info = f_args'} g 
-	  | arg::args ->
-		observe (str "do_prove_princ_for_struct_args with arg := "++ pr_lconstr_env (pf_env g) arg++
-			fnl () ++ 
-			pr_goal (Tacmach.sig_it g)
-			);
-	      let do_finalize dyn_infos =
-		let new_arg = dyn_infos.info in 
-		(* 		tclTRYD *)
-		(do_prove_princ_for_struct_args
-		   do_finalize
-		   {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
-		)
-	      in
-	      do_prove_princ_for_struct do_finalize 
-		{dyn_infos with info = arg }
-		g
-      in
-      observe_tac "do_prove_princ_for_struct_args" (tac ) g
-   in
-   let do_finish_proof dyn_infos = 
-     (* tclTRYD *) (clean_goal_with_heq 
-      static_infos
-      finish_proof dyn_infos)
-  in
-  observe_tac "do_prove_princ_for_struct"
-    (do_prove_princ_for_struct do_finish_proof dyn_infos) 
-
-let is_pte_type t =
-  isSort (snd (decompose_prod t))
-    
-let is_pte (_,_,t) = is_pte_type t
-
-exception Not_Rec
-
-
-    
-
-let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic =
-   fun goal ->
-(*      observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++  *)
-(* 		pr_lconstr (mkConst fnames.(fun_num))); *)
-     let princ_type = pf_concl goal in
-     let princ_info = compute_elim_sig princ_type in
-     let get_body const =
-       match (Global.lookup_constant const ).const_body with
-	 | Some b ->
-	     let body = force b in
-	     Tacred.cbv_norm_flags
-	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
-	       (Global.env ())
-	       (Evd.empty)
-	       body
-	 | None -> error ( "Cannot define a principle over an axiom ")
-     in
-     let fbody = get_body fnames.(fun_num) in
-     let params : identifier list ref = ref [] in
-     let predicates : identifier list ref = ref [] in
-     let args : identifier list ref = ref [] in
-     let branches : identifier list ref = ref [] in
-     let pte_to_fix = ref Idmap.empty in
-     let fbody_with_params = ref None in
-     let intro_with_remembrance  ref number : tactic =
-       tclTHEN
-	 ( tclDO number intro )
-	 (fun g ->
-	    let last_n = list_chop number (pf_hyps g) in
-	    ref :=  List.map (fun (id,_,_) -> id) (fst last_n)@ !ref;
-	    tclIDTAC g
-	 )
-     in
-     let rec partial_combine body params =
-       match kind_of_term body,params with
-	 | Lambda (x,t,b),param::params ->
-	     partial_combine (subst1 param b) params
-	 | Fix(infos),_ ->
-	     body,params, Some (infos)
-	 | _ -> body,params,None
-     in
-     let build_pte_to_fix (offset:int) params predicates
-	 ((idxs,fix_num),(na,typearray,ca))  (avoid,_) =
-(*        let true_params,_ =  list_chop offset params  in  *)
-       let true_params = List.rev params in
-       let avoid = ref avoid in
-       let res = list_fold_left_i
-	 (fun i acc pte_id  ->
-	    let this_fix_id = fresh_id !avoid "fix___" in
-	    avoid := this_fix_id::!avoid;
-(* 	    let this_body = substl (List.rev fnames_as_constr) ca.(i) in  *)
-	    let realargs,_ = decompose_lam ca.(i) in 
-	    let n_realargs = List.length realargs - List.length params in 
-	    observe (str "n_realargs := " ++ str (string_of_int n_realargs));
-	    observe (str "n_fix := " ++ str (string_of_int(Array.length ca)));
-	    observe (str "body := " ++ pr_lconstr ca.(i));
-
-	    let new_type = prod_applist typearray.(i) true_params in
-	    let new_type_args,_ = decompose_prod new_type in
-	    let nargs = List.length new_type_args in
-	    let pte_args =
-	      (* 	      let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in  *)
-	      let f = applist((* all_funs *)mkConst fnames.(i),true_params) in
-	      let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in
-	      (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f]
-	    in
-	    let app_pte = applist(mkVar pte_id,pte_args) in
-	    let new_type = compose_prod new_type_args app_pte in
-	    
-	    let fix_info = 
-	      {
-		idx = idxs.(i) - offset + 1;
-		name = this_fix_id; 
-		types = new_type;
-		nb_realargs = n_realargs
-	      }
-	    in
-	    pte_to_fix := Idmap.add  pte_id fix_info !pte_to_fix;
-	    fix_info::acc
-	 )
-	 0
-	 []
-	 predicates
-       in
-       !avoid,List.rev res
-     in
-     let mk_fixes : tactic =
-       fun g ->
-	 let body_p,params',fix_infos =
-	   partial_combine fbody (List.rev_map mkVar  !params)
-	 in
-	 fbody_with_params := Some body_p;
-	 let offset  = List.length params' in
-	 let not_real_param,true_params =
-	   list_chop
-	     ((List.length !params ) - offset)
-	     !params
-	 in
-	 params := true_params; args := not_real_param;
-(* 	 observe (str "mk_fixes : params are "++  *)
-(* 		    prlist_with_sep spc *)
-(* 		    (fun id -> pr_lconstr (mkVar id)) *)
-(* 		    !params *)
-(* 		 ); *)
-	 let new_avoid,infos =
-	   option_fold_right
-	     (build_pte_to_fix
-		offset
-		(List.map mkVar !params)
-		(List.rev !predicates)
-	     )
-	     fix_infos
-	     ((pf_ids_of_hyps g),[])
-	 in
-	 let pre_info,infos = list_chop fun_num infos in
-	 match pre_info,infos with
-	   | [],[] -> tclIDTAC g
-	   | _,this_fix_info::infos' ->
-	       let other_fix_info =
-		 List.map 
-		   (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types) 
-		   (pre_info@infos')
-	       in
-	       tclORELSE
-		 (h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info)
-		 (tclFAIL 1000 (str "bad index" ++ 
-				  str (string_of_int this_fix_info.idx) ++
-				  str "offset := " ++
-				  (str (string_of_int offset))))
-		 g
-	   | _,[] -> anomaly "Not a valid information"
-     in
-     let do_prove ptes_to_fixes args branches : tactic =
-       fun g ->
-	 let static_infos = 
-	   {
-	     ptes_to_fixes = ptes_to_fixes;
-	     fixes_ids = 
-	       Idmap.fold 
-		 (fun _ fix_info acc -> fix_info.name::acc) 
-		 ptes_to_fixes []
-	   }
-	 in
-	 let nb_intros_to_do = List.length (fst (Sign.decompose_prod_assum (pf_concl g))) in 
-	 observe (str "nb_intros_to_do " ++ str (string_of_int nb_intros_to_do));
-	 tclTHEN 
-	   (tclDO nb_intros_to_do intro)
-	   (fun g -> 
-	      match kind_of_term (pf_concl g) with
-		| App(pte,pte_args) when isVar pte ->
-		    begin
-		      let pte = destVar pte in
-		      try
-			if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec;
-			let nparams = List.length !params in
-			let args_as_constr = List.map mkVar  args in
-			let other_args = fst (list_chop nb_intros_to_do (pf_ids_of_hyps g)) in 
-			let other_args_as_constr = List.map mkVar  other_args in 
-			let rec_num,new_body =
-			  let idx' = list_index pte (List.rev !predicates)  - 1 in
-			  let f = fnames.(idx') in
-			  let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly ""
-			  in
-			  let name_of_f = Name ( id_of_label (con_label f)) in
-			  let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in
-			  let idx'' = list_index name_of_f (Array.to_list na) - 1 in
-			  let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in
-			  let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in
-			  rec_nums.(idx'') - nparams ,body
-			in
-			let applied_body_with_real_args =
-			  Reductionops.nf_beta
-			    (applist(new_body,List.rev args_as_constr))
-			in
-			let applied_body = 
-			  Reductionops.nf_beta
-			    (applist(applied_body_with_real_args,List.rev other_args_as_constr))
-			in
-			observe (str "applied_body_with_real_args := "++ pr_lconstr_env (pf_env g) applied_body_with_real_args);
-			observe (str "applied_body := "++ pr_lconstr_env (pf_env g) applied_body);
-			let do_prove branches applied_body =
-			  do_prove_princ_for_struct
-			    interactive_proof
-			    (Array.to_list fnames)
-			    static_infos
-			    branches
-			    applied_body
-			in
-			let replace_and_prove =
-			  tclTHENS
-			    (fun g -> (Equality.replace (array_last pte_args) applied_body) g)
-			    [
-			      tclTHENLIST 
-				[
-				  generalize other_args_as_constr;
-				  thin other_args;
-				  clean_goal_with_heq 
-				    static_infos do_prove 
-				    {
-				      nb_rec_hyps = List.length branches;
-				      rec_hyps = branches;
-				      info = applied_body_with_real_args;
-				      eq_hyps = [];
-				    } ];
-			      let id = try List.nth (List.rev args_as_constr) (rec_num) with _ -> anomaly ("Cannot find recursive argument of function ! ") in
-			      let id_as_induction_constr = Tacexpr.ElimOnConstr id in 
-			      (tclTHENSEQ
-				 [Tactics.new_destruct [id_as_induction_constr] None Genarg.IntroAnonymous;(* (h_simplest_case id) *)
-				  Tactics.intros_reflexivity
-				 ])
-			    ]
-			in
-			(observe_tac "doing replacement" ( replace_and_prove)) g
-		      with Not_Rec ->
-			let fname = destConst (fst (decompose_app (array_last pte_args))) in
-			tclTHEN
-		     (unfold_in_concl [([],Names.EvalConstRef fname)])
-			  (observe_tac "" 
-			     (fun g' ->
-				let body = array_last (snd (destApp (pf_concl g'))) in 
-				let dyn_infos = 
-				  { nb_rec_hyps = List.length branches;
-				    rec_hyps = branches;
-				    info = body;
-				    eq_hyps = []
-				  }
-				in
-				let do_prove = 
-				  do_prove_princ_for_struct
-			       interactive_proof
-				    (Array.to_list fnames)
-				    static_infos
-				in
-				clean_goal_with_heq static_infos
-				  do_prove dyn_infos g'
-			     )
-			  )
-			  g
-		    end
-		| _ -> assert false
-	   ) g
-     in
-     tclTHENSEQ
-       [
-	 (fun g -> observe_tac "introducing params" (intro_with_remembrance  params princ_info.nparams) g);
-	 (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates  princ_info.npredicates) g);
-	 (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g);
-	 (fun g -> observe_tac "declaring fix(es)" mk_fixes g);
-	 (fun g -> 
-	    let nb_real_args = 
-	      let pte_app = snd (Sign.decompose_prod_assum (pf_concl g)) in 
-	      let pte = fst (decompose_app pte_app) in
-	      try 
-		let fix_info = Idmap.find (destVar pte) !pte_to_fix in
-		fix_info.nb_realargs
-	      with Not_found -> (* Not a recursive function *) 
-		nb_prod (pf_concl g)
-	    in 
-	    observe_tac "" (tclTHEN
-	      (tclDO nb_real_args (observe_tac "intro" intro)) 
-	      (fun g' -> 
-		 let realargs_ids = fst (list_chop ~msg:"args" nb_real_args (pf_ids_of_hyps g')) in 
-		 let do_prove_on_branches branches : tactic =
-		   observe_tac "proving" (do_prove !pte_to_fix ( realargs_ids) branches)
-		 in
-		 observe_tac "instanciating rec hyps"
-		   (instanciate_hyps_with_args do_prove_on_branches !branches  (List.rev realargs_ids))
-		   g'
-	      ))
-	      g
-	 )
-       ]
-       goal
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-  
-exception Toberemoved_with_rel of int*constr
-exception Toberemoved
-  
-let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
-  let princ_type_info = compute_elim_sig princ_type in 
-  let env = Global.env () in 
-(*   let type_sort = (Termops.new_sort_in_family InType) in  *)
-  let change_predicate_sort i (x,_,t) = 
-    let new_sort = sorts.(i) in
-    let args,_ = decompose_prod t in 
-    let real_args = 
-      if princ_type_info.indarg_in_concl 
-      then List.tl args 
-      else args
-    in
-    x,None,compose_prod real_args (mkSort new_sort) 
-  in
-  let new_predicates = 
-    list_map_i
-      change_predicate_sort 
-      0
-      princ_type_info.predicates
-  in
-  let env_with_params_and_predicates = 
-    Environ.push_rel_context 
-      new_predicates
-      (Environ.push_rel_context 
-	 princ_type_info.params 
-	 env
-      )
-  in
-  let rel_as_kn = 
-    fst (match princ_type_info.indref with
-	   | Some (Libnames.IndRef ind) -> ind 
-	   | _ -> failwith "Not a valid predicate"
-	)
-  in
-  let pre_princ = 
-    it_mkProd_or_LetIn 
-      ~init:
-      (it_mkProd_or_LetIn 
-	 ~init:(option_fold_right
-			   mkProd_or_LetIn
-			   princ_type_info.indarg
-			   princ_type_info.concl
-			)
-	 princ_type_info.args
-      )
-      princ_type_info.branches
-  in
-  let is_dom c =
-    match kind_of_term c with
-      | Ind((u,_)) -> u = rel_as_kn
-      | Construct((u,_),_) -> u = rel_as_kn
-      | _ -> false
-  in
-  let get_fun_num c =
-    match kind_of_term c with
-      | Ind(_,num) -> num
-      | Construct((_,num),_) -> num
-      | _ -> assert false
-  in
-  let dummy_var = mkVar (id_of_string "________") in
-  let mk_replacement c i args =
-    let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in 
-(*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
-    res
-  in
-  let rec has_dummy_var t  =
-    fold_constr
-      (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
-      false
-      t
-  in
-  let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
-    let (new_princ_type,_) as res =
-      match kind_of_term pre_princ with
-	| Rel n ->
-	    begin
-	      try match Environ.lookup_rel n env with
-		| _,_,t when is_dom t -> raise Toberemoved
-		| _ -> pre_princ,[] with Not_found -> assert false
-	    end
-	| Prod(x,t,b) ->
-	    compute_new_princ_type_for_binder remove mkProd env x t b
-	| Lambda(x,t,b) ->
-	    compute_new_princ_type_for_binder remove mkLambda env x t b
-	| Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
-	| App(f,args) when is_dom f ->
-	    let var_to_be_removed = destRel (array_last args) in
-	    let num = get_fun_num f in
-	    raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args))
-	| App(f,args) ->
-	    let is_pte = 
-	      match kind_of_term f with 
-		| Rel n ->  
-		    is_pte (Environ.lookup_rel n env)
-		| _ -> false 
-	    in
-	    let args = 
-	      if is_pte && remove 
-	      then array_get_start args 
-	      else args 
-	    in
-	    let new_args,binders_to_remove =
-	      Array.fold_right (compute_new_princ_type_with_acc remove env)
-		args
-		([],[])
-	    in
-	    let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
-	    applist(new_f, new_args),
-	    list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
-	| LetIn(x,v,t,b) ->
-	    compute_new_princ_type_for_letin remove env x v t b
-	| _ -> pre_princ,[]
-    in
-(*     observennl ( *)
-(*       match kind_of_term pre_princ with  *)
-(* 	| Prod _ ->  *)
-(* 	    str "compute_new_princ_type for "++ *)
-(* 	      pr_lconstr_env env pre_princ ++ *)
-(* 	      str" is "++ *)
-(* 	      pr_lconstr_env env new_princ_type ++ fnl () *)
-(* 	| _ -> str "" *)
-(*     ); *)
-    res
-	
-  and compute_new_princ_type_for_binder remove bind_fun env x t b =
-    begin
-      try
-	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
-	let new_x : name = get_name (ids_of_context env) x in
-	let new_env = Environ.push_rel (x,None,t) env in
-	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
-	else
-	  (
-	    bind_fun(new_x,new_t,new_b),
-	    list_union_eq
-	      eq_constr
-	      binders_to_remove_from_t
-	      (List.map pop binders_to_remove_from_b)
-	  )
-	
-      with
-	| Toberemoved ->
-(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = compute_new_princ_type  remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map pop binders_to_remove_from_b
-	| Toberemoved_with_rel (n,c) ->
-(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = compute_new_princ_type  remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
-    end
-  and compute_new_princ_type_for_letin remove env x v t b =
-    begin
-      try
-	let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in
-	let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in
-	let new_x : name = get_name (ids_of_context env) x in
-	let new_env = Environ.push_rel (x,Some v,t) env in
-	let new_b,binders_to_remove_from_b = compute_new_princ_type remove  new_env b in
-	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
-	else
-	  (
-	    mkLetIn(new_x,new_v,new_t,new_b),
-	    list_union_eq
-	      eq_constr
-	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
-	      (List.map pop binders_to_remove_from_b)
-	  )
-	
-      with
-	| Toberemoved ->
-(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
-	    new_b, List.map pop binders_to_remove_from_b
-	| Toberemoved_with_rel (n,c) ->
-(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
-    end
-  and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
-	      let new_e,to_remove_from_e = compute_new_princ_type remove env e
-	      in
-	      new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
-  in
-(*   observe (str "Computing new principe from " ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
-  let pre_res,_ = 
-    compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in 
-  it_mkProd_or_LetIn  	 
-    ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates)
-    princ_type_info.params
-    
-  
-
-let change_property_sort toSort princ princName = 
-  let princ_info = compute_elim_sig princ in 
-  let change_sort_in_predicate (x,v,t) = 
-    (x,None,
-     let args,_ = decompose_prod t in 
-     compose_prod args (mkSort toSort)
-    )
-  in 
-  let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in 
-  let init = 
-    let nargs =  (princ_info.nparams + (List.length  princ_info.predicates)) in 
-    mkApp(princName_as_constr,
-	  Array.init nargs
-	    (fun i -> mkRel (nargs - i )))
-  in
-  it_mkLambda_or_LetIn
-    ~init: 
-    (it_mkLambda_or_LetIn ~init 
-       (List.map change_sort_in_predicate princ_info.predicates)
-    )
-    princ_info.params
-    
-
-let pp_dur time time' = 
-  str (string_of_float (System.time_difference time time'))
-
-(* Things to be removed latter : just here to compare 
-   saving proof with and without  normalizing the proof 
-*)
-let new_save id const (locality,kind) hook =
-  let {const_entry_body = pft;
-       const_entry_type = tpo;
-       const_entry_opaque = opacity } = const in
-  let l,r = match locality with
-    | Decl_kinds.Local when Lib.sections_are_opened () ->
-        let k = Decl_kinds.logical_kind_of_goal_kind kind in
-	let c = Declare.SectionLocalDef (pft, tpo, opacity) in
-	let _ = Declare.declare_variable id (Lib.cwd(), c, k) in
-	(Decl_kinds.Local, Libnames.VarRef id)
-    | Decl_kinds.Local ->
-        let k = Decl_kinds.logical_kind_of_goal_kind kind in
-        let kn = Declare.declare_constant id (DefinitionEntry const, k) in
-	(Decl_kinds.Global, Libnames.ConstRef kn)
-    | Decl_kinds.Global ->
-        let k = Decl_kinds.logical_kind_of_goal_kind kind in
-        let kn = Declare.declare_constant id (DefinitionEntry const, k) in
-	(Decl_kinds.Global, Libnames.ConstRef kn) in
-  let time1 = System.get_time () in
-  Pfedit.delete_current_proof ();
-  let time2 = System.get_time () in
-  hook l r;
-  time1,time2
-(*   definition_message id *)
-
-
-
-
-
-let new_save_named opacity =
-(*   if do_observe ()  *)
-(*   then  *)
-  let time1 = System.get_time () in 
-    let id,(const,persistence,hook) = Pfedit.cook_proof () in
-    let time2 = System.get_time () in 
-    let const = 
-      { const with 
-	  const_entry_body = (* nf_betaoiotazeta  *)const.const_entry_body ;
-	  const_entry_opaque = opacity
-      }
-    in
-    let time3 = System.get_time ()  in
-    let time4,time5 = new_save id const persistence hook in
-    let time6 = System.get_time () in 
-    Pp.msgnl
-      (str "cooking proof time : " ++ pp_dur time1 time2 ++ fnl () ++
-	 str "reducing proof time : " ++ pp_dur time2 time3 ++ fnl () ++
-	 str "saving proof time : " ++ pp_dur time3 time4 ++fnl () ++
-	 str "deleting proof time : " ++ pp_dur time4 time5 ++fnl () ++
-	 str "hook time :" ++ pp_dur time5 time6
-      )
-       
-;;
-
-(* End of things to be removed latter : just here to compare 
-   saving proof with and without  normalizing the proof 
-*)
-
-
-let generate_functional_principle 
-    interactive_proof
-    old_princ_type sorts new_princ_name funs i proof_tac 
-    = 
-  let f = funs.(i) in 
-  let type_sort = Termops.new_sort_in_family InType in 
-  let new_sorts = 
-    match sorts with 
-      | None -> Array.make (Array.length funs) (type_sort)
-      | Some a -> a
-  in
-  (* First we get the type of the old graph principle *)
-  let mutr_nparams = (compute_elim_sig old_princ_type).nparams in 
-  (* First we get the type of the old graph principle *)
-   let new_principle_type =
-    compute_new_princ_type_from_rel
-      (Array.map mkConst funs)
-      new_sorts
-      old_princ_type
-   in
-(*    observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
-  let base_new_princ_name,new_princ_name =
-    match new_princ_name with
-      | Some (id) -> id,id
-      | None ->
-	  let id_of_f = id_of_label (con_label f) in
-	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
-  in
-  let names = ref [new_princ_name] in 
-  let hook _ _  =
-    if sorts = None 
-    then
-(*     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 base_new_princ_name fam_sort in
-      let value =
-	change_property_sort s new_principle_type new_princ_name
-      in
-(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-      let ce =
-	{ const_entry_body = value;
-	  const_entry_type = None;
-	  const_entry_opaque = false;
-	  const_entry_boxed = Options.boxed_definitions()
-	}
-      in
-      ignore(
-	Declare.declare_constant
-	  name
-	  (Entries.DefinitionEntry ce,
-	   Decl_kinds.IsDefinition (Decl_kinds.Scheme)
-	  )
-      );
-      names := name :: !names
-    in
-    register_with_sort InProp;
-    register_with_sort InSet
-  in
-  begin
-    Command.start_proof
-      new_princ_name
-      (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
-      new_principle_type
-      hook
-    ;
-    try
-      let _tim1 = System.get_time ()  in
-      Pfedit.by  (proof_tac (Array.map mkConst funs) mutr_nparams);
-      let _tim2 =  System.get_time ()  in
-(* 	begin *)
-(* 	  let dur1 = System.time_difference tim1 tim2 in *)
-(* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
-(* 	end; *)
-      let do_save =  not (do_observe ()) && not interactive_proof in 
-      let _ = 
-	try 
-	  Options.silently Command.save_named true;
-	  let _dur2 = System.time_difference _tim2 (System.get_time ()) in
-(* 	  Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *)
-	  Options.if_verbose 
-	    (fun () -> 
-	       Pp.msgnl (
-		 prlist_with_sep
-		   (fun () -> str" is defined " ++ fnl ()) 
-		   Ppconstr.pr_id
-		   (List.rev !names) ++ str" is defined " 
-	       )
-	    ) 
-	       ()
-	with e when do_save -> 
-	  msg_warning
-	    (
-	      Cerrors.explain_exn e
-	    );
-	  if not (do_observe ())
-	  then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
-      in
-      ()
-
-(*       let tim3 = Sys.time ()  in *)
-(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *)
-
-    with
-      | e ->
-	  msg_warning
-	    (
-	      Cerrors.explain_exn e
-	    );
-	  if not ( do_observe ())
-	  then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
-  end
-
-
-
-
-
-
-let get_funs_constant mp dp = 
-  let rec get_funs_constant const e : (Names.constant*int) array = 
-    match kind_of_term (snd (decompose_lam e)) with 
-      | Fix((_,(na,_,_))) -> 
-	  Array.mapi 
-	    (fun i na -> 
-	       match na with 
-		 | Name id -> 
-		     let const = make_con mp dp (label_of_id id) in 
-		     const,i
-		 | Anonymous -> 
-		     anomaly "Anonymous fix" 
-	    )
-	    na
-      | _ -> [|const,0|]
-  in
-  function const -> 
-    let find_constant_body const = 
-      match (Global.lookup_constant const ).const_body with
-	| Some b ->
-	    let body = force b in
-	    let body = Tacred.cbv_norm_flags
-	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
-	      (Global.env ())
-	      (Evd.empty)
-	      body
-	    in
-	    body
-	| None -> error ( "Cannot define a principle over an axiom ")
-    in
-    let f = find_constant_body const in
-    let l_const = get_funs_constant const f in 
-    (* 
-       We need to check that all the functions found are in the same block 
-       to prevent Reset stange thing
-    *) 
-    let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in 
-    let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in 
-    (* all the paremeter must be equal*) 
-    let _check_params = 
-      let first_params = List.hd l_params  in 
-      List.iter 
-	(fun params -> 
-	   if not ((=) first_params params) 
-	   then error "Not a mutal recursive block"
-	)
-	l_params
-    in
-    (* The bodies has to be very similar *) 
-    let _check_bodies = 
-      try 
-	let extract_info is_first body = 
-	  match kind_of_term body with 
-	    | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
-	    | _ -> 
-		if is_first && (List.length l_bodies = 1) 
-		then raise Not_Rec
-		else error "Not a mutal recursive block"
-	in
-	let first_infos = extract_info true (List.hd l_bodies) in 
-	let check body  = (* Hope this is correct *)
-	  if not (first_infos = (extract_info false body)) 
-	  then  error "Not a mutal recursive block"
-	in 
-	List.iter check l_bodies
-      with Not_Rec -> ()
-    in
-    l_const
-	
-let make_scheme fas = 
-  let env = Global.env () 
-  and sigma = Evd.empty in
-  let id_to_constr id = 
-    Tacinterp.constr_of_id env  id
-  in 
-  let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in 
-  let first_fun = destConst (List.hd funs) in 
-  let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in 
-  let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in 
-  let first_fun_kn = 
-    (* Fixme: take into accour funs_mp and funs_dp *)
-    fst (destInd (id_to_constr first_fun_rel_id))
-  in
-  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
-  let this_block_funs = Array.map fst this_block_funs_indexes in 
-  let prop_sort = InProp in
-  let funs_indexes = 
-    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
-    List.map
-      (function const -> List.assoc (destConst const) this_block_funs_indexes)
-      funs
-  in
-  let ind_list = 
-    List.map 
-      (fun (idx) -> 
-	 let ind = first_fun_kn,idx in 
-	 let (mib,mip) = Global.lookup_inductive ind in
-	 ind,mib,mip,true,prop_sort
-      )
-      funs_indexes
-  in
-  let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in 
-  let i = ref (-1) in
-  let sorts = 
-    List.rev_map (fun (_,_,x) -> 
-		Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
-	     ) 
-      fas 
-  in
-  let princ_names = List.map (fun (x,_,_) -> x) fas in 
-  let _ = List.map2
-    (fun princ_name scheme_type -> 
-       incr i;
-(*        observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
-(* 	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
-(* 	       ); *)
-       generate_functional_principle
-	 false
-	 scheme_type
-	 (Some (Array.of_list sorts))
-	 (Some princ_name)
-	 this_block_funs
-	 !i
-	 (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs)))
-    )
-    princ_names
-    l_schemes 
-  in
-  ()
-
-let make_case_scheme fa = 
-  let env = Global.env () 
-  and sigma = Evd.empty in
-  let id_to_constr id = 
-    Tacinterp.constr_of_id env  id
-  in 
-  let funs =  (fun (_,f,_) -> id_to_constr f) fa in 
-  let first_fun = destConst  funs in 
-  let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in 
-  let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in 
-  let first_fun_kn = 
-    (* Fixme: take into accour funs_mp and funs_dp *)
-    fst (destInd (id_to_constr first_fun_rel_id))
-  in
-  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
-  let this_block_funs = Array.map fst this_block_funs_indexes in 
-  let prop_sort = InProp in
-  let funs_indexes = 
-    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
-    List.assoc (destConst funs) this_block_funs_indexes
-  in
-  let ind_fun = 
-	 let ind = first_fun_kn,funs_indexes in 
-	 ind,prop_sort
-  in
-  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in 
-  let sorts =
-    (fun (_,_,x) ->
-       Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
-    )
-      fa
-  in
-  let princ_name =  (fun (x,_,_) -> x) fa in
-  let _ = 
-(*     observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
-(* 	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
-(* 	    ); *)
-    generate_functional_principle
-      false
-      scheme_type
-      (Some ([|sorts|]))
-      (Some princ_name)
-      this_block_funs
-      0
-      (prove_princ_for_struct false 0 [|destConst funs|])
-  in
-  ()
diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli
deleted file mode 100644
index cad68da67..000000000
--- a/contrib/funind/new_arg_principle.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-
-val generate_functional_principle : 
-  (* do we accept interactive proving *)
-  bool ->
-  (* induction principle on rel *) 
-  Term.types ->
-  (* *)
-  Term.sorts array option -> 
-  (* Name of the new principle *) 
-  (Names.identifier) option -> 
-  (* 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
-  *)
-  (Term.constr array -> int -> Tacmach.tactic) -> 
-  unit
-
-
-
-(* val my_reflexivity : Tacmach.tactic  *)
-
-val prove_princ_for_struct : 
-  bool -> 
-  int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic
-
-
-val compute_new_princ_type_from_rel : Term.constr array -> Term.sorts array -> 
-  Term.types -> Term.types
-
-val make_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) list ->  unit
-val make_case_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort)  ->  unit
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 681e43af0..e52688dc0 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -17,18 +17,11 @@ let observennl strm =
   then Pp.msg strm 
   else ()
 
-(* 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
 
@@ -44,8 +37,6 @@ let compose_raw_context =
       | 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
   
@@ -245,11 +236,6 @@ let combine_prod n t b =
 let combine_letin n t b = 
   { 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 = 
   { 
@@ -624,7 +610,6 @@ 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 those_pattern_preconds =
 (	  List.flatten
 	    (
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index c2410d55c..a12f1f01f 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -378,7 +378,7 @@ let rec proofPrinc mi: constr funind =
   (* <pcase> Cases b of arrPt end.*)
   | Case (cinfo, pcase, b, arrPt) -> 
      let prod_pcase,_ = decompose_lam pcase in
-     let nmeb,_ = List.hd prod_pcase in
+     let _nmeb,_ = List.hd prod_pcase in
      let newb'= apply_leqtrpl_t b mi.lst_eqs in
      let type_of_b = Typing.type_of mi.env mi.sigma b in
      (* Replace the recursive calls to the function by calls to the constant *)
@@ -428,7 +428,7 @@ let rec proofPrinc mi: constr funind =
      let varnames = List.map snd mi.lst_vars in
      let nb_vars = List.length varnames in
      let nb_eqs = List.length mi.lst_eqs in
-     let eqrels = List.map fst mi.lst_eqs in
+     let _eqrels = List.map fst mi.lst_eqs in
      (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
         trouvés dans les let in et les Cases avec ceux trouves dans u (ie
         mi.mimick). *)