Julien:

+ Induction principle for general recursion
+ Bug correction in structural principles


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

5 files changed, 845 insertions, 446 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 56855f5da..606352d22 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -29,7 +29,7 @@ let interp_casted_constr_with_implicits sigma env impls c  =
     ~allow_soapp:false  ~ltacvars:([],[]) c
 
 let build_newrecursive
-(lnameargsardef:(newfixpoint_expr ) list)  =
+(lnameargsardef)  =
   let env0 = Global.env()
   and sigma = Evd.empty
   in
@@ -69,9 +69,9 @@ let compute_annot (name,annot,args,types,body) =
   match annot with
     | None ->
         if List.length names > 1 then
-            user_err_loc
-              (dummy_loc,"GenFixpoint",
-               Pp.str "the recursive argument needs to be specified");
+          user_err_loc
+            (dummy_loc,"GenFixpoint",
+             Pp.str "the recursive argument needs to be specified");
         let new_annot = (id_of_name (List.hd names)) in
 	(name,Struct new_annot,args,types,body)
     | Some r -> (name,r,args,types,body)
@@ -159,10 +159,10 @@ let register_struct is_rec fixpoint_exprl =
 	Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
 
 
-let generate_correction_proof_wf  
+let generate_correction_proof_wf tcc_lemma_ref   
     is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
     (_: int) (_:Names.constant array) (_:int) : Tacmach.tactic = 
-  Recdef.prove_principle 
+  Recdef.prove_principle  tcc_lemma_ref
     is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 
 
@@ -201,11 +201,16 @@ 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 f_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
-    pre_hook 
-      (generate_correction_proof_wf is_mes
-	 f_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-      )
+  let hook tcc_lemma_ref f_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
+	);
+      Command.save_named true
+    with e -> 
+      (* No proof done *) 
+      ()
   in 
   Recdef.recursive_definition 
     is_mes fname 
@@ -261,11 +266,11 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body =
 
 
 
-let register (fixpoint_exprl :  newfixpoint_expr list) = 
+let do_generate_principle fixpoint_exprl  = 
   let recdefs = build_newrecursive fixpoint_exprl in 
   let _is_struct = 
     match fixpoint_exprl with 
-      | [((name,Wf (wf_rel,wf_x),args,types,body))] -> 
+      | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      fixpoint_exprl 
@@ -275,7 +280,7 @@ let register (fixpoint_exprl :  newfixpoint_expr list) =
 	  in 
 	  register_wf name wf_rel wf_x args types body pre_hook;
 	  false
-      | [((name,Mes (wf_mes,wf_x),args,types,body))] -> 
+      | [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      fixpoint_exprl 
@@ -284,14 +289,16 @@ let register (fixpoint_exprl :  newfixpoint_expr list) =
 	      false
 	  in 
 	  register_mes name wf_mes wf_x args types body pre_hook;
-
 	  false
       | _ -> 
-	  
+	  let fix_names = 
+	    List.map (function (name,_,_,_,_) -> name) fixpoint_exprl 
+	  in
+	  let is_one_rec = is_rec fix_names  in
 	  let old_fixpoint_exprl =  
-	    List.map 
+	    List.map
 	      (function
-		 | (name,Struct id,args,types,body) -> 
+		 | (name,Some (Struct id),args,types,body),_ -> 
 		     let names = 
 		       List.map
 			 snd
@@ -299,11 +306,19 @@ let register (fixpoint_exprl :  newfixpoint_expr list) =
 		     in 
 		     let annot = Util.list_index (Name id) names - 1 in 
  		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
-		 | (_,Wf _,_,_,_) | (_,Mes _,_,_,_)  -> 
+		 | (name,None,args,types,body),recdef -> 
+		     let names =  (Topconstr.names_of_local_assums args) in
+		     if  is_one_rec recdef  && List.length names > 1 then
+		       Util.user_err_loc
+			 (Util.dummy_loc,"GenFixpoint",
+			  Pp.str "the recursive argument needs to be specified")
+		     else 
+		       (name,0,args,types,body),(None:Vernacexpr.decl_notation)
+		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
 		       ("Cannot use mutual definition with well-founded recursion")
 	      ) 
-	      fixpoint_exprl 
+	      (List.combine fixpoint_exprl recdefs)
 	  in
 	  (* ok all the expressions are structural *) 
 	  let fix_names = 
@@ -323,10 +338,10 @@ let register (fixpoint_exprl :  newfixpoint_expr list) =
   ()
 
 
-let do_generate_principle fix_rec_l = 
-  (* we first of all checks whether on not all the correct 
-     assumption  are here 
-  *)
-  let newfixpoint_exprl = List.map compute_annot fix_rec_l in 
-  (* we can then register the functions *) 
-  register newfixpoint_exprl 
+(* let do_generate_principle fix_rec_l =  *)
+(*   (\* we first of all checks whether on not all the correct  *)
+(*      assumption  are here  *)
+(*   *\) *)
+(*   let newfixpoint_exprl = List.map compute_annot fix_rec_l in  *)
+(*   (\* we can then register the functions *\)  *)
+(*   register(\*  newfixpoint_exprl  *\) fix_rec_l *)
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index bbaa8b5a0..e7751c164 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -135,33 +135,34 @@ VERNAC ARGUMENT EXTEND rec_definition2
  [ ident(id)  binder2_list( bl)
      rec_annotation2_opt(annot) ":" lconstr( type_)
 	":=" lconstr(def)] ->
-          [let names = List.map snd (Topconstr.names_of_local_assums bl) in
-	   let check_one_name () =
-	     if List.length names > 1 then
-               Util.user_err_loc
-                 (Util.dummy_loc,"GenFixpoint",
-                  Pp.str "the recursive argument needs to be specified");
-	   in
-	   let check_exists_args an =
-	     try 
-	       let id = match an with Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" in 
-	       (try ignore(Util.list_index (Name id) names - 1); annot
-		with Not_found ->  Util.user_err_loc
-                  (Util.dummy_loc,"GenFixpoint",
-                   Pp.str "No argument named " ++ Nameops.pr_id id)
-	       )
-	     with Failure "check_exists_args" ->  check_one_name ();annot
-	   in
-          let ni =
-            match annot with
-              | None ->
-		  check_one_name ();
-                  annot
-	      | Some an ->
-		  check_exists_args an
-	  in
-	  (id, ni, bl, type_, def) ]
-END
+    [let names = List.map snd (Topconstr.names_of_local_assums bl) in
+     let check_one_name () =
+       if List.length names > 1 then
+         Util.user_err_loc
+           (Util.dummy_loc,"GenFixpoint",
+            Pp.str "the recursive argument needs to be specified");
+     in
+     let check_exists_args an =
+       try 
+	 let id = match an with Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" in 
+	 (try ignore(Util.list_index (Name id) names - 1); annot
+	  with Not_found ->  Util.user_err_loc
+            (Util.dummy_loc,"GenFixpoint",
+             Pp.str "No argument named " ++ Nameops.pr_id id)
+	 )
+       with Failure "check_exists_args" ->  check_one_name ();annot
+     in
+     let ni =
+       match annot with
+         | None ->
+(* 	     check_one_name (); *)
+             annot
+	     
+	 | Some an ->
+	     check_exists_args an
+     in
+     (id, ni, bl, type_, def) ]
+      END
 
 
 VERNAC ARGUMENT EXTEND rec_definitions2
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
index 56d0473d9..03eacea27 100644
--- a/contrib/funind/new_arg_principle.ml
+++ b/contrib/funind/new_arg_principle.ml
@@ -16,20 +16,14 @@ open Indfun_common
 
 (* let msgnl = Pp.msgnl *)
 
-let observe_tac s tac g =
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
-  then
-    let msgnl = Pp.msgnl in 
-    begin
-      msgnl (Printer.pr_goal (sig_it g));
-      try
-	let v = tclINFO tac g in msgnl (str s ++(str " ")++(str "finished")); v
-      with e ->
-	msgnl (str "observation "++ str s++str " raised an exception: "++Cerrors.explain_exn e); raise e
-    end
+let observe_tac s tac g = 
+  if Tacinterp.get_debug () <> Tactic_debug.DebugOff 
+  then Recdef.do_observe_tac s tac g
   else tac g
 
-let tclTRYD tac =  
+
+
+let tclTRYD tac =
   if  !Options.debug  ||  Tacinterp.get_debug () <> Tactic_debug.DebugOff
   then tclTRY tac
   else tac
@@ -60,13 +54,13 @@ let test_var args arg_num =
    
 
 
-let rewrite_until_var arg_num : tactic = 
+let rewrite_until_var arg_num : tactic =
   let constr_eq =  (Coqlib.build_coq_eq_data ()).Coqlib.eq in
-  let replace_if_unify arg (pat,cl,id,lhs)  : tactic = 
-    fun g -> 
-      try 
-	let (evd,matched) = 
-	  Unification.w_unify_to_subterm 
+  let replace_if_unify arg (pat,cl,id,lhs)  : tactic =
+    fun g ->
+      try
+	let (evd,matched) =
+	  Unification.w_unify_to_subterm
 	    (pf_env g) ~mod_delta:false (pat,arg) cl.Clenv.env
 	in
 	let cl' = {cl with Clenv.env = evd } in
@@ -74,8 +68,8 @@ let rewrite_until_var arg_num : tactic =
 	(Equality.replace matched c2) g
       with _ -> tclFAIL 0 (str "") g
   in
-  let rewrite_on_step equalities : tactic = 
-    fun g -> 
+  let rewrite_on_step equalities : tactic =
+    fun g ->
       match kind_of_term (pf_concl g) with
 	| App(_,args) when (not (test_var args arg_num)) ->
 (* 	    tclFIRST (List.map (fun a -> observe_tac (str "replace_if_unify") (replace_if_unify args.(arg_num) a)) equalities) g *)
@@ -84,303 +78,174 @@ let rewrite_until_var arg_num : tactic =
 	    raise (Util.UserError("", (str "No more rewrite" ++
 					 pr_lconstr_env (pf_env g) (pf_concl g))))
   in
-  fun g -> 
-    let equalities = 
-      List.filter  
-	( 
-	  fun (_,_,id_t) -> 
+  fun g ->
+    let equalities =
+      List.filter
+	(
+	  fun (_,_,id_t) ->
 	    match kind_of_term id_t with
-	      | App(f,_) -> eq_constr f constr_eq 
-	      | _ -> false 
+	      | App(f,_) -> eq_constr f constr_eq
+	      | _ -> false
 	)
 	(pf_hyps g)
     in
-    let f (id,_,ctype)  = 
+    let f (id,_,ctype)  =
       let c = mkVar id in
       let eqclause = Clenv.make_clenv_binding g (c,ctype) Rawterm.NoBindings in
       let clause_type = Clenv.clenv_type eqclause in
-      let f,args = decompose_app (clause_type) in 
+      let f,args = decompose_app (clause_type) in
       let rec split_last_two = function
 	| [c1;c2] -> (c1, c2)
 	| x::y::z ->
-	    split_last_two (y::z) 
-	| _ -> 
-	    error ("The term provided is not an equivalence") 
+	    split_last_two (y::z)
+	| _ ->
+	    error ("The term provided is not an equivalence")
       in
       let (c1,c2) = split_last_two args in
-      (c2,eqclause,id,c1) 
+      (c2,eqclause,id,c1)
     in
-    let matching_hyps = List.map f equalities in 
-    tclTRY (tclREPEAT (tclPROGRESS (rewrite_on_step matching_hyps))) g 
+    let matching_hyps = List.map f equalities in
+    tclTRY (tclREPEAT (tclPROGRESS (rewrite_on_step matching_hyps))) g
 
-      
-exception Toberemoved_with_rel of int*constr
-exception Toberemoved
-  
-let prov_pte_prefix = "_____PTE"
-  
-let is_pte_type t =
-  isSort (snd (decompose_prod t))
-    
-let is_pte (_,_,t) = is_pte_type t
-  
 
-let is_pte_id = 
-  let pref_length = String.length prov_pte_prefix in 
-  function  id -> 
-    String.sub (string_of_id id) 0 pref_length = prov_pte_prefix
 
-let compute_new_princ_type_from_rel  replace
-    (rel_as_kn:mutual_inductive)  =
-  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 i args = 
-    mkApp(replace.(i),Array.map pop (array_get_start args))
-  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 env pre_princ : types*(constr list) = 
-(*     let _tim1 = Sys.time() in *)
-    let (new_princ_type,_) as res = 
-      match kind_of_term pre_princ with
-	| Rel n ->
-	    begin
-	      match Environ.lookup_rel n env with
-		| _,_,t when is_dom t -> raise Toberemoved
-	      | _ -> pre_princ,[]
-	    end
-	| Prod(x,t,b) ->
-	    compute_new_princ_type_for_binder mkProd env x t b
-	| Lambda(x,t,b) ->
-	    compute_new_princ_type_for_binder 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 num args))
-	| App(f,args) ->
-	    let new_args,binders_to_remove =
-	      Array.fold_right (compute_new_princ_type_with_acc env)
-		args
-		([],[])
-	    in
-	    let new_f,binders_to_remove_from_f = compute_new_princ_type env f in
-	    mkApp(new_f,Array.of_list 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 env x v t b
-	| _ -> pre_princ,[]
-    in 
-(*     if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
-(*     then *)
-(*       msgnl (str "compute_new_princ_type for "++ *)
-(* 	       pr_lconstr_env env pre_princ ++ *)
-(* 	       str" is "++ *)
-(* 	       pr_lconstr_env env new_princ_type); *)
-      res
-	
-  and compute_new_princ_type_for_binder bind_fun env x t b = 
-    begin
-      try
-	let new_t,binders_to_remove_from_t = compute_new_princ_type 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 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  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  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 env x v t b = 
-    begin
-      try
-	let new_t,binders_to_remove_from_t = compute_new_princ_type env t in
-	let new_v,binders_to_remove_from_v = compute_new_princ_type 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 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  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  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 env e (c_acc,to_remove_acc)  =
-	      let new_e,to_remove_from_e = compute_new_princ_type env e
-	      in
-	      new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
-  in
-  compute_new_princ_type 
-
-
-let make_refl_eq type_of_t t  = 
+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|])
 
-let case_eq  tac body term g = 
+let case_eq  tac body term g =
 (*   msgnl (str "case_eq on " ++ pr_lconstr_env (pf_env g) term); *)
   let type_of_term = pf_type_of g term in
-  let term_eq = 
-    make_refl_eq type_of_term term 
-  in 
+  let term_eq =
+    make_refl_eq type_of_term term
+  in
   let ba_fun ba  : tactic =
-    fun g -> 
-      tclTHENSEQ 
+    fun g ->
+      tclTHENSEQ
 	[intro_patterns [](* ba.branchnames *);
-	 fun g -> 
-	   let (_,_,new_term_value_eq)  = pf_last_hyp g in 
-	   let new_term_value = 
-	     match kind_of_term new_term_value_eq with 
-	       | App(f,[| _;_;args2 |]) -> args2 
-	     | _ ->  
-		 Pp.msgnl (pr_gls g ++ fnl () ++ str "last hyp is" ++ 
+	 fun g ->
+	   let (_,_,new_term_value_eq)  = pf_last_hyp g in
+	   let new_term_value =
+	     match kind_of_term new_term_value_eq with
+	       | App(f,[| _;_;args2 |]) -> args2
+	     | _ ->
+		 Pp.msgnl (pr_gls g ++ fnl () ++ str "last hyp is" ++
 			     pr_lconstr_env (pf_env g) new_term_value_eq
 			  );
-		 assert false 
+		 assert false
 	   in
-	   let fun_body = 
+	   let fun_body =
 	     mkLambda(Anonymous,type_of_term,replace_term term (mkRel 1) body)
-	   in 
-	   let new_body = mkApp(fun_body,[| new_term_value |]) in 
+	   in
+	   let new_body = mkApp(fun_body,[| new_term_value |]) in
 	   tac (pf_nf_betaiota g new_body) g
 	]
 	g
   in
     (
-      tclTHENSEQ 
+      tclTHENSEQ
 	[
-	  generalize [term_eq];
+	  h_generalize [term_eq];
 	  pattern_option [[-1],term] None;
 	  case_then_using Genarg.IntroAnonymous (ba_fun) None ([],[]) term
-	] 
+	]
     )
     g
 
 
 
-let my_reflexivity : tactic = 
-  let test_eq = 
-    lazy (eq_constr (Coqlib.build_coq_eq ())) 
+let my_reflexivity : tactic =
+  let test_eq =
+    lazy (eq_constr (Coqlib.build_coq_eq ()))
   in
-  let build_reflexivity  = 
+  let build_reflexivity  =
     lazy (fun ty t -> mkApp((Coqlib.build_coq_eq_data ()).Coqlib.refl,[|ty;t|]))
   in
-  fun g -> 
+  fun g ->
     begin
-    match kind_of_term (pf_concl g) with 
-      | App(eq,[|ty;t1;t2|]) when (Lazy.force test_eq) eq -> 
-	    if not (Termops.occur_existential t1) 
+    match kind_of_term (pf_concl g) with
+      | App(eq,[|ty;t1;t2|]) when (Lazy.force test_eq) eq ->
+	    if not (Termops.occur_existential t1)
 	    then tclTHEN (h_change None (mkApp(eq,[|ty;t1;t1|]))  onConcl ) (apply ((Lazy.force build_reflexivity) ty t1))
-	    else if not (Termops.occur_existential t2) 
+	    else if not (Termops.occur_existential t2)
 	    then   tclTHEN (h_change None (mkApp(eq,[|ty;t2;t2|])) onConcl ) (apply ((Lazy.force build_reflexivity) ty t2))
 	    else tclFAIL 0 (str "")
 	      
       | _ -> tclFAIL 0 (str "")
     end g
 
-let exactify_proof rec_pos ptes_to_fix : tactic = 
-  let not_as_constant = Coqlib.build_coq_not  () in 
-  let or_as_ind =   Coqlib.build_coq_or () in 
-  let eq_not = eq_constr not_as_constant in 
+let exactify_proof rec_pos ptes_to_fix : tactic =
+  let not_as_constant = Coqlib.build_coq_not  () in
+  let or_as_ind =   Coqlib.build_coq_or () in
+  let eq_not = eq_constr not_as_constant in
   let eq_or = eq_constr or_as_ind in
-  let tac_res tac: tactic = 
-    fun g -> 
+  let tac_res tac: tactic =
+    fun g ->
       match kind_of_term (pf_concl g) with
 	| Prod _ -> tclTHEN intro tac g
-	| App(f,_) -> 
-	    if eq_not f 
+	| App(f,_) ->
+	    if eq_not f
 	    then tclTHEN (intro_force true) (tclABSTRACT None (Cctac.cc_tactic []))
 	      (* Equality.discr_tac None *) g
-	    else if eq_or f 
+	    else if eq_or f
 	    then
-	      tclSOLVE 
+	      tclSOLVE
 		[tclTHEN simplest_left tac;
 		 tclTHEN simplest_right tac
 		] g
 	    else
 	      begin
-		match rec_pos with 
-		  | Some rec_pos -> 
-		      begin 
-			match kind_of_term f with 
-			  | Var id -> 
+		match rec_pos with
+		  | Some rec_pos ->
+		      begin
+			match kind_of_term f with
+			  | Var id ->
 			      begin
 				try
 				  let fix_id = Idmap.find id ptes_to_fix in
-				let fix = mkVar (fix_id) in
-				tclTHEN 
-				  (rewrite_until_var rec_pos) 
-				  (Eauto.e_resolve_constr fix)
-				  g
-				with Not_found -> 
-(* 				Pp.msgnl (str "No fix found for "++ *)
-(* 					    pr_lconstr_env (pf_env g) f); *)
+				  let fix = mkVar (fix_id) in
+				  tclTHEN
+				    (rewrite_until_var rec_pos)
+				    (Eauto.e_resolve_constr fix)
+				    g
+				with Not_found ->
+				  (* 				Pp.msgnl (str "No fix found for "++ *)
+				  (* 					    pr_lconstr_env (pf_env g) f); *)
 				  tclFAIL 0 (str "No such fix found") g
 			      end
-			  | _ -> tclFAIL 0 (str "Not a variable : " 
-					    (* (string_of_pp (pr_lconstr_env (pf_env g) f)) *)
-					   ) g
+			  | _ -> 
+			      tclCOMPLETE 
+				(Eauto. gen_eauto false (false,5) [] (Some []))
+				(* (string_of_pp (pr_lconstr_env (pf_env g) f)) *)
+				g
 		      end
-		  | None -> tclFAIL 0 (str "Not a good term") g
+		  | None -> 
+		      tclCOMPLETE (Eauto. gen_eauto false (false,5) [] (Some [])) g
+		      
 	      end
 	| _ -> tclFAIL 0 (str "Not a good term") g
-   in 
-  let rec exactify_proof g = 
+   in
+  let rec exactify_proof g =
     tclFIRST
       [
 	tclSOLVE [my_reflexivity];
 	tclSOLVE [Eauto.e_assumption];
 	tclSOLVE [Tactics.reflexivity ];
-	tac_res exactify_proof
+	tac_res exactify_proof; 
+	tclCOMPLETE 
+	  (
+	    tclREPEAT
+	      (
+		tclPROGRESS 
+		  (tclTHEN 
+		     (rew_all LR) 
+		     (Eauto. gen_eauto false (false,5) [] (Some []))
+		  )
+	      )
+	  )
       ] g
   in
-  observe_tac "exactify_proof with " exactify_proof 
+  observe_tac "exactify_proof with " exactify_proof
     
 
 let reduce_fname fnames : tactic =
@@ -395,13 +260,13 @@ let reduce_fname fnames : tactic =
     )
     onConcl
   in
-  let refold  : tactic = 
-    reduce 
+  let refold  : tactic =
+    reduce
       (Rawterm.Fold (List.map mkConst fnames))
     onConcl
       
   in
-  fun  g -> 
+  fun  g ->
 (*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
 (*      then     msgnl (str "reduce_fname"); *)
     tclTHENSEQ
@@ -411,40 +276,40 @@ let reduce_fname fnames : tactic =
       ]
       g
 
-let h_exact ?(with_rew_all=false) c :tactic = 
+let h_exact ?(with_rew_all=false) c :tactic =
   observe_tac "h_exact " (exact_check c )
 	  
 	    
-let finalize_proof rec_pos fixes (hyps:identifier list) = 
+let finalize_proof rec_pos fixes (hyps:identifier list) =
   if Tacinterp.get_debug () <> Tactic_debug.DebugOff
   then
     Pp.msgnl (str "rec hyps are : " ++
 		prlist_with_sep spc Ppconstr.pr_id hyps);
-  let exactify_proof = exactify_proof rec_pos fixes in 
+  let exactify_proof = exactify_proof rec_pos fixes in
  
-  let exactify_proof_with_id id : tactic = 
-    let do_exactify_proof_with_id = 
-      fun g -> 
-	let res  = 
+  let exactify_proof_with_id id : tactic =
+    let do_exactify_proof_with_id =
+      fun g ->
+	let res  =
 	  tclTHEN
 	    (Eauto.e_resolve_constr (mkVar id))
 	    (tclTRY exactify_proof)
 	    
-	in 
+	in
 	tclTHEN
 	  res
 	  ((h_exact (Coqlib.build_coq_I ())))
 	  g
-    in 
-    fun g -> observe_tac "exactify_proof_with_id" do_exactify_proof_with_id g 
+    in
+    fun g -> observe_tac "exactify_proof_with_id" do_exactify_proof_with_id g
   in
-  let apply_one_hyp hyp acc = 
-    tclORELSE 
+  let apply_one_hyp hyp acc =
+    tclORELSE
       ( exactify_proof_with_id hyp)
       acc
   in
-  let apply_one_hyp_with_rewall hyp acc = 
-    tclORELSE 
+  let apply_one_hyp_with_rewall hyp acc =
+    tclORELSE
       (tclTHEN
 	 (rew_all RL)
 	 (exactify_proof_with_id hyp)
@@ -452,19 +317,19 @@ let finalize_proof rec_pos fixes (hyps:identifier list) =
       
       acc
   in
-  let apply_hyps = 
-    tclTRYD( 
-      (List.fold_right 
-	 apply_one_hyp 
+  let apply_hyps =
+    tclTRYD(
+      (List.fold_right
+	 apply_one_hyp
 	 hyps
-	 (List.fold_right 
-	    apply_one_hyp_with_rewall 
-	    hyps 
+	 (List.fold_right
+	    apply_one_hyp_with_rewall
+	    hyps
 	    (tclFAIL 0 (str "No rec hyps found ") )
 	 )
       ))
   in
-  let finalize_proof fnames t  : tactic = 
+  let finalize_proof fnames t  : tactic =
     let change_tac  tac g =
 	match kind_of_term ( pf_concl g) with
 	  | App(p,args) ->
@@ -482,12 +347,12 @@ let finalize_proof rec_pos fixes (hyps:identifier list) =
 	      end
 	  | _ -> assert false
     in
-  fun g -> 
+  fun g ->
 (*     if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
 (*     then  *)
 (*       msgnl (str "finalize with body "++ Printer.pr_lconstr t ++  *)
 (* 	       str " on goal "++ Printer.pr_goal (sig_it g)); *)
-    (change_tac apply_hyps) g 
+    (change_tac apply_hyps) g
   in
   finalize_proof
 
@@ -495,17 +360,18 @@ let do_prove_princ_for_struct
     (rec_pos:int option)  (fnames:constant list)
     (ptes:identifier list) (fixes:identifier Idmap.t) (hyps: identifier list)
       (term:constr) : tactic =
-  let finalize_proof term = 
+  let finalize_proof term =
     finalize_proof rec_pos fixes hyps fnames term
   in
   let rec do_prove_princ_for_struct do_finalize term g =
 (*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
 (*      then msgnl (str "Proving with body : " ++ pr_lconstr_env (pf_env g) term); *)
-    let tac = 
+    let tac =
       fun g ->
 	match kind_of_term term with
 	  | Case(_,_,t,_) ->
-	      case_eq (do_prove_princ_for_struct do_finalize) term t g
+	      observe_tac "case_eq" 
+	      (case_eq (do_prove_princ_for_struct do_finalize) term t) g
 	  | Lambda(n,t,b) ->
 	      begin
 		match kind_of_term( pf_concl g) with
@@ -517,7 +383,7 @@ let do_prove_princ_for_struct
 			   let new_term = pf_nf_betaiota g' (mkApp(term,[|mkVar id|])) in
 			   do_prove_princ_for_struct do_finalize new_term g'
 			) g
-		  | _ ->   
+		  | _ ->
 		      do_finalize term g
 	      end
 	  | Cast(t,_,_) -> do_prove_princ_for_struct do_finalize t g
@@ -529,9 +395,9 @@ let do_prove_princ_for_struct
 		match kind_of_term f with
 		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ ->
 		      do_prove_princ_for_struct_args do_finalize f args g
-		  | Const c when not (List.mem c fnames) -> 	
+		  | Const c when not (List.mem c fnames) ->
 		      do_prove_princ_for_struct_args do_finalize f args g
-		  | Const _ -> 
+		  | Const _ ->
 		      do_finalize  term g
 		  | _ ->
 		      warning "Applied binders not yet implemented";
@@ -540,123 +406,127 @@ let do_prove_princ_for_struct
 	  | Fix _ | CoFix _ ->
 	      error ( "Anonymous local (co)fixpoints are not handled yet")
 	  | Prod _ -> assert false
-	  | LetIn (Name id,v,t,b) -> 
+	  | LetIn (Name id,v,t,b) ->
 	      do_prove_princ_for_struct do_finalize (subst1 v b) g
-	  | LetIn(Anonymous,_,_,b) -> 
+	  | LetIn(Anonymous,_,_,b) ->
 	      do_prove_princ_for_struct do_finalize (pop  b) g
-	  | _ -> 
+	  | _ ->
 	      errorlabstrm "" (str "in do_prove_princ_for_struct found : "(* ++ *)
 (* 				 pr_lconstr_env (pf_env g) term *)
 			      )
 
       in
        tac g
-  and do_prove_princ_for_struct_args do_finalize f_args' args :tactic = 
-    fun g -> 
+  and do_prove_princ_for_struct_args do_finalize 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 tac = 
-	match args with 
-	  | []  -> 
+      let tac =
+	match args with
+	  | []  ->
 	      do_finalize f_args'
-	  | arg::args -> 
-	      let do_finalize new_arg = 
-		tclTRYD 
+	  | arg::args ->
+	      let do_finalize new_arg =
+		tclTRYD
 		  (do_prove_princ_for_struct_args
 		     do_finalize
-		     (mkApp(f_args',[|new_arg|])) 
+		     (mkApp(f_args',[|new_arg|]))
 		     args
 		  )
-	      in 
+	      in
 	      do_prove_princ_for_struct do_finalize arg
-      in 
+      in
       tclTRYD(tac) g
 	
   in
-  do_prove_princ_for_struct 
+  do_prove_princ_for_struct
     (finalize_proof)
     term
 
+let is_pte_type t =
+  isSort (snd (decompose_prod t))
+    
+let is_pte (_,_,t) = is_pte_type t
 
-let prove_princ_for_struct fun_num f_names  nparams : tactic = 
-  let fnames_as_constr = Array.to_list (Array.map mkConst f_names) in 
-  let fbody = 
-    match (Global.lookup_constant f_names.(fun_num)).const_body with 
-      | Some b -> 
-	  let body = force b in 
-	  Tacred.cbv_norm_flags 
-	    (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) 
+let prove_princ_for_struct fun_num f_names  nparams : tactic =
+  let fnames_as_constr = Array.to_list (Array.map mkConst f_names) in
+  let fbody =
+    match (Global.lookup_constant f_names.(fun_num)).const_body with
+      | 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 rec_arg_num,fbody = 
-    match kind_of_term fbody with 
-      | Fix((idxs,fix_num),(_,_,ca)) -> 
+  let rec_arg_num,fbody =
+    match kind_of_term fbody with
+      | Fix((idxs,fix_num),(_,_,ca)) ->
 	  begin Some (idxs.(fix_num) - nparams),substl (List.rev fnames_as_constr) ca.(fix_num) end
       | b -> None,fbody
   in
   let f_real_args = nb_lam fbody - nparams in
-  let test_goal_for_hyps g = 
-    let goal_nb_prod = nb_prod (pf_concl g) in 
-    goal_nb_prod = f_real_args 
+  let test_goal_for_hyps g =
+    let goal_nb_prod = nb_prod (pf_concl g) in
+    goal_nb_prod = f_real_args
   in
-  let test_goal_for_args g = 
-    let goal_nb_prod = nb_prod (pf_concl g) in 
-    goal_nb_prod < 1 
+  let test_goal_for_args g =
+    let goal_nb_prod = nb_prod (pf_concl g) in
+    goal_nb_prod < 1
   in
-  let rec intro_params tac params n : tactic =  
-    if n = 0 
+  let rec intro_params tac params n : tactic =
+    if n = 0
     then tac params
-    else 
+    else
       tclTHEN
 	(intro)
-	(fun g -> 
-	   let (id,_,_) = pf_last_hyp g in 
+	(fun g ->
+	   let (id,_,_) = pf_last_hyp g in
 	   intro_params tac (id::params) (n-1) g
 	)
   in
-  let rec intro_pte tac ptes : tactic = 
-    tclTHEN 
-      intro 
-      (fun g -> 
-	 let (id,_,_) as pte = pf_last_hyp g in 
-	 if is_pte pte 
+  let rec intro_pte tac ptes : tactic =
+    tclTHEN
+      intro
+      (fun g ->
+	 let (id,_,_) as pte = pf_last_hyp g in
+	 if is_pte pte
 	 then intro_pte tac (id::ptes) g
-	 else 
+	 else
 	   tclTHENSEQ
-	     [ generalize [(mkVar id)]; 
+	     [ h_generalize [(mkVar id)];
 	       clear  [id];
 	       tac ptes
 	     ]
 	     g
       )
   in
-  let rec intro_hyps tac hyps : tactic = 
-    fun g -> 
+  let rec intro_hyps tac hyps : tactic =
+    fun g ->
       if test_goal_for_hyps g
       then tac hyps g
-      else 
-	tclTHEN 
-	  intro 
-	  (fun g' -> 
+      else
+	tclTHEN
+	  intro
+	  (fun g' ->
 	     let (id,_,_) = pf_last_hyp g' in
 	     intro_hyps tac (id::hyps) g'
 	  )
 	  g
   in
-  let do_fix ptes tac  : tactic = 
-    match rec_arg_num with 
+  let do_fix ptes tac  : tactic =
+    match rec_arg_num with
       | None -> tac (Idmap.empty)
       | Some fix_arg_num ->
-	  fun g -> 
-	  let this_fix_id = (fresh_id (pf_ids_of_hyps g) "fix___") in 
-	  let ptes_to_fix = 
-	    List.fold_left2 
-	      (fun acc pte fix -> 
+	  fun g ->
+	  let this_fix_id = (fresh_id (pf_ids_of_hyps g) "fix___") in
+	  let ptes_to_fix =
+	    List.fold_left2
+	      (fun acc pte fix ->
 		 Idmap.add pte fix acc
 	      )
 	      Idmap.empty
@@ -665,27 +535,27 @@ let prove_princ_for_struct fun_num f_names  nparams : tactic =
 	  in
 	  tclTHEN
 	    (h_mutual_fix  this_fix_id (fix_arg_num  +1) [])
-	    (tac ptes_to_fix) 
+	    (tac ptes_to_fix)
 	    g
   in
-  let rec intro_args tac args : tactic = 
-    fun g -> 
-      if test_goal_for_args g 
+  let rec intro_args tac args : tactic =
+    fun g ->
+      if test_goal_for_args g
       then tac args g
-      else 
-	tclTHEN 
-	  intro 
-	  (fun g' -> 
+      else
+	tclTHEN
+	  intro
+	  (fun g' ->
 	     let (id,_,_) = pf_last_hyp g' in
 	     intro_args tac (id::args) g'
 	  )
 	  g
   in
-  let intro_tacs tac : tactic = 
-    fun g -> 
+  let intro_tacs tac : tactic =
+    fun g ->
 (*       msgnl (str "introducing params"); *)
       intro_params
-	(fun params -> 
+	(fun params ->
 (* 	   msgnl (str "introducing properties"); *)
 	   intro_pte
 	     (fun ptes ->
@@ -697,7 +567,7 @@ let prove_princ_for_struct fun_num f_names  nparams : tactic =
 		       (fun ptes_to_fix ->
 (* 			  msgnl (str "introducing args"); *)
 			  intro_args
-			    (fun args ->  
+			    (fun args ->
 (* 			       tclTHEN  *)
 (* 				 (reduce_fname (Array.to_list f_names)) *)
 				 (tac params ptes ptes_to_fix hyps args))
@@ -712,32 +582,33 @@ let prove_princ_for_struct fun_num f_names  nparams : tactic =
 	nparams
 	g
   in
-  let apply_fbody g params args  = 
+  let apply_fbody g params args  =
 (*     msgnl (str "applying fbody"); *)
     let args' = List.rev_map mkVar args in
-    let f_args = 
+    let f_args =
       List.fold_left (fun acc p -> (mkVar p)::acc) args' params
-    in 
-    let app_f = applist(subst1 (mkConst f_names.(fun_num)) fbody,f_args) in 
+    in
+    let app_f = applist(subst1 (mkConst f_names.(fun_num)) fbody,f_args) in
 (*     Pp.msgnl (pr_lconstr_env (pf_env g) app_f); *)
     pf_nf_betaiota g app_f
   in
-  let prepare_goal_tac tac : tactic =  
-    intro_tacs 
-      (fun  params ptes ptes_to_fix hyps args g -> 
-	 let app_f = apply_fbody g params args in 
+  let prepare_goal_tac tac : tactic =
+    intro_tacs
+      (fun  params ptes ptes_to_fix hyps args g ->
+	 let app_f = apply_fbody g params args in
 (* 	 msgnl (str "proving"); *)
-	 match rec_arg_num with 
-	     Some rec_arg_num -> 
-	       let actual_args = 
-		 List.fold_left (fun  y x -> x::y) 
+	 match rec_arg_num with
+	     Some rec_arg_num ->
+	       let actual_args =
+		 List.fold_left (fun  y x -> x::y)
 		   (List.rev args)
 		   params
 	       in
-	       let to_replace = applist(mkConst f_names.(fun_num),List.map mkVar actual_args) in 
+	       let to_replace =
+	       applist(mkConst f_names.(fun_num),List.map mkVar actual_args) in
 	       
 	       tclTHENS
-		 (Equality.replace 
+		 (Equality.replace
 		    to_replace
 		    app_f
 		 )
@@ -752,7 +623,7 @@ let prove_princ_for_struct fun_num f_names  nparams : tactic =
 (* 		     Tactics.reflexivity) *)
 		 ]
 		 g
-	   | None -> 
+	   | None ->
 	       tclTHEN
 		 (reduce_fname (Array.to_list f_names))
 		 (tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f)
@@ -761,9 +632,205 @@ let prove_princ_for_struct fun_num f_names  nparams : tactic =
 (* 	 tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f g *)
       )
   in
-  prepare_goal_tac (fun g -> do_prove_princ_for_struct rec_arg_num g) 
+  prepare_goal_tac (fun g -> do_prove_princ_for_struct rec_arg_num g)
+
+
+
+(* let case_eq term : tactic =  *)
+(*   fun g ->  *)
+(*     let type_of_term = pf_type_of g term in  *)
+(*     let eq_proof_term =  *)
+(*       let refl_equal_term = Lazy.force refl_equal in *)
+(*       mkApp(refl_equal_term,[|type_of_t;t|]) *)
+(*     in  *)
+(*     let ba_fun ba =  *)
+(*       tclDO ba.nassums h_intro *)
+(*     in  *)
+(*     tclTHENSEQ  *)
+(*       [ *)
+(* 	h_generalize [eq_proof_term];  *)
+(* 	pattern_option [[-1],term] None; *)
+(* 	case_then_using  Genarg.IntroAnonymous ba_fun term None ([],[]) term *)
+(*       ] *)
+(*       g *)
+    
+
+(* let heq_id = id_of_string "Heq" *)
+
+(* let do_prove_princ_for_struct  *)
+(*     predicates_ids ptes_to_fix branches_ids params_ids args_ids rec_arg_num =  *)
+(*   let rec do_prove_princ_for_struct  eqs_id term =  *)
+(*     match kind_of_term term with  *)
+(*       | Case(_,_,t,_) ->  *)
+(* 	  tclTHEN  *)
+(* 	    (case_eq t) *)
+(* 	    (fun g ->  *)
+(* 	       let heq = fresh_id (pf_ids_of_hyps g) heq in  *)
+(* 	       tclTHEN  *)
+(* 		 (h_intro heq)  *)
+(* 		 (fun g' ->  *)
+(* 		    let new_t_value =  *)
+(* 		      match kind_of_term (pf_type_of g' (mkVar heq)) with  *)
+(* 			| App(_,[|_;_;value|]) -> value  *)
+(* 			| _ -> anomaly "should have been an equality" *)
+(* 		    in *)
+(* 		    let type_of_t = pf_type_of g' t in *)
+(* 		    let term_as_fun =  *)
+(* 		      mkLambda(Anonymous,type_of_t, *)
+(* 			       replace_term term (mkRel 1) term *)
+(* 			      ) *)
+(* 		    in *)
+(* 		    let new_term =  *)
+(* 		      pf_nf_betaiota g' (mkApp(term_as_fun,new_t_value)) *)
+(* 		    in do_prove_princ_for_struct (heq::eqs_id) new_term 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(term,[|mkVar id|]))  *)
+(* 		       in *)
+(* 		       do_prove_princ_for_struct do_finalize eqs_id new_term g' *)
+(* 		    ) *)
+(* 	      | _ -> *)
+(* 		  do_finalize eqs_id term  *)
+(* 	  end *)
+(*       | Cast(t,_,_) -> do_prove_princ_for_struct do_finalize eqs_id t  *)
+(*       | Fix _ | CoFix _ -> *)
+(* 	  error ( "Anonymous local (co)fixpoints are not handled yet") *)
+(*       | LetIn (Name id,v,t,b) -> *)
+(* 	  do_prove_princ_for_struct do_finalize (subst1 v b) g *)
+(*       | LetIn(Anonymous,_,_,b) -> *)
+(* 	  do_prove_princ_for_struct do_finalize (pop  b) g *)
+(*       | Prod _ -> assert false *)
+(*       |  *)
+(*   in  *)
+(*   do_prove_princ_for_struct []  *)
+
+
     
   
+(* let fresh_id_from_name avoid na =  *)
+(*   match get_name avoid na with  *)
+(*     | Name id -> id  *)
+(*     | _ -> assert false  *)
+
+  
+(* let fresh_ids (acces_fun: 'a -> name) (l: 'a list)(avoid : identifier list)  =  *)
+(*   let rev_ids,avoid =  *)
+(*     List.fold_left  *)
+(*       (fun (rev_ids,avoid) e ->  *)
+(* 	 let old_name = acces_fun e in  *)
+(* 	 let new_id = fresh_id_from_name avoid old_name in  *)
+(* 	 new_id::rev_ids,new_id::avoid  *)
+(*       ) *)
+(*       ([],avoid)  *)
+(*       l  *)
+(*   in  *)
+(*   List.rev rev_ids,avoid *)
+		      
+(* let fst' (x,_,_) = x  *)
+
+(* let prove_princ_for_struct fun_num f_names  nparams : tactic =  *)
+(*   fun g ->  *)
+(*       let fnames_as_constr = Array.to_list (Array.map mkConst f_names) in *)
+(*       let fbody = *)
+(* 	match (Global.lookup_constant f_names.(fun_num)).const_body with *)
+(* 	  | 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 rec_arg_num,fbody = *)
+(*     match kind_of_term fbody with *)
+(*       | Fix((idxs,fix_num),(_,_,ca)) -> *)
+(* 	  begin Some (idxs.(fix_num) - nparams),substl (List.rev fnames_as_constr) ca.(fix_num) end *)
+(*       | b -> None,fbody *)
+(*   in *)
+(*   let goal_info = compute_elim_sig (mkRel 0,Rawterm.NoBindings) (pf_concl g) in  *)
+(*   let params_ids,to_avoid = fresh_ids fst' goal_info.Tactics.params [] in  *)
+(*   let predicates_ids,to_avoid = fresh_ids fst' goal_info.predicates to_avoid in  *)
+(*   let branches_ids,to_avoid = fresh_ids fst' goal_info.branches to_avoid in  *)
+(*   let first_intros : tactic =  *)
+(*     tclMAP h_intro (params_ids@predicates_ids@branches_ids)  *)
+(*   in  *)
+(*   let fix_id,to_avoid,fix_tac =  *)
+(*     match rec_arg_num with *)
+(*       | None -> None,to_avoid,first_intros *)
+(*       | Some fix_arg_num -> *)
+(* 	  let this_fix_id = (fresh_id to_avoid "fix___") in *)
+(* 	  Some this_fix_id,this_fix_id::to_avoid, *)
+(* 	  tclTHEN  *)
+(* 	    first_intros  *)
+(* 	    (h_mutual_fix  this_fix_id (fix_arg_num  +1) []) *)
+(*   in *)
+(*   let ptes_to_fix = *)
+(*     List.fold_left2 *)
+(*       (fun acc pte fix -> *)
+(* 	 Idmap.add pte fix acc *)
+(*       ) *)
+(*       Idmap.empty *)
+(*       predicates_ids *)
+(*       [fix_id] *)
+(*   in *)
+(*   let args_ids,to_avoid = fresh_ids fst' goal_info.args to_avoid in  *)
+(*   let (tac_replace,term : tactic*constr) =  *)
+(*     let eqs_rhs =   *)
+(*       let fbody_with_funs =  *)
+(* 	substl (List.rev_map mkConst (Array.to_list f_names)) fbody  *)
+(*       in *)
+(*       applist (fbody_with_funs, (List.map mkVar (params_ids@args_ids))) *)
+(*     in *)
+(*     match rec_arg_num with  *)
+(*       | Some rec_arg_num ->  *)
+(* 	  let eqs_lhs =  *)
+(* 	    applist(mkConst f_names.(fun_num),List.map mkVar args_ids)  *)
+(* 	  in *)
+(* 	  tclTHENS  *)
+(* 	    (Equality.replace eqs_lhs eqs_rhs) *)
+(* 	    [ *)
+(* 	      tclIDTAC (\* The proof continue in this branche *\) *)
+(* 	      ; *)
+(* 	      (\* Not in this one *\) *)
+(* 	      let id = List.nth (List.rev args_ids) (rec_arg_num ) in  *)
+(* 	      tclCOMPLETE *)
+(* 		(tclTHENSEQ *)
+(* 		   [(h_simplest_case (mkVar id)); *)
+(* 		    Tactics.intros_reflexivity *)
+(* 		   ]) *)
+(* 	    ],eqs_rhs *)
+(*       | None ->  *)
+(* 	  unfold_in_concl  *)
+(* 	    (Array.to_list (Array.map (fun x -> [],EvalConstRef x) f_names)),  *)
+(* 	  eqs_rhs  *)
+(*   in *)
+(*   tclTHENSEQ *)
+(*     [ *)
+(*       fix_tac;  *)
+(*       tclMAP h_intro args_ids;  *)
+(*       tac_replace;  *)
+(*       do_prove_princ_for_struct  *)
+(* 	predicates_ids *)
+(* 	ptes_to_fix *)
+(* 	branches_ids *)
+(* 	params_ids *)
+(* 	args_ids *)
+(* 	rec_arg_num *)
+(* 	term *)
+(*     ] *)
+   
+
+
+
 
 
 
@@ -771,6 +838,159 @@ let prove_princ_for_struct fun_num f_names  nparams : tactic =
 
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+      
+exception Toberemoved_with_rel of int*constr
+exception Toberemoved
+  
+let prov_pte_prefix = "_____PTE"
+  
+  
+
+let is_pte_id =
+  let pref_length = String.length prov_pte_prefix in
+  function  id ->
+    String.sub (string_of_id id) 0 pref_length = prov_pte_prefix
+
+let compute_new_princ_type_from_rel  replace
+    (rel_as_kn:mutual_inductive)  =
+  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 i args =
+    mkApp(replace.(i),Array.map pop (array_get_start args))
+  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 env pre_princ : types*(constr list) =
+(*     let _tim1 = Sys.time() in *)
+    let (new_princ_type,_) as res =
+      match kind_of_term pre_princ with
+	| Rel n ->
+	    begin
+	      match Environ.lookup_rel n env with
+		| _,_,t when is_dom t -> raise Toberemoved
+	      | _ -> pre_princ,[]
+	    end
+	| Prod(x,t,b) ->
+	    compute_new_princ_type_for_binder mkProd env x t b
+	| Lambda(x,t,b) ->
+	    compute_new_princ_type_for_binder 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 num args))
+	| App(f,args) ->
+	    let new_args,binders_to_remove =
+	      Array.fold_right (compute_new_princ_type_with_acc env)
+		args
+		([],[])
+	    in
+	    let new_f,binders_to_remove_from_f = compute_new_princ_type env f in
+	    mkApp(new_f,Array.of_list 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 env x v t b
+	| _ -> pre_princ,[]
+    in
+(*     if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(*     then *)
+(*       msgnl (str "compute_new_princ_type for "++ *)
+(* 	       pr_lconstr_env env pre_princ ++ *)
+(* 	       str" is "++ *)
+(* 	       pr_lconstr_env env new_princ_type); *)
+      res
+	
+  and compute_new_princ_type_for_binder bind_fun env x t b =
+    begin
+      try
+	let new_t,binders_to_remove_from_t = compute_new_princ_type 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 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  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  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 env x v t b =
+    begin
+      try
+	let new_t,binders_to_remove_from_t = compute_new_princ_type env t in
+	let new_v,binders_to_remove_from_v = compute_new_princ_type 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 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  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  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 env e (c_acc,to_remove_acc)  =
+	      let new_e,to_remove_from_e = compute_new_princ_type env e
+	      in
+	      new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+  in
+  compute_new_princ_type
+
 let change_property_sort nparam toSort princ princName =
   let params,concl = decompose_prod_n nparam princ in 
   let hyps,_ = decompose_prod concl in
@@ -802,6 +1022,8 @@ let change_property_sort nparam toSort princ princName =
   in 
   res
 
+let prov_pte_prefix = "_____PTE"
+
 let generate_new_structural_principle 
     interactive_proof
     old_princ new_princ_name funs i proof_tac 
diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli
index 18e2af7bc..12325668c 100644
--- a/contrib/funind/new_arg_principle.mli
+++ b/contrib/funind/new_arg_principle.mli
@@ -18,6 +18,6 @@ val generate_new_structural_principle :
 
 
 
-val my_reflexivity : Tacmach.tactic 
+(* val my_reflexivity : Tacmach.tactic  *)
 
 val prove_princ_for_struct : int -> Names.constant array -> int -> Tacmach.tactic
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 79fe16f5a..70c573220 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -210,6 +210,7 @@ let iter = function () -> (constr_of_reference (delayed_force iter_ref))
 let max_constr = function () -> (constr_of_reference (delayed_force max_ref))
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
+let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
 
 (* These are specific to experiments in nat with lt as well_founded_relation, *)
 (*    but this should be made more general. *)
@@ -590,7 +591,7 @@ let tclUSER_if_not_mes is_mes =
     tclCOMPLETE (h_apply (delayed_force well_founded_ltof,Rawterm.NoBindings))
   else tclUSER is_mes None
 
-let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac : tactic = 
+let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac wf_tac : tactic = 
   begin 
     fun g -> 
       let nargs = List.length args_id in
@@ -641,7 +642,7 @@ let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac : ta
 	       )
 	       [ 
 		 (* interactive proof of the well_foundness of the relation *) 
-		 tclUSER_if_not_mes is_mes;
+		 wf_tac is_mes;
 		 (* well_foundness -> Acc for any element *)
 		 observe_tac 
 		   "apply wf_thm" 
@@ -726,19 +727,141 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
 	   )
 	     g 
 	)
+	tclUSER_if_not_mes
 	g 
   end
 
 
+let get_current_subgoals_types () = 
+  let pts =  get_pftreestate () in 
+  let _,subs = extract_open_pftreestate pts in 
+  List.map snd subs 
+
+
+let build_and_l l = 
+  let and_constr =  Coqlib.build_coq_and () in 
+  let conj_constr = coq_conj () in 
+  let mk_and p1 p2 = 
+    Term.mkApp(and_constr,[|p1;p2|]) in 
+  let rec f  = function 
+    | [] -> assert false 
+    | [p] -> p,tclIDTAC,1 
+    | p1::pl -> 
+	let c,tac,nb = f pl in 
+	mk_and p1 c, 
+	tclTHENS
+	  (apply (constr_of_reference conj_constr)) 
+	  [tclIDTAC;
+	   tac
+	  ],nb+1
+  in f l
+
+let build_new_goal_type () = 
+  let sub_gls_types = get_current_subgoals_types () in 
+  let res = build_and_l sub_gls_types in 
+  res
+  
+
+
+let interpretable_as_section_decl d1 d2 = match d1,d2 with
+  | (_,Some _,_), (_,None,_) -> false
+  | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2
+  | (_,None,t1), (_,_,t2) -> eq_constr t1 t2
+
+
+
+
+(* let final_decompose lemma n : tactic =   *)
+(*   fun gls ->  *)
+(*     let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in  *)
+(*     tclTHENSEQ  *)
+(*       [ *)
+(* 	generalize [lemma]; *)
+(* 	tclDO  *)
+(* 	  n  *)
+(* 	  (tclTHENSEQ  *)
+(* 	     [h_intro hid; *)
+(* 	      h_case (mkVar hid,Rawterm.NoBindings);  *)
+(* 	      clear [hid];  *)
+(* 	      intro_patterns [Genarg.IntroWildcard] *)
+(* 	     ] *)
+(* 	  ); *)
+(* 	h_intro hid; *)
+(* 	tclTRY  *)
+(* 	  (tclTHENSEQ [h_case (mkVar hid,Rawterm.NoBindings);  *)
+(* 		       clear [hid];  *)
+(* 		       h_intro hid; *)
+(* 		       intro_patterns [Genarg.IntroWildcard] *)
+(* 		      ]); *)
+(* 	e_resolve_constr (mkVar hid); *)
+(* 	e_assumption *)
+(*       ] *)
+(*       gls *)
+
+
+    
+let prove_with_tcc lemma _ : tactic = 
+  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); 
+	gen_eauto(* default_eauto *) false (false,5) [] (Some [])
+	  (* 	      default_auto *)
+      ]
+      gls
+      
+	     
 
-let com_terminate is_mes fonctional_ref input_type relation rec_arg_num
+let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal)   = 
+  let current_proof_name = get_current_proof_name () in
+  let name = match goal_name with 
+    | Some s -> s 
+    | None   ->  
+	try (add_suffix current_proof_name "_subproof") with _ -> assert false 
+	  
+  in  
+  let sign = Global.named_context () in
+  let sign = clear_proofs sign in
+  let na = next_global_ident_away false name [] in
+  if occur_existential gls_type then
+    Util.error "\"abstract\" cannot handle existentials";
+  (*   let v =     let lemme =  mkConst (Lib.make_con na) in  *)
+(*     Tactics.exact_no_check  *)
+(*       (applist (lemme,  *)
+(* 		List.rev (Array.to_list (Sign.instance_from_named_context sign)))) *)
+(*       gls in  *)
+  
+  let hook _ _ = 
+    let lemma = mkConst (Lib.make_con na) in 
+    Array.iteri (fun i _ -> by (observe_tac "tac" (prove_with_tcc lemma i))) (Array.make nb_goal ());
+    ref := Some lemma ;
+    Command.save_named true;
+  in
+  start_proof
+    na
+    (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) 
+    sign
+    gls_type 
+    hook ;
+  by (decompose_and_tac);
+  ()
+    
+let com_terminate ref is_mes fonctional_ref input_type relation rec_arg_num
     thm_name hook =
   let (evmap, env) = Command.get_current_context() in
   start_proof thm_name
     (Global, Proof Lemma) (Environ.named_context_val env)
     (hyp_terminates fonctional_ref) hook;
   by (observe_tac "whole_start" (whole_start is_mes fonctional_ref
-	input_type relation rec_arg_num ))
+				       input_type relation rec_arg_num ));
+  open_new_goal ref
+     None
+     (build_new_goal_type ())
+  
+
     
 
 let ind_of_ref = function 
@@ -988,7 +1111,7 @@ let (com_eqn : identifier ->
      Command.save_named true);;
 
 
-let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_principle =
+let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_principle : unit =
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_rel (Name f,None,function_type) (Global.env()) in
   let res_vars,eq' = decompose_prod (interp_constr Evd.empty env eq) in 
@@ -1016,6 +1139,7 @@ let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_
       env_with_pre_rec_args
       r
   in 
+  let tcc_lemma_constr = ref None in 
 (*   let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook _ _ =   
     let term_ref = Nametab.locate (make_short_qualid term_id) in
@@ -1023,12 +1147,18 @@ let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_
 (*     let _ = message "start second proof" in *)
     com_eqn equation_id functional_ref f_ref term_ref eq;
     let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
-(*     generate_induction_principle *)
-(*       functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; *)
+    generate_induction_principle tcc_lemma_constr
+      functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
     ()
 
   in
-  com_terminate is_mes functional_ref rec_arg_type relation rec_arg_num term_id  hook 
+  com_terminate 
+    tcc_lemma_constr
+    is_mes functional_ref
+    rec_arg_type
+    relation rec_arg_num
+    term_id
+    hook 
 ;;
 
 
@@ -1038,39 +1168,64 @@ let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_
 let base_leaf_princ eq_cst functional_ref eqs expr = 
   tclTHENSEQ 
     [rewriteLR (mkConst eq_cst);
-     list_rewrite true eqs;
+     tclTRY (list_rewrite true eqs);
      gen_eauto(* default_eauto *) false (false,5) [] (Some [])
     ]
 
 
 
-let finalize_rec_leaf_princ_with is_mes hrec acc_inv br = 
-  tclTHENSEQ [
-    Eauto.e_resolve_constr (mkVar br);
-    tclFIRST
-      [
-	e_assumption;
-	reflexivity;
-	tclTHEN (apply (mkVar hrec))
+let prove_with_tcc 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 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);
+	      gen_eauto(* default_eauto *) false (false,5) [] (Some [])
+       (* 	      default_auto *)
+	    ]
+	    gls
+	    
+	    
+
+let finalize_rec_leaf_princ_with tcc_lemma_constr is_mes hrec acc_inv  eqs br = 
+  fun g -> 
+    tclTHENSEQ [
+      Eauto.e_resolve_constr (mkVar br);
+      tclFIRST
+	[
+	  e_assumption;
+	  reflexivity;
+	  tclTHEN (apply (mkVar hrec))
 	  (tclTHENS
 	     (* (try *) (observe_tac "applying inversion" (apply (Lazy.force acc_inv))) 
 (* 	      with e -> Pp.msgnl (Printer.pr_lconstr (Lazy.force acc_inv));raise e *)
 (* 	     ) *)
 	     [ h_assumption
 	     ;
-	       (fun g ->
-	       tclUSER
-		 is_mes
-		 (Some (hrec::(retrieve_acc_var g)))
-		 g
-	       )
+	      tclTHEN
+		(fun g ->
+		   tclUSER
+		     is_mes
+		     (Some (hrec::(retrieve_acc_var g)))
+		     g
+		)
+		(fun g -> prove_with_tcc tcc_lemma_constr eqs g)
 	     ]
 	  );
+	  gen_eauto(* default_eauto *) false (false,5) [] (Some []);
 	(fun g -> tclIDTAC_MESSAGE (str "here" ++ Printer.pr_goal (sig_it g)) g)
       ]
-  ]
+    ]
+      g
     
 let rec_leaf_princ
+    tcc_lemma_constr
     eq_cst
     branches_names 
     is_mes
@@ -1080,14 +1235,14 @@ let rec_leaf_princ
     eqs
     expr
     = 
-  
+  fun g -> 
   tclTHENSEQ 
     [ rewriteLR (mkConst eq_cst);
       list_rewrite true eqs;
       tclFIRST 
-	(List.map (finalize_rec_leaf_princ_with is_mes hrec acc_inv) branches_names)
+	(List.map (finalize_rec_leaf_princ_with tcc_lemma_constr is_mes hrec acc_inv eqs) branches_names)
     ]
-
+    g
 
 let fresh_id avoid na = 
   let id =  
@@ -1099,7 +1254,7 @@ let fresh_id avoid na =
 
 
 
-let prove_principle is_mes functional_ref 
+let prove_principle tcc_lemma_ref is_mes functional_ref 
     eq_ref rec_arg_num rec_arg_type nb_args relation = 
 (*  f_ref eq_ref rec_arg_num rec_arg_type nb_args relation *)
   let eq_cst =   
@@ -1188,13 +1343,19 @@ let prove_principle is_mes functional_ref
 		      (mkVar f_id)
 		      functional_ref
 		      (base_leaf_princ eq_cst)
-		      (rec_leaf_princ eq_cst branches_names)
+		      (rec_leaf_princ tcc_lemma_ref eq_cst branches_names)
 		      []
 		      expr
 		   )
 		     g 
 		)
-		g )
+		(if is_mes 
+		 then 
+		   tclUSER_if_not_mes 
+		 else fun _ -> prove_with_tcc tcc_lemma_ref [])
+	   
+		g 
+	   )
 	)
     end
       g
@@ -1210,10 +1371,10 @@ VERNAC COMMAND EXTEND RecursiveDefinition
 	| None -> 1
 	| Some n -> n 
     in
-    recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _  _ -> ())]
+    recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _  _ _ -> ())]
 | [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
      "[" ne_constr_list(proof) "]" constr(eq) ] ->
-  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq  (fun  _ _  _ _ _ _ -> ())]
+  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq  (fun  _ _  _ _ _ _ _ -> ())]
 END