Merge commit 'upstream/8.0pl3+8.1beta.2' into 8.1

35 files changed, 3225 insertions, 1210 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index e97df539..2b4b7967 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 8931 2006-06-09 07:43:37Z letouzey $ i*)
+(*i $Id: extraction.ml 9032 2006-07-07 16:30:34Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -406,7 +406,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  List.iter 
 	    (option_iter 
 	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
-	    (lookup_structure ip).s_PROJ 
+	    (lookup_projections ip)
 	with Not_found -> ()
 	end; 
 	Record field_glob
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index f0e986fb..7977d4e0 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -16,10 +16,7 @@ open Indfun_common
 open Libnames
 
 let msgnl = Pp.msgnl
-
-let do_observe () = 
-  Tacinterp.get_debug () <> Tactic_debug.DebugOff  
-
+  
 
 let observe strm =
   if do_observe ()
@@ -173,9 +170,11 @@ let isAppConstruct t =
   then isConstruct (fst (destApp t))
   else false 
 
-
-let nf_betaiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta 
-  
+let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
+  let clos_norm_flags flgs env sigma t =
+    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+  clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
+    
 
 let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
   let nochange msg  = 
@@ -231,12 +230,6 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
 	end_of_type_with_pop
 	sub''
     in
-    (* 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,
@@ -556,10 +549,17 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
       g
 
 
+let my_orelse tac1 tac2 g = 
+  try 
+    tac1 g 
+  with e -> 
+(*     observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *)
+    tac2 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
+    my_orelse
       ( (* we instanciate the hyp if possible  *)
 	fun g -> 
 	  let prov_hid = pf_get_new_id hid g in
@@ -748,10 +748,6 @@ let build_proof
      (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 -> 
@@ -812,7 +808,8 @@ type static_fix_info =
       types : types;
       offset : int;
       nb_realargs : int;
-      body_with_param : constr 
+      body_with_param : constr;
+      num_in_block : int 
     }
 
 
@@ -838,11 +835,12 @@ let prove_rec_hyp fix_info  =
 exception Not_Rec
     
 let generalize_non_dep hyp g = 
+(*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
   let hyps = [hyp] in 
   let env = Global.env () in 
   let hyp_typ = pf_type_of g (mkVar hyp) in 
   let to_revert,_ = 
-    Environ.    fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
+    Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
       if List.mem hyp hyps
 	or List.exists (occur_var_in_decl env hyp) keep
 	or occur_var env hyp hyp_typ
@@ -853,7 +851,7 @@ let generalize_non_dep hyp g =
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN 
-    (observe_tac "h_generalize" (h_generalize (List.map mkVar to_revert)))
+    (observe_tac "h_generalize" (h_generalize  (List.map mkVar to_revert) ))
     (observe_tac "thin" (thin to_revert))
     g
   
@@ -864,47 +862,97 @@ let revert idl =
     (generalize (List.map mkVar idl)) 
     (thin idl)
 
+let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
+(*   observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
+(*   observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
+(*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
+  let f_def = Global.lookup_constant (destConst f) in
+  let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
+  let f_body =
+    force (out_some f_def.const_body)
+  in
+  let params,f_body_with_params = decompose_lam_n nb_params f_body in
+  let (_,num),(_,_,bodies) = destFix f_body_with_params in
+  let fnames_with_params =
+    let params = Array.init nb_params (fun i -> mkRel(nb_params - i)) in
+    let fnames = List.rev (Array.to_list (Array.map (fun f -> mkApp(f,params)) fnames)) in
+    fnames
+  in
+(*   observe (str "fnames_with_params " ++ prlist_with_sep fnl pr_lconstr fnames_with_params); *)
+(*   observe (str "body " ++ pr_lconstr bodies.(num)); *)
+  let f_body_with_params_and_other_fun  = substl fnames_with_params bodies.(num) in
+(*   observe (str "f_body_with_params_and_other_fun " ++  pr_lconstr f_body_with_params_and_other_fun); *)
+  let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
+(*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
+  let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) f_def.const_type in
+  let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
+  let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
+  let f_id = id_of_label (con_label (destConst f)) in
+  let prove_replacement =
+    tclTHENSEQ
+      [
+	tclDO (nb_params + rec_args_num + 1) intro;
+	observe_tac "" (fun g ->
+	   let rec_id = pf_nth_hyp_id g 1 in
+	   tclTHENSEQ
+	     [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
+	      observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings));
+	      intros_reflexivity] g
+	)
+      ]
+  in
+  Command.start_proof
+    (*i The next call to mk_equation_id is valid since we are constructing the lemma
+      Ensures by: obvious
+      i*) 
+    (mk_equation_id f_id)
+    (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+    lemma_type
+    (fun _ _ -> ());
+  Pfedit.by (prove_replacement);
+  Command.save_named false
+
+
 
-let do_replace params rec_arg_num rev_args_id fun_to_replace body = 
-  fun g ->
-    let nb_intro_to_do = nb_prod (pf_concl g) in
+  
+let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
+  let equation_lemma = 
+    try 
+      let finfos = find_Function_infos (destConst f) in 
+      mkConst (out_some finfos.equation_lemma)
+    with (Not_found | Failure "out_some" as e) -> 
+      let f_id = id_of_label (con_label (destConst f)) in 
+      (*i The next call to mk_equation_id is valid since we will construct the lemma
+	Ensures by: obvious
+	i*) 
+      let equation_lemma_id = (mk_equation_id f_id) in 
+      generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+      let _ =
+	match e with 
+	  | Failure "out_some" -> 
+	      let finfos = find_Function_infos (destConst f) in 
+	      update_Function 
+		{finfos with
+		   equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with
+					      ConstRef c -> c
+					    | _ -> Util.anomaly "Not a constant" 
+					 )
+		}
+	  | _ -> () 
+
+      in 
+      Tacinterp.constr_of_id (pf_env g) equation_lemma_id
+  in
+  let nb_intro_to_do = nb_prod (pf_concl g) in
     tclTHEN
       (tclDO nb_intro_to_do intro)
       (
 	fun g' -> 
 	  let just_introduced = nLastHyps nb_intro_to_do g' in 
 	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in 
-	  let old_rev_args_id = rev_args_id in 
-	  let rev_args_id = just_introduced_id@rev_args_id in 
-	  let to_replace = 
-	    Reductionops.nf_betaiota (substl (List.map mkVar rev_args_id) fun_to_replace )
-	  and by = 
-	    Reductionops.nf_betaiota (applist(body,List.rev_map mkVar rev_args_id)) 
-	  in 
-(* 	  observe (str "to_replace := " ++ pr_lconstr_env (pf_env g') to_replace); *)
-(* 	  observe (str "by := " ++ pr_lconstr_env (pf_env g') by); *)
-	  let prove_replacement = 
-	    let rec_id = List.nth (List.rev old_rev_args_id) (rec_arg_num) in 
-	    observe_tac "prove_replacement"
-	      (tclTHENSEQ
-		 [ 
-		   revert just_introduced_id;
-		   keep ((List.map id_of_decl params)@ old_rev_args_id);
-		   generalize_non_dep rec_id;
-		   observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings)); 
-		   intros_reflexivity
-		 ]
-	      )
-	  in
-	  tclTHENS
-	    (observe_tac "replacement" (Equality.replace to_replace by))
-	    [ revert just_introduced_id;
-	     tclSOLVE [prove_replacement]]
-	    g'
+	  tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g'
       )
       g
-    
-
 
 let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
   fun g -> 
@@ -1011,7 +1059,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		     nb_realargs = 
 		       List.length 
 			 (fst (decompose_lam bodies.(i))) - fix_offset;
-		     body_with_param = bodies_with_all_params.(i)
+		     body_with_param = bodies_with_all_params.(i);
+		     num_in_block = i
 		   }
 		)
 		typess
@@ -1027,7 +1076,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		   let app_f = mkApp(f,first_args) in
 		   let pte_args = (Array.to_list first_args)@[app_f] in 
 		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in 
-		   let body_with_param = 
+		   let body_with_param,num = 
 		     let body = get_body fnames.(i) in 
 		     let body_with_full_params = 
 		       Reductionops.nf_betaiota (
@@ -1043,13 +1092,14 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 					    (Array.to_list all_funs_with_full_params)) 
 					 bs.(num),
 				       List.rev_map var_of_decl princ_params))
-				 )
+				 ),num
 			 | _ -> error "Not a mutual block"
 		   in
 		   let info = 
 		     {infos with 
 			types = compose_prod type_args app_pte;
-			 body_with_param = body_with_param
+			 body_with_param = body_with_param;
+			 num_in_block = num
 		     }
 		   in 
 (* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
@@ -1118,8 +1168,17 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 tclTHENSEQ
 		   [
 		     observe_tac "do_replace" 
-		       (do_replace princ_info.params fix_info.idx args_id
-			  (List.hd (List.rev pte_args)) fix_body);
+		       (do_replace 
+			  full_params 
+			  (fix_info.idx + List.length princ_params) 
+			  (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
+			  (all_funs.(fix_info.num_in_block)) 
+			  fix_info.num_in_block 
+			  all_funs
+		       );
+(* 		     observe_tac "do_replace"  *)
+(* 		       (do_replace princ_info.params fix_info.idx args_id *)
+(* 			  (List.hd (List.rev pte_args)) fix_body); *)
 		     let do_prove = 
 		       build_proof 
 			 interactive_proof
@@ -1133,13 +1192,16 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			    nb_rec_hyps = List.length branches
 			 }
 		       in
-		       clean_goal_with_heq
+		       observe_tac "cleaning" (clean_goal_with_heq
 			 (Idmap.map prove_rec_hyp ptes_to_fix) 
 			 do_prove 
-			 dyn_infos
+			 dyn_infos)
 		     in
-(* 		     observe (str "branches := " ++  *)
-(* 				prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches); *)
+(* 		     observe (str "branches := " ++ *)
+(* 				prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++  fnl () ++ *)
+(* 			   str "args := " ++ prlist_with_sep spc Ppconstr.pr_id  args_id *)
+			   
+(* 			   ); *)
 		     observe_tac "instancing" (instanciate_hyps_with_args prove_tac 
 		       (List.rev_map id_of_decl princ_info.branches) 
 		       (List.rev args_id))
diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli
index 35da5d50..62eb528e 100644
--- a/contrib/funind/functional_principles_proofs.mli
+++ b/contrib/funind/functional_principles_proofs.mli
@@ -16,5 +16,4 @@ val prove_principle_for_gen :
   Tacmach.tactic
 
 
-val is_pte  : rel_declaration -> bool 
-val do_observe : unit -> bool 
+(* val is_pte  : rel_declaration -> bool  *)
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 8ef13264..f83eae8d 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -19,9 +19,41 @@ exception Toberemoved_with_rel of int*constr
 exception Toberemoved
 
 
+let pr_elim_scheme el = 
+  let env = Global.env () in 
+  let msg = str "params := " ++ Printer.pr_rel_context env el.params in 
+  let env = Environ.push_rel_context el.params env in 
+  let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in 
+  let env = Environ.push_rel_context el.predicates env in 
+  let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in 
+  let env = Environ.push_rel_context el.branches env in 
+  let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in 
+  let env = Environ.push_rel_context el.args env in 
+  msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
+
 
+let observe s = 
+  if do_observe () 
+  then Pp.msgnl s 
 
 
+let pr_elim_scheme el = 
+  let env = Global.env () in 
+  let msg = str "params := " ++ Printer.pr_rel_context env el.params in 
+  let env = Environ.push_rel_context el.params env in 
+  let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in 
+  let env = Environ.push_rel_context el.predicates env in 
+  let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in 
+  let env = Environ.push_rel_context el.branches env in 
+  let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in 
+  let env = Environ.push_rel_context el.args env in 
+  msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
+
+
+let observe s = 
+  if do_observe () 
+  then Pp.msgnl s 
+
 (* 
    Transform an inductive induction principle into 
    a functional one
@@ -29,6 +61,25 @@ 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 env_with_params = Environ.push_rel_context princ_type_info.params env in
+  let tbl = Hashtbl.create 792 in
+  let rec change_predicates_names (avoid:identifier list) (predicates:Sign.rel_context)  : Sign.rel_context = 
+    match predicates with 
+    | [] -> []
+    |(Name x,v,t)::predicates -> 
+       let id =  Nameops.next_ident_away x avoid in 
+       Hashtbl.add tbl id x;
+       (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
+    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
+  in
+  let avoid = (Termops.ids_of_context env_with_params ) in
+  let princ_type_info = 
+    { princ_type_info with
+	predicates = change_predicates_names avoid princ_type_info.predicates
+    }
+  in 
+(*   observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
+(*   observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
   let change_predicate_sort i (x,_,t) = 
     let new_sort = sorts.(i) in
     let args,_ = decompose_prod t in 
@@ -37,7 +88,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       then List.tl args 
       else args
     in
-    x,None,compose_prod real_args (mkSort new_sort) 
+    Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) 
   in
   let new_predicates = 
     list_map_i
@@ -45,20 +96,21 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       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 env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
   let rel_as_kn = 
     fst (match princ_type_info.indref with
 	   | Some (Libnames.IndRef ind) -> ind 
-	   | _ -> failwith "Not a valid predicate"
+	   | _ -> error "Not a valid predicate"
 	)
   in
+  let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
+  let is_pte = 
+    let set = List.fold_right Idset.add ptes_vars Idset.empty in 
+    fun t -> 
+      match kind_of_term t with 
+	| Var id -> Idset.mem id set 
+	| _ -> false 
+  in
   let pre_princ = 
     it_mkProd_or_LetIn 
       ~init:
@@ -72,6 +124,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       )
       princ_type_info.branches
   in
+  let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
     match kind_of_term c with
       | Ind((u,_)) -> u = rel_as_kn
@@ -108,21 +161,15 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| 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
+	    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 
+	      if is_pte f && remove 
 	      then array_get_start args 
 	      else args 
 	    in
@@ -138,15 +185,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	    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 "++ *)
+(*     let _ = match kind_of_term pre_princ with *)
+(* 	| Prod _ -> *)
+(* 	    observe(str "compute_new_princ_type for "++ *)
 (* 	      pr_lconstr_env env pre_princ ++ *)
 (* 	      str" is "++ *)
-(* 	      pr_lconstr_env env new_princ_type ++ fnl () *)
-(* 	| _ -> str "" *)
-(*     ); *)
+(* 	      pr_lconstr_env env new_princ_type ++ fnl ()) *)
+(* 	| _ -> () in *)
     res
 	
   and compute_new_princ_type_for_binder remove bind_fun env x t b =
@@ -156,25 +201,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	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
+	 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 ->
+(* 	    observe (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
+(* 	    observe (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 =
@@ -184,7 +229,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	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
+	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
@@ -198,24 +243,33 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	
       with
 	| Toberemoved ->
-(* 	    msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (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 "); *)
+(* 	    observe (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
+    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 
+    compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ 
+  in 
+  let pre_res = 
+    replace_vars 
+      (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
+      (lift (List.length ptes_vars) pre_res)
+  in
   it_mkProd_or_LetIn  	 
-    ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates)
+    ~init:(it_mkProd_or_LetIn 
+	     ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) 
+			      new_predicates)
+	  )
     princ_type_info.params
     
   
@@ -246,128 +300,101 @@ let change_property_sort toSort princ princName =
 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 qed () = 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
+
+
+
+
+
+let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* 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 =
+  (*   let time1 = System.get_time ()  in *)
+  let new_principle_type =
     compute_new_princ_type_from_rel
       (Array.map mkConst funs)
-      new_sorts
+      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
+  (*    let time2 = System.get_time ()  in *)
+  (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
+  (*    observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
+  let new_princ_name =
+    next_global_ident_away true (id_of_string "___________princ_________") []
   in
   begin
     Command.start_proof
       new_princ_name
       (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
       new_principle_type
-      hook
+      (hook new_principle_type)
     ;
-    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
+    (*       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; *)
+    get_proof_clean true 
   end
 
 
 
+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
+  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 new_principle_type _ _  =
+    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
+  let (id,(entry,g_kind,hook)) =
+    build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook 
+  in
+  save false new_princ_name entry g_kind hook
+(*   defined  () *)
+
 
 exception Not_Rec
 
@@ -441,30 +468,20 @@ let get_funs_constant mp dp =
     l_const
 
 exception No_graph_found 
-	
-let make_scheme fas = 
+exception Found_type of int 
+
+let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = 
   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,_) -> 
-	 try id_to_constr f     
-	 with Not_found -> 
-	   Util.error ("Cannot find "^ string_of_id 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 funs = List.map fst fas in 
+  let first_fun = List.hd funs in 
+
+
+  let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = 
     try 
-    (* Fixme: take into account funs_mp and funs_dp *)
-    fst (destInd (id_to_constr first_fun_rel_id))
-    with Not_found -> raise No_graph_found
+      fst (find_Function_infos  first_fun).graph_ind 
+    with Not_found -> raise No_graph_found 
   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 
@@ -472,7 +489,7 @@ let make_scheme fas =
   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)
+      (function const -> List.assoc const this_block_funs_indexes)
       funs
   in
   let ind_list = 
@@ -484,49 +501,149 @@ let make_scheme fas =
       )
       funs_indexes
   in
-  let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) 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) -> 
+    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 
+  (* We create the first priciple by tactic *)
+  let first_type,other_princ_types = 
+    match l_schemes with 
+	s::l_schemes -> s,l_schemes
+      | _ -> anomaly ""
   in
-  ()
+  let (_,(const,_,_)) = 
+    build_functional_principle false
+      first_type
+      (Array.of_list sorts)
+      this_block_funs
+      0
+      (prove_princ_for_struct false 0 (Array.of_list funs))
+      (fun _ _ _ -> ())
+  in      
+  incr i;
+  (* The others are just deduced *)
+  if other_princ_types = [] 
+  then
+    [const]
+  else
+    let other_fun_princ_types = 
+      let funs = Array.map mkConst this_block_funs in 
+      let sorts = Array.of_list sorts in 
+      List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
+    in
+    let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in 
+    let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
+    let (idxs,_),(_,ta,_ as decl) = destFix fix in 
+    let other_result = 
+      List.map (* we can now compute the other principles *)
+	(fun scheme_type -> 
+	   incr i;
+	   observe (Printer.pr_lconstr scheme_type);
+	   let type_concl = snd (Sign.decompose_prod_assum scheme_type) in 
+	   let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in 
+	   let f = fst (decompose_app applied_f) in
+	   try (* we search the number of the function in the fix block (name of the function) *)
+	     Array.iteri 
+	     (fun j t -> 
+		let t =  snd (Sign.decompose_prod_assum t) in 
+		let applied_g = List.hd (List.rev (snd (decompose_app t))) in 
+		let g = fst (decompose_app applied_g) in
+		if eq_constr f g
+		then raise (Found_type j); 
+		observe (Printer.pr_lconstr f ++ str " <> " ++
+			   Printer.pr_lconstr g)
+		  
+	     )
+	     ta;
+	   (* If we reach this point, the two principle are not mutually recursive 
+	      We fall back to the previous method 
+	   *)
+	     let (_,(const,_,_)) = 
+	       build_functional_principle
+		 false 
+		 (List.nth other_princ_types (!i - 1))
+		 (Array.of_list sorts)
+		 this_block_funs
+		 !i
+		 (prove_princ_for_struct false !i (Array.of_list funs))
+		 (fun _ _ _ -> ())
+	     in 
+	     const
+	 with Found_type i -> 
+	   let princ_body = 
+	     Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt
+	   in 
+	   {const with 
+	      Entries.const_entry_body = princ_body; 
+	      Entries.const_entry_type = Some scheme_type
+	   }
+      )
+      other_fun_princ_types
+    in
+    const::other_result
+
+let build_scheme fas = 
+(*         (fun (f,_) ->  *)
+(* 	 try Libnames.constr_of_global (Nametab.global f) *)
+(* 	 with Not_found ->  *)
+(* 	   Util.error ("Cannot find "^ Libnames.string_of_reference f) *)
+(*       ) *)
+(*       fas *)
 
-let make_case_scheme fa = 
+  let bodies_types = 
+    make_scheme 
+      (List.map 
+	 (fun (_,f,sort) -> 
+	    let f_as_constant =
+	      try
+		match Nametab.global f with 
+		  | Libnames.ConstRef c -> c 
+		  | _ -> Util.error "Functional Scheme can only be used with functions"
+	      with Not_found ->
+	      	Util.error ("Cannot find "^ Libnames.string_of_reference f)
+	    in
+	    (f_as_constant,sort)
+	 ) 
+	 fas
+      ) 
+  in 
+  List.iter2 
+    (fun (princ_id,_,_) def_entry -> 
+       ignore (Declare.declare_constant 
+		 princ_id 
+		 (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+       Options.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
+    )
+    fas
+    bodies_types
+  
+
+
+let build_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 id_to_constr id =  *)
+(*     Tacinterp.constr_of_id env  id *)
+(*   in  *)
+  let funs =  (fun (_,f,_) ->  
+		 try Libnames.constr_of_global (Nametab.global f)
+		 with Not_found -> 
+		   Util.error ("Cannot find "^ Libnames.string_of_reference 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 funs_mp,funs_dp,_ = Names.repr_con first_fun in
+  let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found 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
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
index 8b4faaf4..cf28c6e6 100644
--- a/contrib/funind/functional_principles_types.mli
+++ b/contrib/funind/functional_principles_types.mli
@@ -1,5 +1,7 @@
 open Names
 open Term
+
+
 val generate_functional_principle : 
   (* do we accept interactive proving *)
   bool ->
@@ -19,13 +21,14 @@ val generate_functional_principle :
   (constr array -> int -> Tacmach.tactic) -> 
   unit
 
-
-
 val compute_new_princ_type_from_rel : constr array -> sorts array -> 
   types -> types
 
 
 exception No_graph_found
 
-val make_scheme : (identifier*identifier*Rawterm.rawsort) list ->  unit
-val make_case_scheme : (identifier*identifier*Rawterm.rawsort)  ->  unit
+val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list
+
+val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list ->  unit
+val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort)  ->  unit
+
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index f6d554a8..dffc8120 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -7,6 +7,124 @@ open Libnames
 open Rawterm
 open Declarations
 
+let is_rec_info scheme_info = 
+  let test_branche min acc (_,_,br) = 
+    acc || (
+      let new_branche = 
+	Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in 
+      let free_rels_in_br = Termops.free_rels new_branche in 
+      let max = min + scheme_info.Tactics.npredicates in 
+      Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
+    )
+  in
+  Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+
+
+let choose_dest_or_ind scheme_info =
+    if is_rec_info scheme_info
+    then Tactics.new_induct
+    else Tactics.new_destruct
+
+
+let functional_induction with_clean c princl pat =
+  let f,args = decompose_app c in 
+  fun g ->      
+    let princ,bindings, princ_type = 
+      match princl with 
+	| None -> (* No principle is given let's find the good one *)
+	    begin
+	      match kind_of_term f with
+		| Const c' ->
+		    let princ_option = 
+		      let finfo = (* we first try to find out a graph on f *)
+			try find_Function_infos c' 
+			with Not_found -> 
+			  errorlabstrm "" (str "Cannot find induction information on "++Printer.pr_lconstr (mkConst c') )
+		      in
+		      match Tacticals.elimination_sort_of_goal g with 
+			| InProp -> finfo.prop_lemma
+			| InSet -> finfo.rec_lemma
+			| InType -> finfo.rect_lemma
+		    in
+		    let princ =  (* then we get the principle *)
+		      try mkConst (out_some princ_option )
+		      with Failure "out_some" -> 
+			(*i If there is not default lemma defined then, we cross our finger and try to 
+		    find a lemma named f_ind (or f_rec, f_rect) i*)
+			let princ_name = 
+			  Indrec.make_elimination_ident
+			    (id_of_label (con_label c'))
+			    (Tacticals.elimination_sort_of_goal g)
+			in
+			try 
+			  mkConst(const_of_id princ_name )
+			with Not_found -> (* This one is neither defined ! *)
+			  errorlabstrm "" (str "Cannot find induction principle for "
+					   ++Printer.pr_lconstr (mkConst c') )
+		    in
+		    (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ)
+		| _ -> raise (UserError("",str "functional induction must be used with a function" ))
+		    
+	    end
+	| Some ((princ,binding)) -> 
+	    princ,binding,Tacmach.pf_type_of g princ
+    in
+    let princ_infos = Tactics.compute_elim_sig princ_type in 
+    let args_as_induction_constr =
+      let c_list = 
+	if princ_infos.Tactics.farg_in_concl 
+	then [c] else [] 
+      in
+      List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) 
+    in 
+    let princ' = Some (princ,bindings) in 
+    let princ_vars = 
+      List.fold_right 
+	(fun a acc -> 
+	  try Idset.add (destVar a) acc
+	  with _ -> acc
+	)
+	args
+	Idset.empty
+    in
+    let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in 
+    let old_idl = Idset.diff old_idl princ_vars in 
+    let subst_and_reduce g = 
+      let idl = 
+	map_succeed 
+	  (fun id -> 
+	    if Idset.mem id old_idl then failwith "subst_and_reduce";
+	    id 
+	  )
+	  (Tacmach.pf_ids_of_hyps g)
+      in 
+      let flag = 
+	Rawterm.Cbv
+	  {Rawterm.all_flags 
+	  with Rawterm.rDelta = false; 		 
+	  }
+      in
+      if with_clean 
+      then
+	Tacticals.tclTHEN
+	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
+	  (Hiddentac.h_reduce flag Tacticals.allClauses)	
+	  g
+      else Tacticals.tclIDTAC g 
+
+    in
+    Tacticals.tclTHEN
+      (choose_dest_or_ind 
+	princ_infos
+	args_as_induction_constr
+	princ'
+	pat)
+      subst_and_reduce
+      g
+
+
+
+
 type annot = 
     Struct of identifier 
   | Wf of Topconstr.constr_expr * identifier option
@@ -120,9 +238,22 @@ let prepare_body (name,annot,args,types,body) rt =
   (fun_args,rt')
 
 
+let derive_inversion fix_names = 
+  try
+    Invfun.derive_correctness 
+      Functional_principles_types.make_scheme
+      functional_induction 
+	  (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
+      (*i The next call to mk_rel_id is valid since we have just construct the graph 
+	Ensures by : register_built
+	i*) 
+      (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names)
+  with e -> 
+    msg_warning (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
+	  
 let generate_principle 
     do_built fix_rec_l recdefs  interactive_proof parametrize 
-    (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic)  =
+    (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit =
   let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
@@ -133,6 +264,9 @@ let generate_principle
     if do_built 
     then
       begin
+	(*i The next call to mk_rel_id is valid since we have just construct the graph 
+	   Ensures by : do_built
+	i*) 
 	let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
 	let ind_kn =
 	  fst (locate_with_msg
@@ -149,7 +283,7 @@ let generate_principle
 	in
 	let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in 
 	let _ = 
-	  Util.list_map_i
+	  list_map_i
 	    (fun i x ->
 	       let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in 
 	       let princ_type = 
@@ -167,6 +301,7 @@ let generate_principle
 	    0
 	    fix_rec_l
 	in 
+	Array.iter add_Function funs_kn;
 	()
       end
   with e -> 
@@ -210,7 +345,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
 	  if List.length names = 1 then 1
 	  else error "Recursive argument must be specified"
       | Some wf_arg -> 
-	  Util.list_index (Name wf_arg) names 
+	  list_index (Name wf_arg) names 
   in
   let unbounded_eq = 
     let f_app_args = 
@@ -236,7 +371,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
 	(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
+      derive_inversion [fname]
     with e -> 
       (* No proof done *) 
       ()
@@ -333,15 +468,15 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 			 (Topconstr.names_of_local_assums args) 
 		     in 
 		     let annot = 
-		       try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec 
+		       try Some (list_index (Name id) names - 1), Topconstr.CStructRec 
 		       with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) 
 		     in 
  		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
 		 | (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,"Function",
+		       user_err_loc
+			 (dummy_loc,"Function",
 			  Pp.str "the recursive argument needs to be specified in Function")
 		     else 
 		       (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
@@ -364,8 +499,8 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	    interactive_proof
 	    true
 	    (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
-	  true
-						 
+	  if register_built then derive_inversion  fix_names;
+	  true;
   in
   ()
 
@@ -397,19 +532,19 @@ let rec add_args id new_args b =
   | CApp(loc,(pf,b),bl) -> 
       CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl)
   | CCases(loc,b_option,cel,cal) -> 
-      CCases(loc,Util.option_map (add_args id new_args) b_option,
-	     List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,Util.option_map (add_args id new_args) b_option)) cel, 
+      CCases(loc,option_map (add_args id new_args) b_option,
+	     List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,option_map (add_args id new_args) b_option)) cel, 
 	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
 	    )
   | CLetTuple(loc,nal,(na,b_option),b1,b2) -> 
-      CLetTuple(loc,nal,(na,Util.option_map (add_args id new_args) b_option),
+      CLetTuple(loc,nal,(na,option_map (add_args id new_args) b_option),
 		add_args id new_args b1,
 		add_args id new_args b2
 	       )
 		
   | CIf(loc,b1,(na,b_option),b2,b3) -> 
       CIf(loc,add_args id new_args b1, 
-	  (na,Util.option_map (add_args id new_args) b_option),
+	  (na,option_map (add_args id new_args) b_option),
 	  add_args id new_args b2,
 	  add_args id new_args b3
 	 )
@@ -426,15 +561,17 @@ let rec add_args id new_args b =
 
 
 
-let make_graph (id:identifier) =
- let c_body = 
-    try
-      let c = const_of_id id  in
-      Global.lookup_constant c 
-    with Not_found -> 
-      raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id) )
-  in
+let make_graph (f_ref:global_reference) =
+ let c,c_body = 
+      match f_ref with 
+	| ConstRef c -> 
+	    begin try c,Global.lookup_constant c 
+	    with Not_found -> 
+	      raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+	    end
+	| _ -> raise (UserError ("", str "Not a function reference") )
 
+  in
   match c_body.const_body with
     | None -> error "Cannot build a graph over an axiom !"
     | Some b ->
@@ -494,7 +631,7 @@ let make_graph (id:identifier) =
 				(fun n (nal,t'') -> 
 				   n+List.length nal) n nal_ta' 
 			    in
-			    assert (n'<= n); 
+(* 			    assert (n'<= n);  *)
 			    chop_n_arrow (n - n') t'
 			| _ -> anomaly "Not enough products"
 		    else t
@@ -511,16 +648,6 @@ let make_graph (id:identifier) =
 		let l = 
 		  List.map
 		    (fun (id,(n,recexp),bl,t,b) -> 
-(* 		       let nal =   *)
-(* 			 List.flatten  *)
-(* 			   (List.map  *)
-(* 			      (function  *)
-(* 				 | Topconstr.LocalRawDef (na,_)-> [] *)
-(* 				 | Topconstr.LocalRawAssum (nal,_) -> nal *)
-(* 			      ) *)
-(* 			      (nal_tas@bl) *)
-(* 			   ) *)
-(* 		       in  *)
 		       let bl' =  
 			 List.flatten 
 			   (List.map 
@@ -539,7 +666,8 @@ let make_graph (id:identifier) =
 			   (List.map 
 			      (function
  				 | Topconstr.LocalRawDef (na,_)-> []
-			      	 | Topconstr.LocalRawAssum (nal,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
+			      	 | Topconstr.LocalRawAssum (nal,_) -> 
+				     List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
 			      )
 			      nal_tas
 			   )
@@ -551,23 +679,17 @@ let make_graph (id:identifier) =
 		in
 		l
 	    | _ ->   
+		let id = id_of_label (con_label c) in 
 		[(id,None,nal_tas,t,b)]
 	in
-(* 	List.iter (fun (id,rec_arg,bl,t,b) ->  *)
-(* 		     Pp.msgnl *)
-(* 		     (Ppconstr.pr_id id ++  *)
-(* 		       Ppconstr.pr_binders bl ++  *)
-(* 		       begin		       match rec_arg with  *)
-(* 			 | Some (Struct id) ->  str " { struct " ++ Ppconstr.pr_id id ++ str " }" *)
-(* 			 | _ -> (mt ()) *)
-(* 		      end ++  *)
-(* 		       str " : " ++ Ppconstr.pr_lconstr_expr t ++  *)
-(* 		       str " := " ++  *)
-(* 		       Ppconstr.pr_lconstr_expr b *)
-(* 		     ) *)
-(* 		  ) *)
-(* 	  expr_list; *)
-	do_generate_principle false false expr_list
+	do_generate_principle false false expr_list;
+	(* We register the infos *)
+	let mp,dp,_ = repr_con c in 
+	List.iter (fun (id,_,_,_,_) -> add_Function (make_con mp dp (label_of_id id))) expr_list
+
+
 (* let make_graph _ = assert false	 *)
 	  
 let do_generate_principle = do_generate_principle true 
+
+
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index b32dfacb..f41aac20 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -5,30 +5,15 @@ open Libnames
 
 let mk_prefix pre id = id_of_string (pre^(string_of_id id))
 let mk_rel_id = mk_prefix "R_"
+let mk_correct_id id = Nameops.add_suffix id "_correct"
+let mk_complete_id id = Nameops.add_suffix id "_complete"
+let mk_equation_id id = Nameops.add_suffix id "_equation"
 
 let msgnl m =
   ()
 
 let invalid_argument s = raise (Invalid_argument s)
 
-(* let idtbl = Hashtbl.create 29 *)
-(* let reset_name () = Hashtbl.clear idtbl *)
-
-(* let fresh_id s = *)
-(*   try *)
-(*     let id = Hashtbl.find idtbl s in *)
-(*     incr id; *)
-(*     id_of_string (s^(string_of_int !id)) *)
-(*   with Not_found -> *)
-(*     Hashtbl.add idtbl s (ref (-1)); *)
-(*     id_of_string s *)
-
-(* let fresh_name s = Name (fresh_id s) *)
-(* let get_name ?(default="H") = function *)
-(*   | Anonymous -> fresh_name default *)
-(*   | Name n -> Name n *)
-
-
 
 let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid
 
@@ -159,161 +144,323 @@ let find_reference sl s =
 let eq = lazy(coq_constant "eq")
 let refl_equal = lazy(coq_constant "refl_equal")
 
+(*****************************************************************)
+(* Copy of the standart save mechanism but without the much too  *)
+(* slow reduction function                                       *) 
+(*****************************************************************)
+open Declarations
+open Entries
+open Decl_kinds
+open Declare
+let definition_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is defined")
+
+
+let save with_clean 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
+    | Local when Lib.sections_are_opened () ->
+        let k = logical_kind_of_goal_kind kind in
+	let c = SectionLocalDef (pft, tpo, opacity) in
+	let _ = declare_variable id (Lib.cwd(), c, k) in
+	(Local, VarRef id)
+    | Local ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
+	(Global, ConstRef kn)
+    | Global ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
+	(Global, ConstRef kn) in
+  if with_clean then  Pfedit.delete_current_proof ();
+  hook l r;
+  definition_message id
+
+
+
+
+let extract_pftreestate pts =
+  let pfterm,subgoals = Refiner.extract_open_pftreestate pts in
+  let tpfsigma = Refiner.evc_of_pftreestate pts in 
+  let exl = Evarutil.non_instantiated tpfsigma  in
+  if subgoals <> [] or exl <> [] then
+    Util.errorlabstrm "extract_proof"
+      (if subgoals <> [] then
+        str "Attempt to save an incomplete proof"
+      else
+        str "Attempt to save a proof with existential variables still non-instantiated");
+  let env = Global.env_of_context (Refiner.proof_of_pftreestate pts).Proof_type.goal.Evd.evar_hyps in
+  env,tpfsigma,pfterm
+
+
+let nf_betaiotazeta =
+  let clos_norm_flags flgs env sigma t =
+    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+  clos_norm_flags Closure.betaiotazeta  
+
+let nf_betaiota =
+  let clos_norm_flags flgs env sigma t =
+    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+  clos_norm_flags Closure.betaiota  
+
+let cook_proof do_reduce =
+  let pfs = Pfedit.get_pftreestate () 
+(*   and ident = Pfedit.get_current_proof_name ()  *)
+  and (ident,strength,concl,hook) = Pfedit.current_proof_statement ()  in
+  let env,sigma,pfterm = extract_pftreestate pfs in
+  let pfterm = 
+    if do_reduce
+    then nf_betaiota env sigma pfterm
+    else pfterm
+  in
+  (ident,
+   ({ const_entry_body = pfterm;
+      const_entry_type = Some concl;
+      const_entry_opaque = false;
+      const_entry_boxed = false},
+    strength, hook))
+
+
+let new_save_named opacity =
+  let id,(const,persistence,hook) = cook_proof true  in
+  let const = { const with const_entry_opaque = opacity } in
+  save true id const persistence hook
+
+let get_proof_clean do_reduce = 
+  let result = cook_proof do_reduce in 
+  Pfedit.delete_current_proof ();
+  result
+
+
+
+
+(**********************)
+
+type function_info = 
+    { 
+      function_constant : constant;
+      graph_ind : inductive;
+      equation_lemma : constant option;
+      correctness_lemma : constant option;
+      completeness_lemma : constant option; 
+      rect_lemma : constant option;
+      rec_lemma : constant option;
+      prop_lemma : constant option;
+    }
+      
+
+type function_db  = function_info list
+
+let function_table = ref ([] : function_db)
+  
 
-(* (\************************************************\)  *)
-(* (\* Should be removed latter                     *\) *)
-(* (\* Comes from new induction  (cf Pierre)        *\) *)
-(* (\************************************************\)  *)
-
-(* open Sign *)
-(* open Term *)
-
-(* type elim_scheme =  *)
-
-(* (\* { (\\* lists are in reverse order! *\\) *\) *)
-(* (\*   params: rel_context;     (\\* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *\\) *\) *)
-(* (\*   predicates: rel_context; (\\* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *\\) *\) *)
-(* (\*   branches: rel_context;    (\\* branchr,...,branch1 *\\) *\) *)
-(* (\*   args: rel_context;       (\\* (xni, Ti_ni) ... (x1, Ti_1) *\\) *\) *)
-(* (\*   indarg: rel_declaration option; (\\* Some (H,I prm1..prmp x1...xni) if present, None otherwise *\\) *\) *)
-(* (\*   concl: types;            (\\* Qi x1...xni HI, some prmis may not be present *\\) *\) *)
-(* (\*   indarg_in_concl:bool;    (\\* true if HI appears at the end of conclusion (dependent scheme) *\\) *\) *)
-(* (\* } *\) *)
-
-
-
-(* let occur_rel n c =  *)
-(*   let res = not (noccurn n c) in *)
-(*   res *)
-
-(* let list_filter_firsts f l = *)
-(*   let rec list_filter_firsts_aux f acc l = *)
-(*     match l with *)
-(*       | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l' *)
-(*       | _ -> acc,l *)
-(*   in *)
-(*   list_filter_firsts_aux f [] l *)
-
-(* let count_rels_from n c = *)
-(*   let rels = Termops.free_rels c in *)
-(*   let cpt,rg = ref 0, ref n in *)
-(*   while Util.Intset.mem !rg rels do *)
-(*     cpt:= !cpt+1; rg:= !rg+1; *)
-(*   done; *)
-(*   !cpt *)
-
-(* let count_nonfree_rels_from n c = *)
-(*   let rels = Termops.free_rels c in *)
-(*   if Util.Intset.exists (fun x -> x >= n) rels then *)
-(*     let cpt,rg = ref 0, ref n in *)
-(*     while not (Util.Intset.mem !rg rels) do *)
-(*       cpt:= !cpt+1; rg:= !rg+1; *)
-(*     done; *)
-(*     !cpt *)
-(*   else raise Not_found *)
-
-(* (\* cuts a list in two parts, first of size n. Size must be greater than n *\) *)
-(* let cut_list n l = *)
-(*   let rec cut_list_aux acc n l = *)
-(*     if n<=0 then acc,l *)
-(*     else match l with *)
-(*       | [] -> assert false *)
-(*       | e::l' -> cut_list_aux (acc@[e]) (n-1) l' in *)
-(*   let res = cut_list_aux [] n l in *)
-(*   res *)
-
-(* let exchange_hd_prod subst_hd t = *)
-(*   let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args) *)
-
-(* let compute_elim_sig elimt  = *)
-(*   (\* conclusion is the final (Qi ...) *\) *)
-(*   let hyps,conclusion = decompose_prod_assum elimt in *)
-(*   (\* ccl is conclusion where Qi (that is rel <something>) is replaced *)
-(*      by a constant (Prop) to avoid it being counted as an arg or *)
-(* parameter in the following. *\) *)
-(*   let ccl = exchange_hd_prod mkProp conclusion in *)
-(*   (\* indarg is the inductive argument if it exists. If it exists it is *)
-(* the last hyp before the conclusion, so it is the first element of *)
-(*      hyps. To know the first elmt is an inductive arg, we check if the *)
-(*      it appears in the conclusion (as rel 1). If yes, then it is not *)
-(*      an inductive arg, otherwise it is. There is a pathological case *)
-(*      with False_inf where Qi is rel 1, so we first get rid of Qi in *)
-(*      ccl. *\) *)
-(*   (\* if last arg of ccl is an application then this a functional ind *)
-(* principle *\) let last_arg_ccl =  *)
-(*     try List.hd (List.rev (snd (decompose_app ccl)))  *)
-(*     with Failure "hd" -> mkProp in (\* dummy constr that is not an app *)
-(* *\) let hyps',indarg,dep =  *)
-(*     if isApp last_arg_ccl  *)
-(*     then  *)
-(*       hyps,None , false (\* no HI at all *\) *)
-(*     else  *)
-(*       try  *)
-(* 	if noccurn 1 ccl (\* rel 1 does not occur in ccl *\) *)
-(* 	then *)
-(* 	  List.tl hyps , Some (List.hd hyps), false (\* it does not *)
-(* occur in concl *\) else *)
-(* 	  List.tl hyps , Some (List.hd hyps) , true (\* it does occur in concl *\)  *)
-(*       with Failure s -> Util.error "cannot recognise an induction schema" *)
-(*   in *)
-
-(*   (\* Arguments [xni...x1] must appear in the conclusion, so we count *)
-(*      successive rels appearing in conclusion **Qi is not considered a *)
-(* rel** *\) let nargs = count_rels_from  *)
-(*     (match indarg with *)
-(*       | None -> 1 *)
-(*       | Some _ -> 2) ccl in *)
-(*   let args,hyps'' = cut_list nargs hyps' in *)
-(*   let rel_is_pred (_,_,c) = isSort (snd(decompose_prod_assum c)) in *)
-(*   let branches,hyps''' =  *)
-(*     list_filter_firsts (function x -> not (rel_is_pred x)) hyps'' *)
-(*   in *)
-(*   (\* Now we want to know which hyps remaining are predicates and which *)
-(*      are parameters *\) *)
-(*   (\* We rebuild  *)
-     
-(*      forall (x1:Ti_1) (xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY *)
-(* x1...xni HI ^^^^^^^^^^^^^^^^^^^^^^^^^                  ^^ *)
-(*                                           optional *)
-(* opt *)
-
-(*      Free rels appearing in this term are parameters. We catch all of *)
-(*      them if HI is present. In this case the number of parameters is *)
-(*      the number of free rels. Otherwise (principle generated by *)
-(*      functional induction or by hand) WE GUESS that all parameters *)
-(*      appear in Ti_js, IS THAT TRUE??. *)
-
-(*      TODO: if we want to generalize to the case where arges are merged *)
-(*      with branches (?) and/or where several predicates are cited in *)
-(*      the conclusion, we should do something more precise than just *)
-(*      counting free rels. *)
-(*  *\) *)
-(*   let concl_with_indarg =  *)
-(*     match indarg with *)
-(*     | None -> ccl *)
-(*     | Some c -> it_mkProd_or_LetIn ccl [c] in *)
-(*   let concl_with_args = it_mkProd_or_LetIn concl_with_indarg args in *)
-(* (\*   let nparams2 = Util.Intset.cardinal (Termops.free_rels concl_with_args) in *\) *)
-(*   let nparams =  *)
-(*     try List.length (hyps'''@branches) - count_nonfree_rels_from 1 *)
-(*       concl_with_args with Not_found -> 0 in *)
-(*   let preds,params = cut_list (List.length hyps''' - nparams) hyps''' in *)
-(*   let elimscheme = { *)
-(*     params = params; *)
-(*     predicates = preds; *)
-(*     branches = branches; *)
-(*     args = args; *)
-(*     indarg = indarg; *)
-(*     concl = conclusion; *)
-(*     indarg_in_concl = dep; *)
-(*   } *)
-(*   in *)
-(*   elimscheme *)
-
-(* let get_params elimt =  *)
-(*   (compute_elim_sig elimt).params *)
-(* (\************************************************\)  *)
-(* (\* end of Should be removed latter              *\) *)
-(* (\* Comes from new induction  (cf Pierre)        *\) *)
-(* (\************************************************\)  *)
+let rec do_cache_info finfo = function 
+  | [] -> raise Not_found 
+  | (finfo'::finfos as l) -> 
+      if finfo' == finfo then l 
+      else if finfo'.function_constant = finfo.function_constant 
+      then finfo::finfos
+      else
+	let res = do_cache_info finfo finfos in 
+	if res == finfos then l else  finfo'::l
+  
 
+let cache_Function (_,(finfos)) = 
+  let new_tbl = 
+    try do_cache_info finfos !function_table
+    with Not_found -> finfos::!function_table
+  in  
+  if new_tbl != !function_table 
+  then function_table := new_tbl
+
+let load_Function _  = cache_Function
+let open_Function _ = cache_Function
+let subst_Function (_,subst,finfos) = 
+  let do_subst_con c = fst (Mod_subst.subst_con subst c)
+  and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
+  in
+  let function_constant' = do_subst_con finfos.function_constant in 
+  let graph_ind' = do_subst_ind finfos.graph_ind in 
+  let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in 
+  let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in 
+  let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in 
+  let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in
+  let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in 
+  let prop_lemma' =  Util.option_smartmap do_subst_con finfos.prop_lemma in 
+  if function_constant' == finfos.function_constant && 
+    graph_ind' == finfos.graph_ind && 
+    equation_lemma' == finfos.equation_lemma &&
+    correctness_lemma' == finfos.correctness_lemma && 
+    completeness_lemma' == finfos.completeness_lemma && 
+    rect_lemma' == finfos.rect_lemma && 
+    rec_lemma' == finfos.rec_lemma && 
+    prop_lemma' == finfos.prop_lemma 
+  then finfos 
+  else
+    { function_constant = function_constant';
+      graph_ind = graph_ind';
+      equation_lemma = equation_lemma' ;
+      correctness_lemma = correctness_lemma' ;
+      completeness_lemma = completeness_lemma' ;
+      rect_lemma = rect_lemma' ;
+      rec_lemma = rec_lemma';
+      prop_lemma = prop_lemma';
+    }
+
+let classify_Function (_,infos) = Libobject.Substitute infos
+
+let export_Function infos = Some infos
+
+
+let discharge_Function (_,finfos) = 
+  let function_constant' = Lib.discharge_con finfos.function_constant
+  and graph_ind' = Lib.discharge_inductive finfos.graph_ind 
+  and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma 
+  and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma 
+  and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma 
+  and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma 
+  and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma
+  and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma
+  in
+  if function_constant' == finfos.function_constant && 
+    graph_ind' == finfos.graph_ind && 
+    equation_lemma' == finfos.equation_lemma &&
+    correctness_lemma' == finfos.correctness_lemma && 
+    completeness_lemma' == finfos.completeness_lemma && 
+    rect_lemma' == finfos.rect_lemma && 
+    rec_lemma' == finfos.rec_lemma && 
+    prop_lemma' == finfos.prop_lemma 
+  then Some finfos 
+  else
+    Some { function_constant = function_constant' ;
+	   graph_ind = graph_ind' ;
+	   equation_lemma = equation_lemma' ;
+	   correctness_lemma = correctness_lemma' ;
+	   completeness_lemma = completeness_lemma';
+	   rect_lemma = rect_lemma';
+	   rec_lemma = rec_lemma';
+	   prop_lemma = prop_lemma' ;
+	 }    
+
+open Term
+let pr_info f_info = 
+  str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+    str "function_constant_type := " ++ 
+    (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
+    str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
+    str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
+    str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
+    str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
+    str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
+    str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
+    str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () 
+
+let pr_table l = 
+  Util.prlist_with_sep fnl pr_info l
+
+let in_Function,out_Function = 
+  Libobject.declare_object
+    {(Libobject.default_object "FUNCTIONS_DB") with 
+       Libobject.cache_function = cache_Function;
+       Libobject.load_function  = load_Function;
+       Libobject.classify_function  = classify_Function;
+       Libobject.subst_function = subst_Function;
+       Libobject.export_function = export_Function;
+       Libobject.discharge_function = discharge_Function
+(*        Libobject.open_function = open_Function; *)
+    }
+
+
+
+(* Synchronisation with reset *)
+let freeze () = 
+  let tbl = !function_table in 
+(*   Pp.msgnl (str "freezing function_table : " ++ pr_table tbl); *)
+  tbl
+
+let unfreeze l = 
+(*   Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
+  function_table :=
+ l
+let init () = 
+(*   Pp.msgnl (str "reseting function_table");  *)
+  function_table := []
+
+let _ = 
+  Summary.declare_summary "functions_db_sum"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false; 
+      Summary.survive_section = false }
+
+let find_or_none id = 
+  try Some 
+    (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
+    ) 
+  with Not_found -> None
+
+
+
+let find_Function_infos f = 
+  List.find (fun finfo ->  finfo.function_constant = f) !function_table
+
+
+let find_Function_of_graph ind = 
+  List.find (fun finfo ->  finfo.graph_ind = ind) !function_table
+  
+let update_Function finfo = 
+(*   Pp.msgnl (pr_info finfo); *)
+  Lib.add_anonymous_leaf (in_Function finfo)
+      
+  
+let add_Function f = 
+  let f_id = id_of_label (con_label f) in 
+  let equation_lemma = find_or_none (mk_equation_id f_id)
+  and correctness_lemma = find_or_none (mk_correct_id f_id) 
+  and completeness_lemma = find_or_none (mk_complete_id f_id) 
+  and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
+  and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
+  and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
+  and graph_ind = 
+    match Nametab.locate (make_short_qualid (mk_rel_id f_id)) 
+    with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
+  in
+  let finfos = 
+    { function_constant = f;
+      equation_lemma = equation_lemma;
+      completeness_lemma = completeness_lemma;
+      correctness_lemma = correctness_lemma;
+      rect_lemma = rect_lemma;
+      rec_lemma = rec_lemma;
+      prop_lemma = prop_lemma;
+      graph_ind = graph_ind
+    }
+  in
+  update_Function finfos
+
+let pr_table () = pr_table !function_table
+(*********************************)
+(* Debuging *)
+let function_debug = ref false 
+open Goptions
+
+let function_debug_sig =
+  {
+    optsync = false;
+    optname = "Function debug";
+    optkey =  PrimaryTable("Function_debug");
+    optread = (fun () -> !function_debug);
+    optwrite = (fun b -> function_debug := b)
+  }
+
+let _ = declare_bool_option function_debug_sig
+
+
+let do_observe () = 
+  !function_debug = true
+      
+      
+    
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index ab5195b0..00e1ce8d 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -1,7 +1,15 @@
 open Names
 open Pp
 
+(* 
+   The mk_?_id function build different name w.r.t. a function 
+   Each of their use is justified in the code 
+*) 
 val mk_rel_id : identifier -> identifier
+val mk_correct_id : identifier -> identifier
+val mk_complete_id : identifier -> identifier
+val mk_equation_id : identifier -> identifier
+
 
 val msgnl : std_ppcmds -> unit
 
@@ -39,3 +47,59 @@ val refl_equal : Term.constr Lazy.t
 val const_of_id: identifier -> constant
 
 
+(* [save_named] is a copy of [Command.save_named] but uses 
+   [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast] 
+   
+
+
+   DON'T USE IT if you cannot ensure that there is no VMcast in the proof
+
+*)
+
+(* val nf_betaiotazeta : Reductionops.reduction_function *)
+
+val new_save_named : bool -> unit 
+
+val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind -> 
+  Tacexpr.declaration_hook -> unit 
+
+(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and 
+   abort the proof 
+*)
+val get_proof_clean : bool ->     
+  Names.identifier *
+    (Entries.definition_entry * Decl_kinds.goal_kind *
+       Tacexpr.declaration_hook)
+    
+
+
+
+(*****************)
+
+type function_info = 
+    { 
+      function_constant : constant;
+      graph_ind : inductive;
+      equation_lemma : constant option;
+      correctness_lemma : constant option;
+      completeness_lemma : constant option;
+      rect_lemma : constant option;
+      rec_lemma : constant option;
+      prop_lemma : constant option;
+    }
+
+val find_Function_infos : constant -> function_info
+val find_Function_of_graph : inductive -> function_info
+(* WARNING: To be used just after the graph definition !!! *)
+val add_Function : constant -> unit
+
+val update_Function : function_info -> unit 
+
+
+(** debugging *) 
+val pr_info : function_info -> Pp.std_ppcmds
+val pr_table : unit -> Pp.std_ppcmds
+
+
+val function_debug : bool ref 
+val do_observe : unit -> bool
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 61f26d30..00b5f28c 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -14,6 +14,7 @@ open Indfun_common
 open Indfun
 open Genarg
 open Pcoq
+open Tacticals
 
 let pr_binding prc = function
   | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
@@ -36,7 +37,8 @@ let pr_with_bindings prc prlc (c,bl) =
 let pr_fun_ind_using  prc prlc _ opt_c = 
   match opt_c with
     | None -> mt ()
-    | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc c)
+    | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b))
+
 
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings_opt
@@ -47,25 +49,9 @@ END
 
 
 TACTIC EXTEND newfuninv
-   [ "functional" "inversion" ident(hyp) ident(fname) fun_ind_using(princl)] -> 
+   [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] -> 
      [
-       fun g -> 
-	 let fconst = const_of_id fname in
-	 let princ = 
-	   match princl with 
-	     | None -> 
-		 let f_ind_id =  
-		   (
-		     Indrec.make_elimination_ident
-		       fname 
-		       (Tacticals.elimination_sort_of_goal g)
-		   )
-	       in
-		 let princ = const_of_id f_ind_id in
-		 princ
-	     | Some princ -> destConst (fst princ)
-	 in       
-	 Invfun.invfun hyp fconst princ g
+       Invfun.invfun hyp fname
      ]
 END
 
@@ -82,26 +68,11 @@ ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat
 END
 
 
-let is_rec scheme_info = 
-  let test_branche min acc (_,_,br) = 
-    acc ||
-      (let new_branche = Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in 
-      let free_rels_in_br = Termops.free_rels new_branche in 
-      let max = min + scheme_info.Tactics.npredicates in 
-      Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br)
-  in
-  Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
-
-
-let choose_dest_or_ind scheme_info =
-    if is_rec scheme_info
-    then Tactics.new_induct
-    else Tactics.new_destruct
 
 
 TACTIC EXTEND newfunind
    ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
-     [
+     [ 
        let pat = 
 	 match pat with 
 	   | None -> IntroAnonymous
@@ -112,77 +83,23 @@ TACTIC EXTEND newfunind
 	 | [c] -> c 
 	 | c::cl -> applist(c,cl)
        in 
-       let f,args = decompose_app c in 
-       fun g -> 
-	 let princ,bindings = 
-	   match princl with 
-	     | None -> (* No principle is given let's find the good one *)
-		 let fname = 
-		   match kind_of_term f with 
-		     | Const c' -> 
-			 id_of_label (con_label c') 
-		     | _ -> Util.error "Must be used with a function" 
-		 in
-		 let princ_name = 
-		   (
-		     Indrec.make_elimination_ident
-		       fname
-		       (Tacticals.elimination_sort_of_goal g)
-		   )
-		 in
-		 mkConst(const_of_id princ_name ),Rawterm.NoBindings
-	     | Some princ -> princ 
-	 in
-	 let princ_type = Tacmach.pf_type_of g princ in 
-	 let princ_infos = Tactics.compute_elim_sig princ_type in 
-	 let args_as_induction_constr =
-	   let c_list = 
-	     if princ_infos.Tactics.farg_in_concl 
-	     then [c] else [] 
-	   in
-	   List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) 
-	 in 
-	 let princ' = Some (princ,bindings) in 
-	 let princ_vars = 
-	   List.fold_right 
-	     (fun a acc -> 
-		try Idset.add (destVar a) acc
-		with _ -> acc
-	     )
-	     args
-	     Idset.empty
-	 in
-	 let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in 
-	 let old_idl = Idset.diff old_idl princ_vars in 
-	 let subst_and_reduce g = 
-	   let idl = 
-	     Util.map_succeed 
-	       (fun id -> 
-		  if Idset.mem id old_idl then failwith "";
-		  id 
-	       )
-	       (Tacmach.pf_ids_of_hyps g)
-	   in 
-	   let flag = 
-	     Rawterm.Cbv
-	       {Rawterm.all_flags 
-		with Rawterm.rDelta = false; 		 
-	       }
-	   in
-	   Tacticals.tclTHEN
-	     (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
-	     (Hiddentac.h_reduce flag Tacticals.allClauses)
-	     g
-	 in
-	 Tacticals.tclTHEN
-	   (choose_dest_or_ind 
-	   princ_infos
-	   args_as_induction_constr
-	   princ'
-	   pat)
-	   subst_and_reduce
-	   g
-     ]
+       functional_induction true c  princl pat ]
+END
+(***** debug only ***)
+TACTIC EXTEND snewfunind
+   ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
+     [ 
+       let pat = 
+	 match pat with 
+	   | None -> IntroAnonymous
+	   | Some pat -> pat
+       in
+       let c = match cl with 
+	 | [] -> assert false
+	 | [c] -> c 
+	 | c::cl -> applist(c,cl)
+       in 
+       functional_induction false c princl pat ]
 END
 
 
@@ -213,7 +130,10 @@ VERNAC ARGUMENT EXTEND rec_definition2
      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 
+	 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,"Function",
@@ -240,12 +160,15 @@ END
 
 VERNAC COMMAND EXTEND Function
    ["Function" rec_definitions2(recsl)] ->
-	[ do_generate_principle false  recsl]
+	[ 
+	  do_generate_principle false  recsl; 
+	  
+	]
 END
 
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
-| [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] 
+| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] 
 END 
 
 VERNAC ARGUMENT EXTEND fun_scheme_args
@@ -257,29 +180,176 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
    ["Functional" "Scheme" fun_scheme_args(fas) ] ->
     [
       try 
-	Functional_principles_types.make_scheme fas
+	Functional_principles_types.build_scheme fas
       with Functional_principles_types.No_graph_found -> 
 	match fas with 
 	  | (_,fun_name,_)::_ -> 
 	      begin
-		make_graph fun_name;
-		try Functional_principles_types.make_scheme fas
+		make_graph (Nametab.global fun_name);
+		try Functional_principles_types.build_scheme fas
 		with Functional_principles_types.No_graph_found -> 
 		  Util.error ("Cannot generate induction principle(s)")
 	      end
 	  | _ -> assert false (* we can only have non empty  list *)
     ]
 END
-
+(***** debug only ***)
 
 VERNAC COMMAND EXTEND NewFunctionalCase
    ["Functional" "Case" fun_scheme_arg(fas) ] ->
     [
-      Functional_principles_types.make_case_scheme fas
+      Functional_principles_types.build_case_scheme fas
     ]
 END
 
-
+(***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph 
-["Generate" "graph" "for" ident(c)] -> [ make_graph c ]
+["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ]
+END
+
+
+
+
+
+(* FINDUCTION *)
+
+(* comment this line to see debug msgs *)
+(* let msg x = () ;; let pr_lconstr c = str "" *)
+  (* uncomment this to see debugging *)
+let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+
+
+
+(** Information about an occurrence of a function call (application)
+    inside a term. *)
+type fapp_info = {
+  fname: constr; (** The function applied *)
+  largs: constr list; (** List of arguments *)
+  free: bool; (** [true] if all arguments are debruijn free *)
+  max_rel: int; (** max debruijn index in the funcall *)
+  onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
+}
+
+
+(** [constr_head_match(a b c) a] returns true, false otherwise. *)
+let constr_head_match u t=
+  if isApp u 
+  then 
+    let uhd,args= destApp u in
+    uhd=t
+  else false
+
+(** [hdMatchSub inu t] returns the list of occurrences of [t] in
+    [inu]. DeBruijn are not pushed, so some of them may be unbound in
+    the result. *)
+let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
+  let subres = 
+    match kind_of_term inu with
+      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> 
+	  hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
+      | Fix (_,(lna,tl,bl))  -> (* not sure Fix is correct *)
+	  Array.fold_left 
+	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) 
+	    [] bl
+      | _ -> (* Cofix will be wrong *)
+	  fold_constr 
+	    (fun l cstr -> 
+	      l @ hdMatchSub cstr test) [] inu in 
+  if not (test inu) then subres
+  else
+    let f,args = decompose_app inu in
+    let freeset = Termops.free_rels inu in
+    let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in
+    {fname = f; largs = args; free = Util.Intset.is_empty freeset;
+    max_rel = max_rel; onlyvars = List.for_all isVar args } 
+    ::subres
+
+
+(** [find_fapp test g] returns the list of [app_info] of all calls to
+    functions that satisfy [test] in the conclusion of goal g. Trivial
+    repetition (not modulo conversion) are deleted. *)
+let find_fapp (test:constr -> bool) g : fapp_info list = 
+  let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
+  let res = 
+    List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in
+  (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
+  res)
+
+
+
+(** [finduction id filter g] tries to apply functional induction on
+    an occurence of function [id] in the conclusion of goal [g]. If
+    [id]=[None] then calls to any function are selected. In any case
+    [heuristic] is used to select the most pertinent occurrence. *)
+let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list)
+    (nexttac:Proof_type.tactic) g =
+  let test = match oid with
+    | Some id -> 
+	let idconstr = mkConst (const_of_id id) in
+	(fun u -> constr_head_match u idconstr) (* select only id *)
+    | None -> (fun u -> isApp u) in (* select calls to any function *)
+  let info_list = find_fapp test g in
+  let ordered_info_list = heuristic info_list in
+  prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); 
+  if List.length ordered_info_list = 0 then Util.error "function not found in goal\n";
+  let taclist: Proof_type.tactic list = 
+    List.map 
+      (fun info -> 
+	(tclTHEN 
+	  (functional_induction true (applist (info.fname, info.largs)) 
+	    None IntroAnonymous) 
+	  nexttac)) ordered_info_list in
+  tclFIRST taclist g
+
+
+
+
+(** [chose_heuristic oi x] returns the heuristic for reordering
+    (and/or forgetting some elts of) a list of occurrences of
+     function calls infos to chose first with functional induction. *)
+let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
+  match oi with
+    | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
+    | None -> 
+	(* Default heuristic: keep only occurrence where all arguments
+	   are *bound* (meaning already introduced) variables *)
+	(* TODO: put other funcalls at the end instead of deleting them *)
+	let ordering x y =
+	  if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
+	  else if x.free && x.onlyvars then -1
+	  else if y.free && y.onlyvars then 1
+	  else 0 (* both not pertinent *)
+	in
+	List.sort ordering
+
+
+TACTIC EXTEND finduction
+    ["finduction" ident(id) natural_opt(oi)] -> 
+      [ 
+	match oi with
+	  | Some(n) when n<=0 -> Util.error "numerical argument must be > 0"
+	  | _ -> 
+	      let heuristic = chose_heuristic oi in
+	      finduction (Some id) heuristic tclIDTAC
+      ]
+END
+
+
+
+TACTIC EXTEND fauto
+    [ "fauto" tactic(tac)] -> 
+      [
+	let heuristic = chose_heuristic None in
+	finduction None heuristic (snd tac)
+      ]
+  |
+    [ "fauto" ] -> 
+      [
+	let heuristic = chose_heuristic None in
+	finduction None heuristic tclIDTAC
+      ]
+
 END
+
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 2e5616f0..084ec7e0 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -1,7 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+open Tacexpr
+open Declarations
 open Util
 open Names
 open Term
-open Tacinvutils
 open Pp
 open Libnames
 open Tacticals
@@ -9,131 +17,963 @@ open Tactics
 open Indfun_common
 open Tacmach
 open Sign
+open Hiddentac
 
+(* Some pretty printing function for debugging purpose *)
 
-let tac_pattern l =
-  (Hiddentac.h_reduce 
-    (Rawterm.Pattern l)
-    Tacticals.onConcl
-  )
+let pr_binding prc  = 
+  function
+    | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
 
+let pr_bindings prc prlc = function
+  | Rawterm.ImplicitBindings l ->
+      brk (1,1) ++ str "with" ++ brk (1,1) ++
+      Util.prlist_with_sep spc prc l
+  | Rawterm.ExplicitBindings l ->
+      brk (1,1) ++ str "with" ++ brk (1,1) ++ 
+        Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+  | Rawterm.NoBindings -> mt ()
 
-let rec nb_prod x =
-  let rec count n c =
-    match kind_of_term c with
-        Prod(_,_,t) -> count (n+1) t
-      | LetIn(_,a,_,t) -> count n (subst1 a t)
-      | Cast(c,_,_) -> count n c
-      | _ -> n
-  in count 0 x
 
-let intro_discr_until n tac : tactic = 
-  let rec intro_discr_until acc : tactic =
-  fun g -> 
-    if nb_prod (pf_concl g) <= n then tac (List.rev acc) g
-    else 
-      tclTHEN 
-	intro 
-	(fun g' ->
-	  let id,_,t = pf_last_hyp g' in
-	  tclORELSE
-	     (tclABSTRACT None (Extratactics.h_discrHyp (Rawterm.NamedHyp id)))
-	    (intro_discr_until ((id,t)::acc))
-	    g'
-	) 
-	g
+let pr_with_bindings prc prlc (c,bl) =
+  prc c ++ hv 0 (pr_bindings prc prlc bl)
+
+
+
+let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds = 
+  pr_with_bindings prc prc  (c,bl)
+
+let pr_elim_scheme el = 
+  let env = Global.env () in 
+  let msg = str "params := " ++ Printer.pr_rel_context env el.params in 
+  let env = Environ.push_rel_context el.params env in 
+  let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in 
+  let env = Environ.push_rel_context el.predicates env in 
+  let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in 
+  let env = Environ.push_rel_context el.branches env in 
+  let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in 
+  let env = Environ.push_rel_context el.args env in 
+  let msg = 
+    Util.option_fold_right
+      (fun o msg -> msg ++ fnl () ++ str "indarg := " ++ Printer.pr_rel_context env [o]) 
+      el.indarg
+      msg
+  in 
+  let env = Util.option_fold_right (fun o env -> Environ.push_rel_context [o] env) el.indarg env in 
+  msg ++ fnl () ++ str "concl := " ++ Printer.pr_lconstr_env env el.concl
+
+(* The local debuging mechanism *)
+let msgnl = Pp.msgnl
+
+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 goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+ let v = tac g in msgnl (goal ++ fnl () ++ 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
+
+(* [nf_zeta] $\zeta$-normalization of a term *)
+let nf_zeta =       
+  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+    Environ.empty_env
+    Evd.empty
+
+
+(* [id_to_constr id] finds the term associated to [id] in the global environment *)
+let id_to_constr id = 
+  try
+    Tacinterp.constr_of_id (Global.env ())  id
+  with Not_found -> 
+    raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id))
+
+(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] 
+   (resp. g_to_f = false) where [graph]  is the graph of [f] and is the [i]th function in the block. 
+
+   [generate_type true f i] returns 
+   \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, 
+   graph\ x_1\ldots x_n\ res \rightarrow res = fv \] decomposed as the context and the conclusion 
+
+   [generate_type false f i] returns 
+   \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, 
+   res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion 
+ *)
+
+let generate_type g_to_f f graph i = 
+  (*i we deduce the number of arguments of the function and its returned type from the graph i*)
+  let graph_arity = Inductive.type_of_inductive (Global.lookup_inductive (destInd graph))  in 
+  let ctxt,_ = decompose_prod_assum graph_arity in 
+  let fun_ctxt,res_type = 
+    match ctxt with 
+      | [] | [_] -> anomaly "Not a valid context"
+      | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
   in
-  intro_discr_until []
-
-
-let rec discr_rew_in_H hypname idl : tactic =
-  match idl with 
-    | [] -> (Extratactics.h_discrHyp (Rawterm.NamedHyp hypname))
-    | ((id,t)::idl') ->
-       match kind_of_term t with 
-	 | App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) -> 
-	     begin 
-	       let constr,_ = decompose_app arg1 in 
-	       if isConstruct constr 
-	       then 
-		 (discr_rew_in_H hypname idl')
-	       else 
-		 tclTHEN 
-		   (tclTRY (Equality.general_rewrite_in true hypname (mkVar id)))
-		   (discr_rew_in_H hypname idl')
-	     end
-	 | _ -> discr_rew_in_H hypname idl'
-
-let finalize fname hypname idl : tactic = 
-  tclTRY (
-    (tclTHEN 
-      (Hiddentac.h_reduce
-	(Rawterm.Unfold [[],EvalConstRef fname])
-	(Tacticals.onHyp hypname)
-      )
-      (discr_rew_in_H hypname idl)
-    ))
+  let nb_args = List.length fun_ctxt in
+  let args_from_decl i decl = 
+    match decl with 
+      | (_,Some _,_) -> incr i; failwith "args_from_decl"
+      | _ -> let j = !i in incr i;mkRel (nb_args - j  + 1) 
+  in
+  (*i We need to name the vars [res] and [fv] i*)
+  let res_id = 
+    Termops.next_global_ident_away 
+      true
+      (id_of_string "res")
+      (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt)
+  in
+  let fv_id = 
+    Termops.next_global_ident_away 
+      true
+      (id_of_string "fv")
+      (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt))
+  in
+  (*i we can then type the argument to be applied to the function [f] i*)
+  let args_as_rels = 
+    let i = ref 0 in
+    Array.of_list ((map_succeed (args_from_decl i) (List.rev fun_ctxt))) 
+  in
+  let args_as_rels = Array.map Termops.pop args_as_rels in
+  (*i
+    the hypothesis [res = fv] can then be computed 
+    We will need to lift it by one in order to use it as a conclusion 
+    i*)
+  let res_eq_f_of_args =
+    mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
+  in 
+  (*i 
+    The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed 
+    We will need to lift it by one in order to use it as a conclusion 
+    i*)  
+  let graph_applied = 
+    let args_and_res_as_rels = 
+      let i = ref 0 in
+      Array.of_list ((map_succeed (args_from_decl i) (List.rev ((Name res_id,None,res_type)::fun_ctxt))) )
+    in
+    let args_and_res_as_rels = 
+      Array.mapi (fun i c -> if i <> Array.length args_and_res_as_rels - 1 then lift 1 c else c) args_and_res_as_rels
+    in
+    mkApp(graph,args_and_res_as_rels) 
+  in 
+  (*i The [pre_context]  is the defined to be the context corresponding to 
+    \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,  \]
+    i*)
+  let pre_ctxt = 
+    (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(mkConst f,args_as_rels)),res_type)::fun_ctxt 
+  in 
+  (*i and we can return the solution depending on which lemma type we are defining i*)
+  if g_to_f 
+  then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args)
+  else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied)
 
-let gen_fargs fargs : tactic = 
-  fun g -> 
-    generalize
-      (List.map
-	 (fun arg -> 
-	    let targ = pf_type_of g arg in
-	    let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
-	    refl_arg
-	 )
-	 (Array.to_list fargs)
-      ) 
-      g 
-      
 
-let invfun (hypname:identifier) fname princ : tactic=
-  fun g -> 
-    let nprod_goal = nb_prod (pf_concl g) in
-    let princ_info = 
-      let princ_type = 
-	(try (match (Global.lookup_constant princ) with
-		  {Declarations.const_type=t} -> t
-	     )
-	 with _ -> assert false)
+(* 
+   [find_induction_principle f] searches and returns the [body] and the [type] of [f_rect]
+   
+   WARNING: while convertible, [type_of body] and [type] can be non equal
+*)
+let find_induction_principle f = 
+  let f_as_constant =  match kind_of_term f with  
+    | Const c' -> c'
+    | _ -> error "Must be used with a function"
+  in
+  let infos = find_Function_infos f_as_constant in 
+  match infos.rect_lemma with 
+    | None -> raise Not_found 
+    | Some rect_lemma -> 
+	let rect_lemma = mkConst rect_lemma in 
+	let typ = Typing.type_of (Global.env ()) Evd.empty rect_lemma in 
+	rect_lemma,typ
+	
+  
+
+(*     let fname =  *)
+(*       match kind_of_term f with  *)
+(* 	| Const c' ->  *)
+(* 	    id_of_label (con_label c')  *)
+(* 	| _ -> error "Must be used with a function"  *)
+(*     in *)
+
+(*     let princ_name =  *)
+(*       ( *)
+(* 	Indrec.make_elimination_ident *)
+(* 	  fname *)
+(* 	  InType *)
+(*       ) *)
+(*     in *)
+(*     let c = (\* mkConst(mk_from_const (destConst f) princ_name ) in  *\) failwith "" in  *)
+(*     c,Typing.type_of (Global.env ()) Evd.empty c *)
+
+
+let rec generate_fresh_id x avoid i = 
+  if i == 0 
+  then [] 
+  else
+    let id = Termops.next_global_ident_away true x avoid in 
+    id::(generate_fresh_id x (id::avoid) (pred i))
+
+
+(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] 
+   is the tactic used to prove correctness lemma. 
+   
+   [functional_induction] is the tactic defined in [indfun] (dependency problem)
+   [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions
+   (resp. graphs of the functions and principles and correctness lemma types) to prove correct. 
+   
+   [i] is the indice of the function to prove correct
+
+   The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is 
+   it looks like~:
+   [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, 
+   res = f x_1\ldots x_n in, \rightarrow graph\ x_1\ldots x_n\ res]
+
+
+   The sketch of the proof is the following one~: 
+   \begin{enumerate}
+   \item intros until $x_n$
+   \item $functional\ induction\ (f.(i)\ x_1\ldots x_n)$ using schemes.(i)
+   \item for each generated branch intro [res] and [hres :res = f x_1\ldots x_n], rewrite [hres] and the 
+   apply the corresponding constructor of the corresponding graph inductive.
+   \end{enumerate}
+   
+*)
+let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic =
+  fun g ->
+    (* first of all we recreate the lemmas types to be used as predicates of the induction principle 
+       that is~:
+       \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun  fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
+    *)
+    let lemmas =
+      Array.map
+	(fun (_,(ctxt,concl)) ->
+	   match ctxt with
+	     | [] | [_] | [_;_] -> anomaly "bad context"
+	     | hres::res::(x,_,t)::ctxt ->
+		 Termops.it_mkLambda_or_LetIn
+		   ~init:(Termops.it_mkProd_or_LetIn ~init:concl [hres;res])
+		   ((x,None,t)::ctxt)
+	)
+	lemmas_types_infos
+    in
+    (* we the get the definition of the graphs block *)
+    let graph_ind = destInd graphs_constr.(i) in
+    let kn = fst graph_ind in 
+    let mib,_ = Global.lookup_inductive graph_ind in 
+    (* and the principle to use in this lemma in $\zeta$ normal form *)
+    let f_principle,princ_type = schemes.(i) in
+    let princ_type =  nf_zeta princ_type in
+    let princ_infos = Tactics.compute_elim_sig princ_type in
+    (* The number of args of the function is then easilly computable *)
+    let nb_fun_args = nb_prod (pf_concl g)  - 2  in
+    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let ids = args_names@(pf_ids_of_hyps g) in
+    (* Since we cannot ensure that the funcitonnal principle is defined in the 
+       environement and due to the bug #1174, we will need to pose the principle
+       using a name 
+    *)
+    let principle_id = Termops.next_global_ident_away true (id_of_string "princ") ids in
+    let ids = principle_id :: ids in
+    (* We get the branches of the principle *)
+    let branches = List.rev princ_infos.branches in
+    (* and built the intro pattern for each of them *)
+    let intro_pats =
+      List.map
+	(fun (_,_,br_type) ->
+	   List.map
+	     (fun id -> Genarg.IntroIdentifier id)
+	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+	)
+	branches
+    in
+    (* before building the full intro pattern for the principle *)
+    let pat = Genarg.IntroOrAndPattern intro_pats in
+    let eq_ind = Coqlib.build_coq_eq () in
+    let eq_construct = mkConstruct((destInd eq_ind),1) in
+    (* The next to referencies will be used to find out which constructor to apply in each branch *)
+    let ind_number = ref 0 
+    and min_constr_number = ref 0 in 
+    (* The tactic to prove the ith branch of the principle *)
+    let prove_branche i g =
+      (* We get the identifiers of this branch *)
+      let this_branche_ids =
+	List.fold_right
+	  (fun pat acc ->
+	     match pat with
+	       | Genarg.IntroIdentifier id -> Idset.add id acc
+	       | _ -> anomaly "Not an identifier"
+	  )
+	  (List.nth intro_pats (pred i))
+	  Idset.empty
       in
-      Tactics.compute_elim_sig princ_type
+      (* and get the real args of the branch by unfolding the defined constant *)
+      let pre_args,pre_tac =
+	List.fold_right
+	  (fun (id,b,t) (pre_args,pre_tac) ->
+	     if Idset.mem id this_branche_ids
+	     then
+	       match b with
+		 | None -> (id::pre_args,pre_tac)
+		 | Some b ->
+		     (pre_args,
+		      tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac
+		     )
+		     
+	     else (pre_args,pre_tac)
+	  )
+	  (pf_hyps g)
+	  ([],tclIDTAC)
+      in
+      (* 
+	 We can then recompute the arguments of the constructor. 
+	 For each [hid] introduced by this branch, if [hid] has type  
+	 $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are
+	 [ fv (hid fv (refl_equal fv)) ]. 
+	 
+	 If [hid] has another type the corresponding argument of the constructor is [hid]
+      *)
+      let constructor_args =
+	List.fold_right
+	  (fun hid acc ->
+	     let type_of_hid = pf_type_of g (mkVar hid) in
+	     match kind_of_term type_of_hid with
+	       | Prod(_,_,t') ->
+		   begin
+		     match kind_of_term t' with
+		       | Prod(_,t'',t''') ->
+			   begin
+			     match kind_of_term t'',kind_of_term t''' with
+			       | App(eq,args), App(graph',_)
+				   when
+				     (eq_constr eq eq_ind) &&
+				       array_exists  (eq_constr graph') graphs_constr ->
+				   ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
+				    ::args.(2)::acc)
+			       | _ -> mkVar hid ::  acc
+			   end
+		       | _ -> mkVar hid :: acc
+		   end
+	       | _ -> mkVar hid :: acc
+	  ) pre_args []
+      in
+      (* in fact we must also add the parameters to the constructor args *)
+      let constructor_args =
+	let params_id = fst (list_chop princ_infos.nparams args_names) in
+	(List.map mkVar params_id)@(List.rev constructor_args)
+      in
+      (* We then get the constructor corresponding to this branch and 
+	 modifies the references has needed i.e. 
+	 if the constructor is the last one of the current inductive then 
+	 add one the number of the inductive to take and add the number of constructor of the previous 
+	 graph to the minimal constructor number 
+      *)
+      let constructor = 
+	let constructor_num = i - !min_constr_number in 
+	let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in 
+	if constructor_num <= length
+	then 
+	  begin 
+	    (kn,!ind_number),constructor_num
+	  end
+	else 
+	  begin
+	    incr ind_number;
+	    min_constr_number := !min_constr_number + length ;
+	    (kn,!ind_number),1
+	  end
+      in
+      (* we can then build the final proof term *)
+      let app_constructor = applist((mkConstruct(constructor)),constructor_args) in
+      (* an apply the tactic *)
+      let res,hres =
+	match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with
+	  | [res;hres] -> res,hres
+	  | _ -> assert false
+      in
+      observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor);
+      (
+	tclTHENSEQ
+	  [
+	    (* unfolding of all the defined variables introduced by this branch *)
+	    observe_tac "unfolding" pre_tac;
+	    (* $zeta$ normalizing of the conclusion *)
+	    h_reduce
+	      (Rawterm.Cbv
+		 { Rawterm.all_flags with
+		     Rawterm.rDelta = false ;
+		     Rawterm.rConst = []
+		 }
+	      )
+	      onConcl;
+	    (* introducing the the result of the graph and the equality hypothesis *)
+	    observe_tac "introducing" (tclMAP h_intro [res;hres]);
+	    (* replacing [res] with its value *)
+	    observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres));
+	    (* Conclusion *)
+	    observe_tac "exact" (h_exact app_constructor)
+	  ]
+      )
+	g
     in
-    let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
-    let do_invert  fargs  appf : tactic = 
-      let frealargs = (snd (array_chop (List.length princ_info.params) fargs))  
+    (* end of branche proof *)
+    let param_names = fst (list_chop princ_infos.nparams args_names) in
+    let params = List.map mkVar param_names in
+    let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
+    (* The bindings of the principle 
+       that is the params of the principle and the different lemma types 
+    *)
+    let bindings =
+      let params_bindings,avoid =
+	List.fold_left2
+	  (fun (bindings,avoid) (x,_,_) p ->
+	     let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+	     (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
+	  )
+	  ([],[])
+	  princ_infos.params
+	  (List.rev params)
       in
-      let pat_args = 
-	(List.map (fun e -> ([Rawterm.ArgArg (-1)],e)) (Array.to_list frealargs)) @ [[],appf] 
+      let lemmas_bindings =
+	List.rev (fst  (List.fold_left2
+	  (fun (bindings,avoid) (x,_,_) p ->
+	     let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+	     (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
+	  ([],avoid)
+	  princ_infos.predicates
+	  (lemmas)))
       in
-      tclTHENSEQ 
-	[
-	  gen_fargs frealargs;
-	  tac_pattern pat_args;
-	  Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
-	  intro_discr_until nprod_goal (finalize fname hypname) 
-	    
+      Rawterm.ExplicitBindings (params_bindings@lemmas_bindings)
+    in
+    tclTHENSEQ
+      [ observe_tac "intro args_names" (tclMAP h_intro args_names);
+	observe_tac "principle" (forward
+	  (Some (h_exact f_principle))
+	  (Genarg.IntroIdentifier principle_id)
+	  princ_type);
+	tclTHEN_i
+	  (observe_tac "functional_induction" (
+	     fun g -> 
+	       observe
+		 (str "princ" ++ pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g))  (mkVar principle_id,bindings));
+	       functional_induction  false (applist(funs_constr.(i),List.map mkVar args_names))
+		 (Some (mkVar principle_id,bindings))
+		 pat g
+	   ))
+	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
+      ]
+      g
+
+(* [generalize_depedent_of x hyp g] 
+   generalize every hypothesis which depends of [x] but [hyp] 
+*)
+let generalize_depedent_of x hyp g = 
+  tclMAP 
+    (function 
+       | (id,None,t) when not (id = hyp) && 
+	   (Termops.occur_var (pf_env g) x t) -> h_generalize [mkVar id]
+       | _ -> tclIDTAC
+    )
+    (pf_hyps g)
+    g
+
+(* [prove_fun_complete funs graphs schemes lemmas_types_infos i] 
+   is the tactic used to prove completness lemma. 
+   
+   [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions
+   (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. 
+   
+   [i] is the indice of the function to prove complete
+
+   The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is 
+   it looks like~:
+   [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, 
+   graph\ x_1\ldots x_n\ res, \rightarrow  res = f x_1\ldots x_n in]
+
+
+   The sketch of the proof is the following one~: 
+   \begin{enumerate}
+   \item intros until $H:graph\ x_1\ldots x_n\ res$
+   \item $elim\ H$ using schemes.(i)
+   \item for each generated branch, intro  the news hyptohesis, for each such hyptohesis [h], if [h] has 
+   type [x=?] with [x] a variable, then subst [x], 
+   if [h] has type [t=?] with [t] not a variable then rewrite [t] in the subterms, else 
+   if [h] is a match then destruct it, else do just introduce it, 
+   after all intros, the conclusion should be a reflexive equality.
+   \end{enumerate}
+   
+*)
+
+
+let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = 
+  fun g ->  
+    (* We compute the types of the different mutually recursive lemmas 
+       in $\zeta$ normal form
+    *)
+    let lemmas = 
+      Array.map 
+	(fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt)) 
+	lemmas_types_infos
+    in
+    (* We get the constant and the principle corresponding to this lemma *)
+    let f = funcs.(i) in
+    let graph_principle = nf_zeta schemes.(i)  in 
+    let princ_type = pf_type_of g graph_principle in 
+    let princ_infos = Tactics.compute_elim_sig princ_type in 
+    (* Then we get the number of argument of the function 
+       and compute a fresh name for each of them
+    *)
+    let nb_fun_args = nb_prod (pf_concl g)  - 2  in 
+    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let ids = args_names@(pf_ids_of_hyps g) in
+    (* and fresh names for res H and the principle (cf bug bug #1174) *)
+    let res,hres,graph_principle_id = 
+      match generate_fresh_id (id_of_string "z") ids 3 with 
+	| [res;hres;graph_principle_id] -> res,hres,graph_principle_id
+	| _ -> assert false 
+    in
+    let ids = res::hres::graph_principle_id::ids in 
+    (* we also compute fresh names for each hyptohesis of each branche of the principle *)
+    let branches = List.rev princ_infos.branches in 
+    let intro_pats = 
+      List.map 
+	(fun (_,_,br_type) -> 
+	   List.map 
+	     (fun id -> id) 
+	     (generate_fresh_id (id_of_string "y") ids (nb_prod br_type))
+	)
+	branches
+    in
+    let eq_ind = Coqlib.build_coq_eq () in 
+    (* We will need to change the function by its body 
+       using [f_equation] if it is recursive (that is the graph is infinite 
+       or unfold if the graph is finite 
+    *)
+    let rewrite_tac j ids : tactic = 
+      let graph_def = graphs.(j) in 
+      if Rtree.is_infinite graph_def.mind_recargs
+      then 
+	let eq_lemma = 
+	  try out_some (find_Function_infos (destConst funcs.(j))).equation_lemma
+	  with Failure "out_some" | Not_found -> anomaly "Cannot find equation lemma"
+	in 
+	tclTHENSEQ[
+	  tclMAP h_intro ids;
+	  Equality.rewriteLR (mkConst eq_lemma);
+	  (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *)
+	  h_reduce 
+	    (Rawterm.Cbv
+	       {Rawterm.all_flags 
+		with Rawterm.rDelta = false; 		 
+	       }) 
+	    onConcl
+	  ;
+	  h_generalize (List.map mkVar ids);
+	  thin ids
 	]
+      else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
+    in
+    (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis 
+       (unfolding, substituting, destructing cases \ldots)
+    *)
+    let rec intros_with_rewrite_aux : tactic = 
+      fun g -> 
+	match kind_of_term (pf_concl g) with 
+	  | Prod(_,t,t') -> 
+	      begin 
+		match kind_of_term t with 
+		  | App(eq,args) when (eq_constr eq eq_ind) -> 
+		      if isVar args.(1)
+		      then 			
+			let id = pf_get_new_id (id_of_string "y") g  in 
+			tclTHENSEQ [ h_intro id;
+				     generalize_depedent_of (destVar args.(1)) id; 
+				     tclTRY (Equality.rewriteLR (mkVar id));
+				     intros_with_rewrite
+				   ] 
+			  g
+		      else
+			begin 
+			  let id = pf_get_new_id (id_of_string "y") g  in 
+			  tclTHENSEQ[
+			    h_intro id;
+			    tclTRY (Equality.rewriteLR (mkVar id));
+			    intros_with_rewrite
+			  ] g
+			end
+		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> 
+		      Tauto.tauto g
+		  | Case(_,_,v,_) -> 
+		      tclTHENSEQ[
+			h_case (v,Rawterm.NoBindings);
+			intros_with_rewrite
+		      ] g
+		  | LetIn _ -> 
+		      tclTHENSEQ[
+			h_reduce 
+			  (Rawterm.Cbv
+			     {Rawterm.all_flags 
+			      with Rawterm.rDelta = false; 		 
+			     }) 
+			  onConcl
+			;
+			intros_with_rewrite
+		      ] g
+		  | _ -> 			
+		      let id = pf_get_new_id (id_of_string "y") g  in 
+		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
+	      end
+	  | LetIn _ -> 
+	      tclTHENSEQ[
+		h_reduce 
+		  (Rawterm.Cbv
+		     {Rawterm.all_flags 
+		      with Rawterm.rDelta = false; 		 
+		     }) 
+		  onConcl
+		;
+		intros_with_rewrite
+	      ] g
+	  | _ -> tclIDTAC g 
+    and intros_with_rewrite g = 
+      observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
+    in
+    (* The proof of each branche itself *)
+    let ind_number = ref 0 in 
+    let min_constr_number = ref 0 in
+    let prove_branche i g = 
+      (* we fist compute the inductive corresponding to the branch *)
+      let this_ind_number = 
+	let constructor_num = i - !min_constr_number in 
+	let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in 
+	if constructor_num <= length
+	then !ind_number
+	else 
+	  begin
+	    incr ind_number;
+	    min_constr_number := !min_constr_number + length;
+	    !ind_number
+	  end
+      in
+      let this_branche_ids = List.nth intro_pats (pred i) in
+      tclTHENSEQ[
+	(* we expand the definition of the function *)
+        observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
+	(* introduce hypothesis with some rewrite *)
+        (intros_with_rewrite);
+	(* The proof is complete *)
+        observe_tac "reflexivity" (reflexivity)
+      ]
+	g
+    in
+    let params_names = fst (list_chop princ_infos.nparams args_names) in
+    let params = List.map mkVar params_names in 
+    tclTHENSEQ 
+      [ tclMAP h_intro (args_names@[res;hres]);
+	observe_tac "h_generalize" 
+	(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
+	h_intro graph_principle_id;
+	observe_tac "" (tclTHEN_i 
+	  (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
+	  (fun i g -> prove_branche i g ))
+      ]
+      g
+
+
+
+
+let do_save () = Command.save_named false
+
+
+(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness 
+   lemmas for each function in [funs] w.r.t. [graphs]
+   
+   [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and 
+   [functional_induction] is Indfun.functional_induction (same pb) 
+*)
+   
+let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = 
+  let funs = Array.of_list funs and graphs = Array.of_list graphs in
+  let funs_constr = Array.map mkConst funs  in
+  try 
+    let graphs_constr = Array.map mkInd graphs in 
+    let lemmas_types_infos = 
+      Util.array_map2_i 
+	(fun i f_constr graph -> 
+	   let const_of_f = destConst f_constr in 
+	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = 
+	     generate_type false const_of_f graph i
+	   in 
+	   let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in 
+	   let type_of_lemma = nf_zeta type_of_lemma in
+	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+	   type_of_lemma,type_info
+	)
+	funs_constr
+	graphs_constr 
+    in
+    let schemes = 
+      (* The functional induction schemes are computed and not saved if there is more that one function 
+	 if the block contains only one function we can safely reuse [f_rect]
+      *)
+      try
+	if Array.length funs_constr <> 1 then raise Not_found;
+	[| find_induction_principle funs_constr.(0) |]
+      with Not_found -> 
+	  Array.of_list 
+	    (List.map 
+	       (fun entry -> 
+		  (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type )
+	       )
+	       (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs))
+	    )
     in
-    match kind_of_term typhyp with
-      | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) -> 
-(* 	  let valf = def_of_const (mkConst fname) in *)
-	  let eq_arg1 , eq_arg2 , good_eq_form , fargs = 
-	    match kind_of_term arg1 , kind_of_term arg2 with
-	      | App(f, args),_ when eq_constr f (mkConst fname) -> 
-		  arg1 , arg2 , tclIDTAC , args
-	      | _,App(f, args) when eq_constr f (mkConst fname) -> 
-		  arg2 , arg1 , symmetry_in hypname , args
-	      | _ , _  -> error "inversion impossible" 
-	  in
-	  tclTHEN
-	    good_eq_form
-	    (do_invert fargs eq_arg1)
-	    g
-      | App(f',fargs) when eq_constr f' (mkConst fname) -> 
-	  do_invert fargs typhyp g
-	  
-
-      | _ -> error "inversion impossible"
+    let proving_tac = 
+      prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos
+    in
+    Array.iteri 
+      (fun i f_as_constant -> 
+	 let f_id = id_of_label (con_label f_as_constant) in
+	 Command.start_proof 
+	   (*i The next call to mk_correct_id is valid since we are constructing the lemma
+	     Ensures by: obvious
+	     i*) 
+	   (mk_correct_id f_id)
+	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+	   (fst lemmas_types_infos.(i))
+	   (fun _ _ -> ());
+	 Pfedit.by (observe_tac ("procve correctness ("^(string_of_id f_id)^")") (proving_tac i));
+	 do_save ();
+	 let finfo = find_Function_infos f_as_constant in 
+	 update_Function
+	   {finfo with 
+	      correctness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_correct_id f_id)))
+	   }
+
+      )
+      funs;
+    let lemmas_types_infos = 
+      Util.array_map2_i 
+	(fun i f_constr graph -> 
+	   let const_of_f = destConst f_constr in 
+	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = 
+	     generate_type true  const_of_f graph i
+	   in 
+	   let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in 
+	   let type_of_lemma = nf_zeta type_of_lemma in
+	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+	   type_of_lemma,type_info
+	)
+	funs_constr
+	graphs_constr 
+    in
+    let kn,_ as graph_ind  = destInd graphs_constr.(0) in 
+    let  mib,mip = Global.lookup_inductive graph_ind in
+    let schemes = 
+      Array.of_list 
+	(Indrec.build_mutual_indrec (Global.env ()) Evd.empty
+	   (Array.to_list 
+	      (Array.mapi
+		 (fun i mip -> (kn,i),mib,mip,true,InType)
+		 mib.Declarations.mind_packets
+	      )
+	   )
+	)
+    in
+    let proving_tac = 
+      prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos
+    in
+    Array.iteri 
+      (fun i f_as_constant -> 
+	 let f_id = id_of_label (con_label f_as_constant) in
+	 Command.start_proof 
+	   (*i The next call to mk_complete_id is valid since we are constructing the lemma
+	     Ensures by: obvious
+	     i*) 
+	   (mk_complete_id f_id)
+	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+	   (fst lemmas_types_infos.(i))
+	   (fun _ _ -> ());
+	 Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i));
+	 do_save ();
+	 let finfo = find_Function_infos f_as_constant in 
+	 update_Function
+	   {finfo with 
+	      completeness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_complete_id f_id)))
+	   }
+      )
+      funs;
+  with e ->
+    (* In case of problem, we reset all the lemmas *)
+    (*i The next call to mk_correct_id is valid since we are erasing the lemmas
+      Ensures by: obvious
+      i*) 
+    let first_lemma_id = 
+      let f_id = id_of_label (con_label funs.(0)) in 
+      
+      mk_correct_id f_id 
+    in
+     ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ());
+    raise e
+	   
+		   
+
+
+
+(***********************************************)
+
+(* [revert_graph kn post_tac hid] transforme an hypothesis [hid] having type Ind(kn,num) t1 ... tn res
+   when [kn] denotes a graph block  into
+   f_num t1... tn = res (by applying [f_complete] to the first type) before apply post_tac on the result 
+   
+   if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
+*)
+let revert_graph kn post_tac hid g =
+    let typ = pf_type_of g (mkVar hid) in 
+    match kind_of_term typ with 
+      | App(i,args) when isInd i -> 
+	  let ((kn',num) as ind') = destInd i in 
+	  if kn = kn' 
+	  then (* We have generated a graph hypothesis so that we must change it if we can *)
+	    let info = 
+	      try find_Function_of_graph ind'
+	      with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+		anomaly "Cannot retrieve infos about a mutual block"
+	    in 
+	    (* if we can find a completeness lemma for this function 
+	       then we can come back to the functional form. If not, we do nothing 
+	    *)
+	    match info.completeness_lemma with 
+	      | None -> tclIDTAC g
+	      | Some f_complete -> 
+		  let f_args,res = array_chop (Array.length args - 1) args in
+		  tclTHENSEQ
+		    [
+		      h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])];
+		      thin [hid];
+		      h_intro hid; 
+		      post_tac hid
+		    ]
+		    g
+		    
+	  else tclIDTAC g
+      | _ -> tclIDTAC g
+
+
+(* 
+   [functional_inversion hid fconst f_correct ] is the functional version of [inversion]
+   
+   [hid] is the hypothesis to invert, [fconst] is the function to invert and  [f_correct]
+   is the correctness lemma for [fconst].
+
+   The sketch is the follwing~: 
+   \begin{enumerate} 
+   \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ 
+   (fails if it is not possible)
+   \item replace [hid] with $R\_f t_1 \ldots t_n res$ using [f_correct]
+   \item apply [inversion] on [hid]
+   \item finally in each branch, replace each  hypothesis [R\_f ..]  by [f ...] using [f_complete] (whenever 
+   such a lemma exists)
+   \end{enumerate}
+*)
+     
+let functional_inversion kn hid fconst f_correct : tactic = 
+  fun g -> 
+    let old_ids = List.fold_right Idset.add  (pf_ids_of_hyps g) Idset.empty in 
+    let type_of_h = pf_type_of g (mkVar hid) in 
+    match kind_of_term type_of_h with 
+      | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ())  -> 
+	  let pre_tac,f_args,res = 
+	    match kind_of_term args.(1),kind_of_term args.(2) with 
+	      | App(f,f_args),_ when eq_constr f fconst -> 
+		  ((fun hid -> h_symmetry (onHyp hid)),f_args,args.(2))
+	      |_,App(f,f_args) when eq_constr f fconst -> 
+		 ((fun hid -> tclIDTAC),f_args,args.(1)) 
+	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
+	  in 
+	  tclTHENSEQ[
+	    pre_tac hid;
+	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
+	    thin [hid];
+	    h_intro hid;
+	    Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid);
+	    (fun g ->
+	       let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in 
+	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
+	    );
+	  ] g
+      | _ -> tclFAIL 1 (mt ()) g
+
+
+
+let invfun qhyp f  =  
+  let f = 
+    match f with 
+      | ConstRef f -> f 
+      | _ -> raise (Util.UserError("",str "Not a function"))
+  in
+  try 
+    let finfos = find_Function_infos f in 
+    let f_correct = mkConst(out_some finfos.correctness_lemma) 
+    and kn = fst finfos.graph_ind
+    in
+    Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp 
+  with 
+    | Not_found ->  error "No graph found" 
+    | Failure "out_some"  -> error "Cannot use equivalence with graph!"
+
 
+let invfun qhyp f g = 
+  match f with 
+    | Some f -> invfun qhyp f g
+    | None -> 
+	Tactics.try_intros_until 
+	  (fun hid g -> 
+	     let hyp_typ = pf_type_of g (mkVar hid)  in 
+	     match kind_of_term hyp_typ with 
+	       | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> 
+		   begin
+		     let f1,_ = decompose_app args.(1) in 
+		     try 
+		       if not (isConst f1) then failwith "";
+		       let finfos = find_Function_infos (destConst f1) in 
+		       let f_correct = mkConst(out_some finfos.correctness_lemma) 
+		       and kn = fst finfos.graph_ind
+		       in
+		       functional_inversion kn hid f1 f_correct g
+		     with | Failure "" | Failure "out_some" | Not_found -> 
+		       try 
+			 let f2,_ = decompose_app args.(2) in 
+			 if not (isConst f2) then failwith "";
+			 let finfos = find_Function_infos (destConst f2) in 
+			 let f_correct = mkConst(out_some finfos.correctness_lemma) 
+			 and kn = fst finfos.graph_ind
+			 in
+			 functional_inversion kn hid  f2 f_correct g
+		       with
+			 | Failure "" -> 
+			     errorlabstrm "" (Ppconstr.pr_id hid ++ str " must contain at leat one function")
+			 | Failure "out_some"  ->  
+			     error "Cannot use equivalence with graph for any side of equality"
+			 | Not_found -> error "No graph found for any side of equality" 
+		   end
+	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
+	  )
+	  qhyp
+	  g
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index b6f26dfd..dbf2f944 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -9,11 +9,11 @@ open Util
 open Rawtermops
 
 let observe strm =  
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  && false 
+  if do_observe ()
   then Pp.msgnl strm 
   else ()
 let observennl strm =  
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  &&false 
+  if do_observe ()
   then Pp.msg strm 
   else ()
 
@@ -44,12 +44,8 @@ let compose_raw_context =
 (* 
    The main part deals with building a list of raw constructor expressions
    from the rhs of a fixpoint equation. 
-   
-   
 *)
 
-
-
 type 'a build_entry_pre_return = 
     {
       context : raw_context;  (* the binding context of the result *)
@@ -62,7 +58,6 @@ type 'a build_entry_return =
       to_avoid : identifier list
     }
 
-
 (*
   [combine_results combine_fun res1 res2] combine two results [res1] and [res2] 
   w.r.t. [combine_fun].
@@ -113,8 +108,6 @@ let combine_args arg args =
 let ids_of_binder =  function 
   | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
   | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> [id]
-(*   | LetTuple(nal,_) ->  *)
-(*       map_succeed (function Name id -> id | _ -> failwith "ids_of_binder") nal *)
 
 let rec change_vars_in_binder mapping = function 
     [] -> []
@@ -216,7 +209,6 @@ let combine_app f args =
     (* Note that the binding context of [args] MUST be placed before the one of 
        the applied value in order to preserve possible type dependencies 
     *)
-
       context = args.context@new_ctxt;
       value = new_value;
   }
@@ -245,10 +237,9 @@ let mk_result ctxt value avoid =
 	;
     to_avoid = avoid
   }
-
-
-let make_discr_match_el  = 
-  List.map (fun e -> (e,(Anonymous,None)))
+(*************************************************
+  Some functions to deal with overlapping patterns 
+**************************************************)
 
 let coq_True_ref = 
   lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "True")
@@ -256,6 +247,25 @@ let coq_True_ref =
 let coq_False_ref = 
   lazy  (Coqlib.gen_reference "" ["Init";"Logic"] "False")
 
+(*
+  [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
+  (the list of expresions on which we will do the matching)
+ *) 
+let make_discr_match_el  = 
+  List.map (fun e -> (e,(Anonymous,None)))
+
+(*
+  [make_discr_match_brl i \[pat_1,...,pat_n\]]  constructs a discrimination pattern matching on the ith expression. 
+  that is. 
+  match ?????? with \\
+  | pat_1 => False  \\
+  | pat_{i-1} => False \\
+  | pat_i => True \\
+  | pat_{i+1} => False \\
+  \vdots 
+  | pat_n => False
+  end
+*)
 let make_discr_match_brl i = 
   list_map_i 
     (fun j (_,idl,patl,_) -> 
@@ -264,84 +274,28 @@ let make_discr_match_brl i =
        else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref))
     )
     0 
-    
+(* 
+   [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff 
+   brl_{i} is the first branch matched by [el] 
+
+   Used when we want to simulate the coq pattern matching algorithm
+*)
 let make_discr_match brl = 
   fun el i -> 
   mkRCases(None,
 	   make_discr_match_el el,
 	   make_discr_match_brl i brl)
-  
-
-
-let rec make_pattern_eq_precond id e pat : identifier * (binder_type * Rawterm.rawconstr) list = 
-  match pat with 
-    | PatVar(_,Anonymous) -> assert false 
-    | PatVar(_,Name x) -> 
-	id,[Prod (Name x),mkRHole ();Prod Anonymous,raw_make_eq (mkRVar x) e]
-    | PatCstr(_,constr,patternl,_) -> 
-	let new_id,new_patternl,patternl_eq_precond = 
-	  List.fold_right 
-	    (fun pat' (id,new_patternl,preconds) -> 
-	       match pat' with 
-		 | PatVar (_,Name id) -> (id,id::new_patternl,preconds)
-		 | _ -> 
-		     let new_id = Nameops.lift_ident id in 
-		     let new_id',pat'_precond = 
-		       make_pattern_eq_precond new_id (mkRVar id) pat' 
-		     in
-		     (new_id',id::new_patternl,preconds@pat'_precond)
-	    )
-	    patternl
-	    (id,[],[])
-	in
-	let cst_narg = 
-	  Inductiveops.mis_constructor_nargs_env
-	    (Global.env ())
-	    constr
-	in
-	let implicit_args =  
-	  Array.to_list 
-	    (Array.init 
-	       (cst_narg - List.length patternl)
-	       (fun _ -> mkRHole ())
-	    )
-	in
-	let cst_as_term =      
-	  mkRApp(mkRRef(Libnames.ConstructRef constr),
-		 implicit_args@(List.map mkRVar new_patternl)
-		)
-	in
-	let precond' = 
-	  (Prod Anonymous, raw_make_eq cst_as_term  e)::patternl_eq_precond 
-	in
-	let precond'' = 
-	  List.fold_right 
-	    (fun id acc ->
-	       (Prod (Name id),(mkRHole ()))::acc
-	    )
-	    new_patternl
-	    precond'
-	in
-	new_id,precond''
 
 let pr_name = function
   | Name id -> Ppconstr.pr_id id
   | Anonymous -> str "_"
 
-let make_pattern_eq_precond id e pat = 
-  let res = make_pattern_eq_precond id e pat in 
-  observe 
-    (prlist_with_sep spc  
-       (function (Prod na,t) -> 
-	  str "forall " ++ pr_name na ++ str ":" ++ pr_rawconstr t
-	| _ -> assert false
-       )
-       (snd res)
-    );
-  res
-
+(**********************************************************************)
+(*  functions used to build case expression from lettuple and if ones *)
+(**********************************************************************)		
 
-let build_constructors_of_type msg ind' argl = 
+(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)	  
+let build_constructors_of_type ind' argl = 
   let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
   let npar = mib.Declarations.mind_nparams in
   Array.mapi (fun i _ ->
@@ -366,21 +320,11 @@ let build_constructors_of_type msg ind' argl =
 		let pat_as_term = 
 		  mkRApp(mkRRef (ConstructRef(ind',i+1)),argl)
 		in
-(* 		Pp.msgnl (str "new constructor := " ++ Printer.pr_rawconstr pat_as_term); *)
 		cases_pattern_of_rawconstr Anonymous pat_as_term
 	     )
     ind.Declarations.mind_consnames
 
-let find_constructors_of_raw_type msg t argl : Rawterm.cases_pattern array  =
-  let ind,args = raw_decompose_app t in
-  match ind with
-    | RRef(_,IndRef ind')  ->
-(* 	let _,ind = Global.lookup_inductive ind' in *)
-	build_constructors_of_type msg ind' argl
-    | _ -> error msg
-	
-
-
+(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
 let rec find_type_of nb b = 
   let f,_ = raw_decompose_app b in 
   match f with 
@@ -412,18 +356,145 @@ let rec find_type_of nb b =
     | _ -> raise (Invalid_argument "not a ref")
     
 
-let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return = 
-(*   Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *)
+
+
+(******************)
+(* Main functions *)
+(******************)
+
+
+
+let raw_push_named (na,raw_value,raw_typ) env = 
+  match na with 
+    | Anonymous -> env 
+    | Name id -> 
+	let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in 
+	let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in 
+	Environ.push_named (id,value,typ) env
+
+
+let add_pat_variables pat typ env : Environ.env = 
+  let rec add_pat_variables env pat typ  : Environ.env = 
+    observe (str "new rel env := " ++ Printer.pr_rel_context_of env);
+
+    match pat with 
+      | PatVar(_,na) -> Environ.push_rel (na,None,typ) env 
+      | PatCstr(_,c,patl,na) -> 
+	  let Inductiveops.IndType(indf,indargs) = 
+	    try Inductiveops.find_rectype env Evd.empty typ
+	    with Not_found -> assert false 
+	  in
+	  let constructors = Inductiveops.get_constructors env indf in 
+	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in 
+	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in 
+	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) 
+  in
+  let new_env = add_pat_variables  env pat typ in 
+  let res =
+    fst (
+      Sign.fold_rel_context
+	(fun (na,v,t) (env,ctxt) ->
+	 match na with
+	   | Anonymous -> assert false
+	   | Name id ->
+	       let new_t =  substl ctxt t in
+	       let new_v = option_map (substl ctxt) v in
+	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
+			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
+			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
+			  option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
+			  option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+		       );
+	       (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
+      )
+	(Environ.rel_context new_env)
+	~init:(env,[])
+    )
+  in
+  observe (str "new var env := " ++ Printer.pr_named_context_of res);
+  res
+
+
+
+
+let rec pattern_to_term_and_type env typ  = function
+  | PatVar(loc,Anonymous) -> assert false
+  | PatVar(loc,Name id) ->
+	mkRVar id
+  | PatCstr(loc,constr,patternl,_) ->
+      let cst_narg =
+	Inductiveops.mis_constructor_nargs_env
+	  (Global.env ())
+	  constr
+      in
+      let Inductiveops.IndType(indf,indargs) = 
+	try Inductiveops.find_rectype env Evd.empty typ
+	with Not_found -> assert false 
+      in
+      let constructors = Inductiveops.get_constructors env indf in 
+      let constructor  = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in 
+      let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in 
+      let _,cstl = Inductiveops.dest_ind_family indf in 
+      let csta = Array.of_list cstl in 
+      let implicit_args =
+	Array.to_list
+	  (Array.init
+	     (cst_narg - List.length patternl)
+	     (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i))
+	  )
+      in
+      let patl_as_term =
+	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
+      in
+      mkRApp(mkRRef(Libnames.ConstructRef constr),
+	     implicit_args@patl_as_term
+	    )
+
+(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) 
+   of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the 
+   corresponding graphs. 
+
+
+   The idea to transform a term [t] into a list of constructors [lc] is the following:
+   \begin{itemize} 
+   \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding 
+   to [body] and add (bind x. _) to each elements of [lc]
+   \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames) 
+   then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], 
+   then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn], 
+   [g c1 ... cn] is an element of [lc]
+   \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then 
+   compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn], 
+   then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn]
+   create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc]
+   \item if the term is a cast just treat its body part
+   \item 
+   if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case 
+   and concatenate them (informally, each branch of a match produces a new constructor)
+   \end{itemize}
+   
+   WARNING: The terms constructed here are only USING the rawconstr syntax but are highly bad formed. 
+   We must wait to have complete all the current calculi to set the recursive calls. 
+   At this point, each term [f t1 ... tn]  (where f appears in [funnames]) is replaced by 
+   a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later. 
+   We in fact not create a constructor list since then end of each constructor has not the expected form 
+   but only the value of the function 
+*)
+
+
+let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return = 
+  observe (str " Entering : " ++ Printer.pr_rawconstr rt);
   match rt with 
     | RRef _ | RVar _ | REvar _ | RPatVar _     | RSort _  | RHole _  -> 
-	mk_result [] rt avoid
+	(* do nothing (except changing type of course) *)
+	mk_result [] rt avoid 
     | RApp(_,_,_) ->
 	let f,args = raw_decompose_app rt in
 	let args_res : (rawconstr list) build_entry_return =
-	  List.fold_right
+	  List.fold_right (* create the arguments lists of constructors and combine them *)
 	    (fun arg ctxt_argsl ->
-	       let arg_res = build_entry_lc  funnames ctxt_argsl.to_avoid arg in
-	       combine_results combine_args  arg_res ctxt_argsl
+	       let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
+	       combine_results combine_args arg_res ctxt_argsl
 	    )
 	    args
 	    (mk_result [] [] avoid)
@@ -431,6 +502,16 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 	begin
 	  match f with
 	    | RVar(_,id) when Idset.mem id funnames ->
+		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
+		   then we create a fresh variable [res], 
+		   add [res] and its "value" (i.e. [res v1 ... vn]) to each 
+		   pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and 
+		   a pseudo value "v1 ... vn". 
+		   The "value" of this branch is then simply [res]
+		*)
+		let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in 
+		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in 
+		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
 		let res = fresh_id args_res.to_avoid "res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkRVar res in 
@@ -438,7 +519,7 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 		  List.map 
 		    (fun arg_res -> 
 		       let new_hyps = 
-			 [Prod (Name res),mkRHole ();
+			 [Prod (Name res),res_raw_type;
 			  Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
 		       in
 		       {context =  arg_res.context@new_hyps; value = res_rt } 
@@ -447,6 +528,11 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 		in 
 		{ result = new_result; to_avoid = new_avoid }
 	    | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ -> 
+		(* if have [g t1 ... tn] with [g] not appearing in [funnames] 
+		   then  
+		   foreach [ctxt,v1 ... vn] in [args_res] we return  
+		   [ctxt, g v1 .... vn]
+		*)
 		{
 		  args_res with 
 		    result = 
@@ -455,8 +541,12 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 			 {args_res with value = mkRApp(f,args_res.value)})
 		      args_res.result
 		}
-	    | RApp _ -> assert false (* we have collected all the app *)
+	    | RApp _ -> assert false (* we have collected all the app in [raw_decompose_app] *)
        	    | RLetIn(_,n,t,b) -> 
+		(* if we have [(let x := v in b) t1 ... tn] , 
+		   we discard our work and compute the list of constructor for 
+		   [let x = v in (b t1 ... tn)] up to alpha conversion 
+		*)
 		let new_n,new_b,new_avoid = 
 		  match n with 
 		    | Name id when List.exists (is_free_in id) args -> 
@@ -473,136 +563,169 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 		    | _ -> n,b,avoid
 		in
 		build_entry_lc 
+		  env
 		  funnames 
 		  avoid
 		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
 	    | RCases _ | RLambda _ | RIf _ | RLetTuple _ -> 
-		let f_res = build_entry_lc funnames  args_res.to_avoid f in
+		(* we have [(match e1, ...., en with ..... end) t1 tn]
+		   we first compute the result from the case and 
+		   then combine each of them with each of args one
+		*)
+		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
-	    | RDynamic _ ->error "Not handled RDynamic"
+	    | RDynamic _ ->error "Not handled RDynamic" 
 	    | RCast(_,b,_,_) -> 
-		build_entry_lc funnames  avoid (mkRApp(b,args))
+		(* for an applied cast we just trash the cast part 
+		   and restart the work. 
+
+		   WARNING: We need to restart since [b] itself should be an application term
+		*)
+		build_entry_lc env funnames avoid (mkRApp(b,args))
 	    | RRec _ -> error "Not handled RRec"
 	    | RProd _ -> error "Cannot apply a type"
-	end
+	end (* end of the application treatement *) 
+
     | RLambda(_,n,t,b) ->
-	let b_res = build_entry_lc funnames avoid b in
-	let t_res = build_entry_lc funnames avoid t  in
+	(* we first compute the list of constructor 
+	   corresponding to the body of the function, 
+	   then the one corresponding to the type 
+	   and combine the two result
+	*)
+	let t_res = build_entry_lc env funnames avoid t  in
 	let new_n = 
 	  match n with 
 	    | Name _ -> n 
 	    | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
 	in
+	let new_env = raw_push_named (new_n,None,t) env in
+	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_lam new_n) t_res b_res
     | RProd(_,n,t,b) ->
-	let b_res = build_entry_lc funnames avoid b in
-	let t_res = build_entry_lc funnames avoid t in
+	(* we first compute the list of constructor 
+	   corresponding to the body of the function, 
+	   then the one corresponding to the type 
+	   and combine the two result
+	*)
+	let t_res = build_entry_lc env funnames avoid t in
+	let new_env = raw_push_named (n,None,t) env in
+	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_prod n) t_res b_res
-    | RLetIn(_,n,t,b) ->
-	let b_res = build_entry_lc funnames avoid b in
-	let t_res = build_entry_lc funnames avoid t in
-	combine_results (combine_letin n) t_res b_res
+    | RLetIn(_,n,v,b) ->
+	(* we first compute the list of constructor 
+	   corresponding to the body of the function, 
+	   then the one corresponding to the value [t] 
+	   and combine the two result
+	*)
+	let v_res = build_entry_lc env funnames avoid v in
+	let v_as_constr = Pretyping.Default.understand Evd.empty env v in 
+	let v_type = Typing.type_of env Evd.empty v_as_constr in 
+	let new_env = 
+	  match n with
+	      Anonymous -> env
+	    | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env 
+	in
+	let b_res = build_entry_lc new_env funnames avoid b in
+	combine_results (combine_letin n) v_res b_res
     | RCases(_,_,el,brl) -> 
+	(* we create the discrimination function 
+	   and treat the case itself 
+	*)
 	let make_discr = make_discr_match brl in 
-	build_entry_lc_from_case funnames make_discr el brl avoid
+	build_entry_lc_from_case env funnames make_discr el brl avoid
     | RIf(_,b,(na,e_option),lhs,rhs) -> 
-	begin
-	  match b with 
-	    | RCast(_,b,_,t) -> 
-		let msg = "If construction must be used with cast" in 
-		let case_pat = find_constructors_of_raw_type msg t [] in 
-		assert (Array.length case_pat = 2);
-		let brl = 
-		  list_map_i
-		    (fun i x -> (dummy_loc,[],[case_pat.(i)],x)) 
-		    0
-		    [lhs;rhs]
-		in 
-		let match_expr =
-		  mkRCases(None,[(b,(Anonymous,None))],brl)
-		in
-(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
-		build_entry_lc funnames avoid match_expr
-	    | _ ->  
-		try 
-		  let ind = find_type_of 2 b in 
-		  let case_pat = build_constructors_of_type (str "") ind [] in 
-		  let brl = 
-		  list_map_i
-		    (fun i x -> (dummy_loc,[],[case_pat.(i)],x)) 
-		    0
-		    [lhs;rhs]
-		in 
-		let match_expr =
-		  mkRCases(None,[(b,(Anonymous,None))],brl)
-		in
-		(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
-		build_entry_lc funnames avoid match_expr
-		with Invalid_argument s -> 
-		  let msg = "If construction must be used with cast : "^ s in 
-		  error msg
-		  
-	end
+	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	let b_typ = Typing.type_of env Evd.empty b_as_constr in 
+	let (ind,_) =  
+	  try Inductiveops.find_inductive env Evd.empty b_typ 
+	  with Not_found -> 
+	    errorlabstrm "" (str "Cannot find the inductive associated to " ++ 
+			       Printer.pr_rawconstr b ++ str " in " ++
+			       Printer.pr_rawconstr rt ++ str ". try again with a cast")
+	in
+	let case_pats = build_constructors_of_type ind [] in 
+	assert (Array.length case_pats = 2);
+	let brl =
+	  list_map_i
+	    (fun i x -> (dummy_loc,[],[case_pats.(i)],x))
+	    0
+	    [lhs;rhs]
+	in
+	let match_expr =
+	  mkRCases(None,[(b,(Anonymous,None))],brl)
+	in
+	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
+	build_entry_lc env funnames avoid match_expr
     | RLetTuple(_,nal,_,b,e) ->  
-	begin 
-	  let nal_as_rawconstr = 
-	    List.map 
-	      (function 
-		   Name id -> mkRVar id 
+	begin
+	  let nal_as_rawconstr =
+	    List.map
+	      (function
+		   Name id -> mkRVar id
 		 | Anonymous -> mkRHole ()
 	      )
-	      nal 
+	      nal
 	  in
-	  match b with 
-	    | RCast(_,b,_,t) -> 
-		let case_pat = 
-		  find_constructors_of_raw_type 
-		    "LetTuple construction must be used with cast" t nal_as_rawconstr in
-		assert (Array.length case_pat = 1);
-		let br = 
-		  (dummy_loc,[],[case_pat.(0)],e) 
-		in
-		let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in 
-		build_entry_lc funnames avoid match_expr
-	    | _ -> 
-		try 
-		  let ind = find_type_of 1 b in 
-		  let case_pat = 
-		    build_constructors_of_type 
-		      (str "LetTuple construction must be used with cast") ind nal_as_rawconstr in 
-		  let br = 
-		    (dummy_loc,[],[case_pat.(0)],e) 
-		  in
-		  let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in 
-		  build_entry_lc funnames avoid match_expr
-		with Invalid_argument s -> 
-		  let msg = "LetTuple construction must be used with cast : "^ s in 
-		  error msg
-		
+	  let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+	  let b_typ = Typing.type_of env Evd.empty b_as_constr in 
+	  let (ind,_) = 
+	    try Inductiveops.find_inductive env Evd.empty b_typ 
+	    with Not_found -> 
+	      errorlabstrm "" (str "Cannot find the inductive associated to " ++ 
+				 Printer.pr_rawconstr b ++ str " in " ++
+				 Printer.pr_rawconstr rt ++ str ". try again with a cast")
+	  in
+	  let case_pats = build_constructors_of_type ind nal_as_rawconstr in 
+	  assert (Array.length case_pats = 1);
+	  let br =
+	    (dummy_loc,[],[case_pats.(0)],e)
+	  in
+	  let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+	  build_entry_lc env funnames avoid match_expr
+
 	end
     | RRec _ -> error "Not handled RRec"
     | RCast(_,b,_,_) -> 
-	build_entry_lc funnames  avoid b
+	build_entry_lc env funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
-and build_entry_lc_from_case funname make_discr
+and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuple)
     (brl:Rawterm.cases_clauses) avoid : 
     rawconstr build_entry_return = 
   match el with 
-    | [] -> assert false (* matched on Nothing !*) 
+    | [] -> assert false (* this case correspond to match <nothing> with .... !*) 
     | el -> 
+	(* this case correspond to 
+	   match el with brl end
+	   we first compute the list of lists corresponding to [el] and 
+	   combine them . 
+	   Then for each elemeent of the combinations, 
+	   we compute the result we compute one list per branch in [brl] and 
+	   finally we just concatenate those list 
+	*)
 	let case_resl = 
 	    List.fold_right
 	    (fun (case_arg,_) ctxt_argsl ->
-	       let arg_res = build_entry_lc funname avoid case_arg  in
+	       let arg_res = build_entry_lc env funname avoid case_arg  in
 	       combine_results combine_args arg_res ctxt_argsl
 	    )
 	    el
 	      (mk_result [] [] avoid)
 	in
+	(****** The next works only if the match is not dependent ****)
+	let types = 
+	  List.map (fun (case_arg,_) -> 
+		      let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in 
+		      Typing.type_of env Evd.empty case_arg_as_constr
+		   ) el
+	in
 	let results =
 	  List.map 
-	    (build_entry_lc_from_case_term funname (make_discr (List.map fst el)) []  brl case_resl.to_avoid) 
+	    (build_entry_lc_from_case_term
+	       env types
+	       funname (make_discr (* (List.map fst el) *))
+	       []  brl 
+	       case_resl.to_avoid) 
 	    case_resl.result 
 	in 
 	{ 
@@ -611,36 +734,54 @@ and build_entry_lc_from_case funname make_discr
 	    List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
 	} 
 
-and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid
+and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
     matched_expr =
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
+	(* alpha convertion to prevent name clashes *)
 	let _,idl,patl,return = alpha_br avoid br in
-	let new_avoid  = idl@avoid in 
-(* 	let e_ctxt,el = (matched_expr.context,matched_expr.value) in *)
-(*  	if  (List.length patl) <> (List.length el) *)
-(* 	then error ("Pattern matching on product: not yet implemented"); *)
+	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an indentifier *)
+	(* building a list of precondition stating that we are not in this branch 
+	   (will be used in the following recursive calls)
+	*)
+	let new_env = List.fold_right2 add_pat_variables patl types env in 
 	let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list = 
-	  List.map 
-	    (fun pat -> 
+	  List.map2
+	    (fun pat typ -> 
 	       fun avoid pat'_as_term -> 
 		 let renamed_pat,_,_ = alpha_pat avoid pat in
 		 let pat_ids = get_pattern_id renamed_pat  in 
-		 List.fold_right 
-		   (fun id acc -> mkRProd (Name id,mkRHole (),acc))
+		 let env_with_pat_ids = add_pat_variables pat typ new_env in 
+		   List.fold_right 
+		   (fun id acc -> 		 
+		      let typ_of_id = Typing.type_of env_with_pat_ids Evd.empty (mkVar id) in 
+		      let raw_typ_of_id = 
+			Detyping.detype false [] (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
+		      in
+		      mkRProd (Name id,raw_typ_of_id,acc))
 		   pat_ids
 		   (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
 	    )
 	    patl
+	    types
 	in
+	(* Checking if we can be in this branch 
+	   (will be used in the following recursive calls)
+	*)	   
 	let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
 	  List.map 
 	    (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat') 
 	    patl
 	in
+	(* 
+	   we first compute the other branch result (in ordrer to keep the order of the matching 
+	   as much as possible)
+	*)
 	let brl'_res =
 	  build_entry_lc_from_case_term
+	    env 
+	    types
 	    funname
 	    make_discr
 	    ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
@@ -648,48 +789,63 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
 	    avoid
 	    matched_expr
 	in
+	(* We know create the precondition of this branch i.e.
+
+	   1- the list of variable appearing in the different patterns of this branch and 
+	      the list of equation stating than el = patl (List.flatten ...)
+	   2- If there exists a previous branch which pattern unify with the one of this branch 
+              then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
+	*)
       	let those_pattern_preconds =
-(	  List.flatten
+	  (List.flatten
 	    (
-	    List.map2
-	      (fun pat e ->
+	      list_map3
+	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in 
+		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right 
 		   (fun id  acc -> 
 		      if Idset.mem id this_pat_ids 
-		      then (Prod (Name id),mkRHole ())::acc
+		      then (Prod (Name id),
+		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in 
+		      let raw_typ_of_id = 
+			Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id
+		      in
+		      raw_typ_of_id
+			   )::acc
 		      else acc
 			
 		   )
 		   idl
-		   [(Prod Anonymous,raw_make_eq pat_as_term e)]
+		   [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
 	      )
 	      patl
 	      matched_expr.value
+	      types
+	  )
 	  )
-)
 	  @
-	    (if List.exists (function (unifl,neql) ->
-			       let (unif,eqs) = 
-				 List.split (List.map2 (fun x y -> x y) unifl patl)
-			       in
-			       List.for_all (fun x -> x) unif) patterns_to_prevent
-	     then 
-	       let i = List.length patterns_to_prevent in 
-	       [(Prod Anonymous,make_discr  i  )]
-	     else 
-	       []
-	    )
+	  (if List.exists (function (unifl,_) ->
+			     let (unif,_) = 
+			       List.split (List.map2 (fun x y -> x y) unifl patl)
+			     in
+			     List.for_all (fun x -> x) unif) patterns_to_prevent
+	   then 
+	     let i = List.length patterns_to_prevent in 
+	     let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
+	     [(Prod Anonymous,make_discr pats_as_constr i  )]
+	   else 
+	     []
+	  )
 	in
-	let return_res = build_entry_lc funname new_avoid return in
+	(* We compute the result of the value returned by the branch*)
+	let return_res = build_entry_lc new_env funname new_avoid return in
+	(* and combine it with the preconds computed for this branch *)
 	let this_branch_res =
 	  List.map
 	    (fun res  ->
-	       { context = 
-		   matched_expr.context@
-(* 		     ids@ *)
-		     those_pattern_preconds@res.context ;
+	       { context = matched_expr.context@those_pattern_preconds@res.context ;
 		 value = res.value}
 	    )
 	    return_res.result
@@ -702,7 +858,9 @@ let is_res id =
     String.sub (string_of_id id) 0 3 = "res"
   with Invalid_argument _ -> false 
 
-(* rebuild the raw constructors expression. 
+(* 
+   The second phase which reconstruct the real type of the constructor. 
+   rebuild the raw constructors expression. 
    eliminates some meaningless equalities, applies some rewrites......
 *)
 let rec rebuild_cons nb_args relname args crossed_types depth rt = 
@@ -722,6 +880,10 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 			    args new_crossed_types
 			    (depth + 1) b
 			in 
+			(*i The next call to mk_rel_id is valid since we are constructing the graph
+			  Ensures by: obvious
+			  i*) 
+
 			let new_t = 
 			  mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) 
 			in mkRProd(n,new_t,new_b),
@@ -730,7 +892,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 			assert false 
 		end
 	    | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt]) 
-		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  
+		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
 		  -> 
 		let is_in_b = is_free_in id b in
 		let _keep_eq = 
@@ -748,9 +910,11 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 		    (depth + 1) subst_b
 		in 
 		mkRProd(n,t,new_b),id_to_exclude
-(*  		if keep_eq then *)
-(* 		  mkRProd(n,t,new_b),id_to_exclude *)
-(* 		else new_b, Idset.add id id_to_exclude *)
+		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities 
+		     if keep_eq then
+		     mkRProd(n,t,new_b),id_to_exclude
+		     else new_b, Idset.add id id_to_exclude
+		  *)
 	    | _ -> 
 		let new_b,id_to_exclude =  
 		  rebuild_cons 
@@ -766,18 +930,8 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 	end
     | RLambda(_,n,t,b) ->
 	begin
-(* 	  let not_free_in_t id = not (is_free_in id t) in  *)
-(* 	  let new_crossed_types = t :: crossed_types in  *)
-(* 	  let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in *)
-(* 	  match n with *)
-(* 	    | Name id when Idset.mem id id_to_exclude -> *)
-(* 		new_b, *)
-(* 		Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
-(* 	    | _ ->  *)
-(* 		RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude *)
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
-(* 	  let new_b,id_to_exclude = rebuild_cons relname (args new_crossed_types b in *)
 	  match n with
 	    | Name id ->
 		let new_b,id_to_exclude = 
@@ -838,15 +992,24 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
     | _ -> mkRApp(mkRVar  relname,args@[rt]),Idset.empty
 
 
+(* debuging wrapper *)
 let rebuild_cons nb_args relname args crossed_types rt = 
-  observennl  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ 
-		 str "nb_args := " ++ str (string_of_int nb_args));
+(*   observennl  (str "rebuild_cons : rt := "++ pr_rawconstr rt ++  *)
+(* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
   let res = 
     rebuild_cons nb_args relname args crossed_types 0 rt 
   in
-  observe (str " leads to "++ pr_rawconstr (fst res));
+(*   observe (str " leads to "++ pr_rawconstr (fst res)); *)
   res
 
+
+(* naive implementation of parameter detection. 
+
+   A parameter is an argument which is only preceded by parameters and whose 
+   calls are all syntaxically equal. 
+
+   TODO: Find a valid way to deal with implicit arguments here! 
+*)
 let rec compute_cst_params relnames params = function 
   | RRef _ | RVar _ | REvar _ | RPatVar _ -> params
   | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames ->
@@ -900,13 +1063,6 @@ let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool)
   in 
   List.rev !l
 
-(*      (Topconstr.CProdN
-	 (dummy_loc,
-	  [[(dummy_loc,Anonymous)],returned_types.(i)],
-	  Topconstr.CSort(dummy_loc, RProp Null )
-	 )
-      )
-*)
 let rec rebuild_return_type rt = 
   match rt with 
     | Topconstr.CProdN(loc,n,t') -> 
@@ -915,36 +1071,58 @@ let rec rebuild_return_type rt =
 	Topconstr.CArrow(loc,t,rebuild_return_type t')
     | Topconstr.CLetIn(loc,na,t,t') -> 
 	Topconstr.CLetIn(loc,na,t,rebuild_return_type t') 
-    | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc, RProp Null))
+    | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None))
 
 
-let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list)  returned_types (rtl:rawconstr list) =
+let build_inductive 
+    parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list)  
+    returned_types 
+    (rtl:rawconstr list) =
   let _time1 = System.get_time () in
 (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *)
   let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
   let funnames = Array.of_list funnames in  
   let funsargs = Array.of_list funsargs in 
   let returned_types = Array.of_list returned_types in
+  (* alpha_renaming of the body to prevent variable capture during manipulation *)
   let rtl_alpha = List.map (function rt ->  (alpha_rt [] rt) ) rtl in
   let rta = Array.of_list rtl_alpha in
+  (*i The next call to mk_rel_id is valid since we are constructing the graph
+    Ensures by: obvious
+    i*) 
   let relnames = Array.map mk_rel_id funnames in
   let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in 
-  let resa = Array.map (build_entry_lc funnames_as_set []) rta in 
+  (* Construction of the pseudo constructors *)
+  let env = 
+    Array.fold_right 
+      (fun id env -> 
+	 Environ.push_named (id,None,Typing.type_of env Evd.empty (Tacinterp.constr_of_id env id))  env
+      )
+      funnames 
+      (Global.env ())
+  in      
+  let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in 
+  (* and of the real constructors*)
   let constr i res = 
     List.map 
       (function result (* (args',concl') *) -> 
 	 let rt = compose_raw_context result.context result.value in 
 	 let nb_args = List.length funsargs.(i) in 
-(* 	 Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* 	   let old_implicit_args = Impargs.is_implicit_args () *)
+(* 	   and old_strict_implicit_args =  Impargs.is_strict_implicit_args () *)
+(* 	   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in *)
+(* 	   let old_rawprint = !Options.raw_print in  *)
+(* 	   Options.raw_print := true; *)
+(* 	   Impargs.make_implicit_args false; *)
+(* 	   Impargs.make_strict_implicit_args false; *)
+(* 	   Impargs.make_contextual_implicit_args false; *)
+(* 	   Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* 	   Impargs.make_implicit_args old_implicit_args; *)
+(* 	   Impargs.make_strict_implicit_args old_strict_implicit_args; *)
+(* 	   Impargs.make_contextual_implicit_args old_contextual_implicit_args; *)
+(* 	   Options.raw_print := old_rawprint; *)
 	 fst (
 	   rebuild_cons nb_args relnames.(i)
-(* 	     (List.map  *)
-(* 		(function  *)
-(* 		     (Anonymous,_,_) -> mkRVar(fresh_id res.to_avoid "x__")  *)
-(* 		   | Name id, _,_ -> mkRVar id *)
-(* 		) *)
-(* 		funsargs.(i) *)
-(* 	     )  *)
 	     []
 	     []
 	     rt 
@@ -952,15 +1130,21 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
       ) 
       res.result 
   in 
-  let next_constructor_id = ref (-1) in 
+  (* adding names to constructors  *)
+ let next_constructor_id = ref (-1) in 
   let mk_constructor_id i = 
     incr next_constructor_id;
+    (*i The next call to mk_rel_id is valid since we are constructing the graph
+      Ensures by: obvious
+      i*) 
     id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
   in
   let rel_constructors i rt : (identifier*rawconstr) list = 
+    next_constructor_id := (-1);
     List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
   in
   let rel_constructors = Array.mapi rel_constructors resa in
+  (* Computing the set of parameters if asked *)
   let rels_params = 
     if parametrize 
     then
@@ -968,12 +1152,12 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
     else []
   in
   let nrel_params = List.length rels_params in
-  let rel_constructors = 
+  let rel_constructors = (* Taking into account the parameters in constructors *)
     Array.map (List.map 
     (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
     rel_constructors
   in
-  let rel_arity i funargs = 
+  let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
     let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list  = 
       (snd (list_chop nrel_params funargs))
     in 
@@ -992,13 +1176,11 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
       )
       rel_first_args
       (rebuild_return_type returned_types.(i))
-(*       (Topconstr.CProdN *)
-(* 	 (dummy_loc, *)
-(* 	  [[(dummy_loc,Anonymous)],returned_types.(i)], *)
-(* 	  Topconstr.CSort(dummy_loc, RProp Null ) *)
-(* 	 ) *)
-(* ) *)
   in
+  (* We need to lift back our work topconstr but only with all information 
+     We mimick a Set Printing All. 
+     Then save the graphs and reset Printing options to their primitive values 
+  *)
   let rel_arities = Array.mapi rel_arity funsargs in
   let old_rawprint = !Options.raw_print in 
   Options.raw_print := true;
@@ -1017,9 +1199,9 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
   let ext_rels_constructors = 
     Array.map (List.map 
       (fun (id,t) -> 
-	 false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty t)
+	 false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty ((* zeta_normalize *) t))
       ))
-      rel_constructors
+      (rel_constructors)
   in
   let rel_ind i ext_rel_constructors = 
     (dummy_loc,relnames.(i)),
@@ -1030,26 +1212,26 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
   let rel_inds = Array.to_list ext_rel_constructors in 
-  let _ = 
-    observe (
-      str "Inductive" ++ spc () ++
-	prlist_with_sep 
-	(fun () -> fnl ()++spc () ++ str "with" ++ spc ()) 
-	(function ((_,id),_,params,ar,constr) -> 
-	   Ppconstr.pr_id id ++ spc () ++ 
-	     Ppconstr.pr_binders params ++ spc () ++
-	     str ":" ++ spc () ++ 
-	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ 
-	     prlist_with_sep 
-	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ())
-	     (function (_,((_,id),t)) -> 
-		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++
-		  Ppconstr.pr_lconstr_expr t)
-	     constr
-	)
-	rel_inds
-    )
-  in
+(*   let _ =  *)
+(*   Pp.msgnl  (\* observe *\) ( *)
+(*       str "Inductive" ++ spc () ++ *)
+(* 	prlist_with_sep  *)
+(* 	(fun () -> fnl ()++spc () ++ str "with" ++ spc ())  *)
+(* 	(function ((_,id),_,params,ar,constr) ->  *)
+(* 	   Ppconstr.pr_id id ++ spc () ++  *)
+(* 	     Ppconstr.pr_binders params ++ spc () ++ *)
+(* 	     str ":" ++ spc () ++  *)
+(* 	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
+(* 	     prlist_with_sep  *)
+(* 	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
+(* 	     (function (_,((_,id),t)) ->  *)
+(* 		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
+(* 		  Ppconstr.pr_lconstr_expr t) *)
+(* 	     constr *)
+(* 	) *)
+(* 	rel_inds *)
+(*     ) *)
+(*   in *)
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 0cda56df..9cd04123 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -1,16 +1,16 @@
 
-(* val new_build_entry_lc :  *)
-(*   Names.identifier list ->  *)
-(*   (Names.name*Rawterm.rawconstr) list list ->  *)
-(*   Topconstr.constr_expr list ->  *)
-(*   Rawterm.rawconstr list ->  *)
-(*   unit  *)
+
+(*
+  [build_inductive parametrize funnames funargs returned_types bodies] 
+  constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments 
+  and returning [returned_types] using bodies [bodies]
+*)
 
 val build_inductive :
-  bool -> 
-  Names.identifier list ->
-  (Names.name*Rawterm.rawconstr*bool) list list ->
-  Topconstr.constr_expr list ->
-  Rawterm.rawconstr list ->
+  bool -> (* if true try to detect parameter. Always use it as true except for debug *)
+  Names.identifier list -> (* The list of function name *)
+  (Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *)
+  Topconstr.constr_expr list -> (* The list of function returned type *)
+  Rawterm.rawconstr list -> (* the list of body *)
   unit
 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index c6406468..14805cf4 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
 let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
 let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-
+let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
 
 (*
   Some basic functions to decompose rawconstrs
@@ -49,8 +49,8 @@ let raw_decompose_app =
 
 
 (* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) 
-let raw_make_eq t1 t2  = 
-  mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[mkRHole ();t2;t1])
+let raw_make_eq ?(typ= mkRHole ()) t1 t2  = 
+  mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
 
 (* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) 
 let raw_make_neq t1 t2 = 
@@ -321,7 +321,7 @@ let rec alpha_rt excluded rt =
 	     List.map (alpha_rt excluded) args
 	    )
   in 
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  && false 
+  if Indfun_common.do_observe ()  && false 
   then
     Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
 	      prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++
@@ -386,30 +386,32 @@ let is_free_in id =
       
 
 
-let rec pattern_to_term  = function 
+let rec pattern_to_term  = function
   | PatVar(loc,Anonymous) -> assert false
-  | PatVar(loc,Name id) -> 
+  | PatVar(loc,Name id) ->
 	mkRVar id
-  | PatCstr(loc,constr,patternl,_) -> 
-      let cst_narg = 
+  | PatCstr(loc,constr,patternl,_) ->
+      let cst_narg =
 	Inductiveops.mis_constructor_nargs_env
 	  (Global.env ())
 	  constr
       in
-      let implicit_args =  
-	Array.to_list 
-	  (Array.init 
+      let implicit_args =
+	Array.to_list
+	  (Array.init
 	     (cst_narg - List.length patternl)
 	     (fun _ -> mkRHole ())
 	  )
       in
-      let patl_as_term = 
+      let patl_as_term =
 	List.map pattern_to_term patternl
       in
       mkRApp(mkRRef(Libnames.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
 
+  
+
 let replace_var_by_term x_id term = 
   let rec replace_var_by_pattern rt = 
     match rt with 
@@ -539,3 +541,63 @@ let ids_of_pat =
   in
   ids_of_pat Idset.empty 
   
+
+
+
+
+let zeta_normalize = 
+  let rec zeta_normalize_term rt = 
+    match rt with 
+      | RRef _ -> rt 
+      | RVar _ -> rt 
+      | REvar _ -> rt 
+      | RPatVar _ -> rt 
+      | RApp(loc,rt',rtl) -> 
+	  RApp(loc,
+	       zeta_normalize_term rt',
+	       List.map zeta_normalize_term rtl
+	      )
+      | RLambda(loc,name,t,b) -> 
+	  RLambda(loc,
+		  name,
+		  zeta_normalize_term t,
+		  zeta_normalize_term b
+		 )
+      | RProd(loc,name,t,b) -> 
+	  RProd(loc,
+		name, 		  
+		zeta_normalize_term t,
+		zeta_normalize_term b
+		 )
+      | RLetIn(_,Name id,def,b) -> 
+	  zeta_normalize_term (replace_var_by_term id def b)
+      | RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
+      | RLetTuple(loc,nal,(na,rto),def,b) -> 
+	  RLetTuple(loc,
+		    nal,
+		    (na,option_map zeta_normalize_term rto),
+		    zeta_normalize_term def,
+		    zeta_normalize_term b
+		   )
+      | RCases(loc,infos,el,brl) -> 
+	  RCases(loc,
+		 infos,
+		 List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, 
+		 List.map zeta_normalize_br brl
+		)
+      | RIf(loc,b,(na,e_option),lhs,rhs) -> 
+	  RIf(loc, zeta_normalize_term b,
+	      (na,option_map zeta_normalize_term e_option),
+	      zeta_normalize_term lhs,
+	      zeta_normalize_term rhs
+	     )
+      | RRec _ -> raise (UserError("",str "Not handled RRec"))
+      | RSort _ -> rt 
+      | RHole _ -> rt 
+      | RCast(loc,b,k,t) -> 
+	  RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t)
+      | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+  and zeta_normalize_br (loc,idl,patl,res) = 
+    (loc,idl,patl,zeta_normalize_term res)
+  in
+  zeta_normalize_term 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 5dcdb15c..aa355485 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -25,7 +25,7 @@ val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
 val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
 val mkRSort : rawsort -> rawconstr 
 val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
-
+val mkRCast : rawconstr* rawconstr -> rawconstr 
 (*
   Some basic functions to decompose rawconstrs
   These are analogous to the ones constrs
@@ -36,7 +36,7 @@ val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
 
 
 (* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) 
-val  raw_make_eq : rawconstr -> rawconstr -> rawconstr
+val  raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr
 (* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) 
 val  raw_make_neq : rawconstr -> rawconstr -> rawconstr
 (* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *) 
@@ -106,3 +106,9 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
    returns the set of variables appearing in a pattern 
 *)
 val   ids_of_pat : cases_pattern -> Names.Idset.t 
+
+
+(* 
+   removing let_in construction in a rawterm 
+*)
+val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 2c7e4d33..5d19079b 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -1,16 +1,10 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 (*s FunInv Tactic: inversion following the shape of a function.  *)
-(* Use:
-   \begin{itemize}
-   \item The Tacinv directory must be in the path (-I <path> option)
-   \item use the bytecode version of coqtop or coqc (-byte option), or make a
-         coqtop 
-   \item Do [Require Tacinv] to be able to use it.
-   \item For syntax see Tacinv.v
-   \end{itemize}
-*)
 
+(* Deprecated: see indfun_main.ml4 instead *)
+
+(* Don't delete this file yet, it may be used for other purposes *)
 
 (*i*)
 open Termops
@@ -862,7 +856,6 @@ END
 (* 
 *** Local Variables: ***
 *** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" ***
-*** tab-width: 1 ***
 *** tuareg-default-indent:1 ***
 *** tuareg-begin-indent:1 ***
 *** tuareg-let-indent:1 ***
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ecb04e07..024cb599 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -336,8 +336,8 @@ and
   | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, 
                                      List.map xlate_match_pattern l)
 and  translate_one_equation = function
-    (_,lp, a) -> CT_eqn ( xlate_match_pattern_ne_list lp,
-	     xlate_formula a)
+    (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
+  | _ -> xlate_error "TODO: disjunctive multiple patterns"
 and 
   xlate_binder_ne_list = function
     [] -> assert false
@@ -978,7 +978,7 @@ and xlate_tac =
 	let id_opt = 
 	  match out_gen Extratactics.rawwit_in_arg_hyp id_opt with 
 	  | None -> ctv_ID_OPT_NONE
-	  | Some id ->   ctf_ID_OPT_SOME (xlate_ident id)
+	  | Some (_,id) ->   ctf_ID_OPT_SOME (xlate_ident id)
 	in
 	let tac_opt = 
 	  match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with
@@ -2035,7 +2035,6 @@ let rec xlate_vernac =
   | VernacExtend (s, l) ->
       CT_user_vernac
        (CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l))
-  | VernacDebug b -> xlate_error "Debug On/Off not supported"
   | VernacList((_, a)::l) -> 
       CT_coerce_COMMAND_LIST_to_COMMAND
 	(CT_command_list(xlate_vernac a, 
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 2aa3516f..83ea5b63 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -49,6 +49,11 @@ Inductive term : Set :=
   | Tvar : nat -> term.
 
 Delimit Scope romega_scope with term.
+Arguments Scope Tplus [romega_scope romega_scope].
+Arguments Scope Tmult [romega_scope romega_scope].
+Arguments Scope Tminus [romega_scope romega_scope].
+Arguments Scope Topp [romega_scope romega_scope].
+
 Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
 Infix "-" := Tminus : romega_scope.
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index bbf722db..ded069bf 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -20,3 +20,27 @@ Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
 End FixPoint.
 
 End Well_founded.
+
+Require Import Wf_nat.
+Require Import Lt.
+
+Section Well_founded_measure.
+Variable A : Set.
+Variable f : A -> nat.
+Definition R := fun x y => f x < f y.
+
+Section FixPoint.
+
+Variable P : A -> Set.
+
+Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
+ 
+Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x :=
+   F_sub x (fun y: { y : A | f y < f x}  => Fix_measure_F_sub (proj1_sig y) 
+   (Acc_inv r (f (proj1_sig y)) (proj2_sig y))).
+
+Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
+
+End FixPoint.
+
+End Well_founded_measure.
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index db10cb2a..b1694d7c 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -34,3 +34,13 @@ induction t.
  simpl ; auto.
 Qed.
 
+Ltac destruct_one_pair :=
+ match goal with
+ | [H : (ex _) |- _] => destruct H
+ | [H : (ex2 _) |- _] => destruct H
+ | [H : (sig _) |- _] => destruct H
+ | [H : (_ /\ _) |- _] => destruct H
+end.
+
+Ltac destruct_exists := repeat (destruct_one_pair) .
+
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 382ae2d5..859f9013 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -16,7 +16,7 @@ let reverse_array arr =
   Array.of_list (List.rev (Array.to_list arr))
     
 let trace s = 
-  if !Options.debug then msgnl s
+  if !Options.debug then (msgnl s; msgerr s)
   else ()
 
 (** Utilities to find indices in lists *)
@@ -37,7 +37,9 @@ let list_assoc_index x l =
 let subst_evars evs n t = 
   let evar_info id = 
     let rec aux i = function
-	(k, h, v) :: tl -> if k = id then (i, h, v) else aux (succ i) tl
+	(k, h, v) :: tl -> 
+	  trace (str "Searching for " ++ int id ++ str " found: " ++ int k);
+	  if k = id then (i, h, v) else aux (succ i) tl
       | [] -> raise Not_found
     in 
     let (idx, hyps, v) = aux 0 evs in
@@ -45,29 +47,29 @@ let subst_evars evs n t =
   in
   let rec substrec depth c = match kind_of_term c with
     | Evar (k, args) ->
-	(try 
-	   let index, hyps = evar_info k in
-	     (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
-			 int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
-		
-	   let ex = mkRel (index + depth) in
-	     (* Evar arguments are created in inverse order, 
-		and we must not apply to defined ones (i.e. LetIn's)
-	     *)
-	   let args =
-	     let rec aux hyps args acc =
-	       match hyps, args with
-		   ((_, None, _) :: tlh), (c :: tla) -> 
-		     aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
-		 | ((_, Some _, _) :: tlh), (_ :: tla) ->
-		     aux tlh tla acc
-		 | [], [] -> acc
-		 | _, _ -> failwith "subst_evars: invalid argument"
-	     in aux hyps (Array.to_list args) [] 
-	   in
-	     mkApp (ex, Array.of_list args)
-	 with Not_found -> 
-	   anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found"))
+	(let index, hyps = 
+	   try evar_info k
+	   with Not_found -> 
+	     anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
+	 in
+	 (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+		       int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
+	 let ex = mkRel (index + depth) in
+	   (* Evar arguments are created in inverse order, 
+	      and we must not apply to defined ones (i.e. LetIn's)
+	   *)
+	 let args =
+	   let rec aux hyps args acc =
+	     match hyps, args with
+		 ((_, None, _) :: tlh), (c :: tla) -> 
+		   aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
+	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
+		   aux tlh tla acc
+	       | [], [] -> acc
+	       | _, _ -> failwith "subst_evars: invalid argument"
+	   in aux hyps (Array.to_list args) [] 
+	 in
+	   mkApp (ex, Array.of_list args))
     | _ -> map_constr_with_binders succ substrec depth c
   in 
     substrec 0 t
@@ -106,11 +108,13 @@ open Tacticals
 let eterm_term evm t tycon = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
-  let evl = to_list evm in
+  let evl = List.rev (to_list evm) in
+    trace (str "Eterm, transformed to list");
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
     fold_right 
       (fun (id, ev) l ->
+	 trace (str "Eterm: " ++ str "treating evar: " ++ int id);
 	 let hyps = Environ.named_context_of_val ev.evar_hyps in
 	 let y' = (id, hyps, etype_of_evar l ev hyps) in
 	   y' :: l) 
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index cd2e7c43..ffb16a19 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac.ml 8964 2006-06-20 13:52:21Z msozeau $ *)
 
 open Global
 open Pp
@@ -43,7 +43,7 @@ open Eterm
 let require_library dirpath =
   let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
     Library.require_library [qualid] None
-
+(*
 let subtac_one_fixpoint env isevars (f, decl) = 
   let ((id, n, bl, typ, body), decl) = 
     Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) 
@@ -53,7 +53,7 @@ let subtac_one_fixpoint env isevars (f, decl) =
 	       Ppconstr.pr_constr_expr body)
     with _ -> ()
   in ((id, n, bl, typ, body), decl)
-    
+*)
 	      
 let subtac_fixpoint isevars l = 
   (* TODO: Copy command.build_recursive *)
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
index a0d2fb2b..25922782 100644
--- a/contrib/subtac/subtac.mli
+++ b/contrib/subtac/subtac.mli
@@ -1,14 +1,3 @@
 val require_library : string -> unit
-val subtac_one_fixpoint :
-  'a ->
-  'b ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c
 val subtac_fixpoint : 'a -> 'b -> unit
 val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 7428e1ed..78c3c70b 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: subtac_coercion.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac_coercion.ml 8964 2006-06-20 13:52:21Z msozeau $ *)
 
 open Util
 open Names
@@ -106,25 +106,25 @@ module Coercion = struct
       : (Term.constr -> Term.constr) option 
       =
     let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
-      (try trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
+      (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ 
 		  str " and "++ my_print_constr env y ++ 
 		  str " with evars: " ++ spc () ++
 		  my_print_evardefs !isevars);
        with _ -> ());
     let rec coerce_unify env x y =
-      (try trace (str "coerce_unify from " ++ (my_print_constr env x) ++ 
+      (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ 
 		  str " to "++ my_print_constr env y)
        with _ -> ());
       try 
 	isevars := the_conv_x_leq env x y !isevars;
-	(try (trace (str "Unified " ++ (my_print_constr env x) ++ 
-		     str " and "++ my_print_constr env y));
+	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++ 
+			str " and "++ my_print_constr env y);
 	 with _ -> ());
 	None
       with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
-	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ 
+	(try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ 
 		    str " to "++ my_print_constr env y);
 	 with _ -> ());
 	match (kind_of_term x, kind_of_term y) with
@@ -370,7 +370,7 @@ module Coercion = struct
 
   let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
     (try
-       trace (str "inh_conv_coerce_to_fail called for " ++
+       debug 1 (str "inh_conv_coerce_to_fail called for " ++
 	      Termops.print_constr_env env t ++ str " and "++ spc () ++
 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -436,7 +436,7 @@ module Coercion = struct
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
     (try 
-       trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++
+       debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
 	      Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ 
 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -461,7 +461,7 @@ module Coercion = struct
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
     (try 
-       trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++
+       debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++
 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ 
 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b09228c0..c738d7a6 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -117,7 +117,8 @@ let interp_context sigma env params =
 
 let list_chop_hd i l = match list_chop i l with
   | (l1,x::l2) -> (l1,x,l2)
-  | _ -> assert false
+  | (x :: [], l2) -> ([], x, [])
+  | _ -> assert(false)
 
 let collect_non_rec env = 
   let rec searchrec lnonrec lnamerec ldefrec larrec nrec = 
@@ -173,82 +174,189 @@ let list_of_local_binders l =
     | [] -> List.rev acc
   in aux [] l
 
-let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+let lift_binders k n l =
+  let rec aux n = function
+    | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+    | [] -> []
+  in aux n l
+
+let rec gen_rels = function
+    0 -> []
+  | n -> mkRel n :: gen_rels (pred n)
+
+let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+  let sigma = Evd.empty in
+  let isevars = ref (Evd.create_evar_defs sigma) in
+  let env = Global.env() in 
+  let pr c = my_print_constr env c in
+  let prr = Printer.pr_rel_context env in
+  let pr_rel env = Printer.pr_rel_context env in
+  let _ = 
+    try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
+		 Ppconstr.pr_binders bl ++ str " : " ++ 
+		 Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+		 Ppconstr.pr_constr_expr body)
+    with _ -> ()
+  in
+  let env', binders_rel = interp_context isevars env bl in
+  let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
+  let before_length, after_length = List.length before, List.length after in
+  let argid = match argname with Name n -> n | _ -> assert(false) in
+  let _liftafter = lift_binders 1 after_length after in
+  let envwf = push_rel_context before env in
+  let wf_rel, measure_fn = 
+    let rconstr = interp_constr isevars envwf r in
+    if measure then
+      let lt_rel = constr_of_global (Lazy.force lt_ref) in
+      let name s = Name (id_of_string s) in
+	mkLambda (name "x", argtyp,
+		  mkLambda (name "y", argtyp,
+			    mkApp (lt_rel,
+				   [| mkApp (rconstr, [| mkRel 2 |]) ;
+				      mkApp (rconstr, [| mkRel 1 |]) |]))),
+	Some rconstr
+    else rconstr, None
+  in
+  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
+  in
+  let argid' = id_of_string (string_of_id argid ^ "'") in
+  let wfarg len = (Name argid', None, 
+		   mkSubset (Name argid') argtyp 
+		     (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+  in
+  let top_bl = after @ (arg :: before) in
+  let intern_bl = after @ (wfarg 1 :: arg :: before) in
+  let top_env = push_rel_context top_bl env in
+  let intern_env = push_rel_context intern_bl env in
+  let top_arity = interp_type isevars top_env arityc in
+  (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
+  let proj = (Lazy.force sig_).Coqlib.proj1 in
+  let projection = 
+    mkApp (proj, [| argtyp ;
+		    (mkLambda (Name argid', argtyp,
+			       (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ;
+		    mkRel 1
+		 |])
+  in
+  (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+  let intern_arity = substnl [projection] after_length top_arity in 
+  (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
+  let intern_before_env = push_rel_context before env in
+  let intern_fun_bl = after @ [wfarg 1]  in
+  (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
+  let intern_fun_arity = intern_arity in
+  (try debug 2 (str "Intern fun arity: " ++ 
+		  my_print_constr intern_env intern_fun_arity) with _ -> ());
+  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+  let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
+  let fun_bl = after @ (intern_fun_binder :: [arg]) in
+  (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
+  let fun_env = push_rel_context fun_bl intern_before_env in
+  let fun_arity = interp_type isevars fun_env arityc in
+  let intern_body = interp_casted_constr isevars fun_env body fun_arity in
+  let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
+  let _ = 
+      try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+		   str "Intern bl" ++ prr intern_bl ++ spc () ++
+		   str "Top bl" ++ prr top_bl ++ spc () ++
+		   str "Intern arity: " ++ pr intern_arity ++
+		   str "Top arity: " ++ pr top_arity ++ spc () ++
+		   str "Intern body " ++ pr intern_body_lam)
+      with _ -> ()
+  in
+  let _impl = 
+    if Impargs.is_implicit_args()
+    then Impargs.compute_implicits top_env top_arity
+    else [] 
+  in
+  let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
+  let fix_def =
+    match measure_fn with
+	None ->
+	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
+		 [| argtyp ;
+		    wf_rel ;
+		    make_existential dummy_loc intern_before_env isevars wf_proof ;
+		    prop ;
+		    intern_body_lam |])
+      | Some f ->
+	  mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
+		 [| argtyp ; f ; prop ;
+		    intern_body_lam |])
+  in
+  let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
+  let def = it_mkLambda_or_LetIn def_appl binders_rel in
+  let typ = it_mkProd_or_LetIn top_arity binders_rel in
+    debug 2 (str "Constructed def");
+    debug 2 (my_print_constr intern_before_env def);
+    debug 2 (str "Type: " ++ my_print_constr env typ);
+  let fullcoqc = Evarutil.nf_isevar !isevars def in
+  let fullctyp = Evarutil.nf_isevar !isevars typ in
+  let _ = try trace (str "After evar normalization: " ++ spc () ++
+		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
+		     ++ str "Coq type: " ++ my_print_constr env fullctyp) 
+     with _ -> () 
+  in
+  let evm = non_instanciated_map env isevars in
+  let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in
+  let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in 	
+  let evars_typ = out_some evars_typ in
+  (try trace (str "Building evars sum for : ");
+     List.iter
+       (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+       evars;
+   with _ -> ());
+  let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in
+  (try trace (str "Evars sum: " ++ my_print_constr env sumg);
+     trace (str "Evars type: " ++ my_print_constr env evars_typ);
+   with _ -> ());
+  let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
+    Command.start_proof proofid goal_proof_kind sumg
+      (fun strength gr -> 
+	 debug 2 (str "Proof finished");
+	 let def = constr_of_global gr in
+	 let args = Subtac_utils.destruct_ex def sumg in
+	 let _, newdef = decompose_lam_n (List.length args) evars_def in
+	 let constr = Term.substl (List.rev args) newdef in
+	   debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
+	   let ce = 
+	     { const_entry_body = constr;
+	       const_entry_type = Some fullctyp;
+	       const_entry_opaque = false;
+	       const_entry_boxed = boxed} 
+	   in
+	   let _constant = Declare.declare_constant 
+			    recname (DefinitionEntry ce,IsDefinition Definition)
+	   in
+	     definition_message recname);
+    trace (str "Started existentials proof");
+    Pfedit.by sum_tac;
+    trace (str "Applied sum tac")  
+
+let build_mutrec l boxed = 
   let sigma = Evd.empty
   and env0 = Global.env()
   in 
   let lnameargsardef =
     (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
-      lnameargsardef
+    l
   in
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
   and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
   in
-  (* Build the recursive context and notations for the recursive types *)
+    (* Build the recursive context and notations for the recursive types *)
   let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
-      (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) -> 
-	let isevars = ref (Evd.create_evar_defs sigma) in	  
-	  match ro with
-	      CStructRec ->
-		let arityc = Command.generalize_constr_expr arityc bl in
-		let arity = interp_type isevars env0 arityc in
-		let impl = 
-		  if Impargs.is_implicit_args()
-		  then Impargs.compute_implicits env0 arity
-		  else [] in
-		let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
-		  (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
-	    | CWfRec r -> 		    
-		let n = out_some n in 
-		let _ = 
-		  try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
-			     Ppconstr.pr_binders bl ++ str " : " ++ 
-			     Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
-			     Ppconstr.pr_constr_expr body)
-		  with _ -> ()
-		in
-		let env', binders_rel = interp_context isevars env0 bl in
-		let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
-		let argid = match argname with Name n -> n | _ -> assert(false) in
-		let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
-		let envwf = push_rel_context before env0 in
-		let wf_rel = interp_constr isevars envwf r in
-		let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
-		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
-		let argid' = id_of_string (string_of_id argid ^ "'") in
-		let before_length, after_length = List.length before, List.length after in
-		let full_length = before_length + 1 + after_length in
-		let wfarg len = (Name argid, None, 
-				 mkSubset (Name argid') argtyp 
-				   (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
-		in
-		let new_bl = after' @ (accarg :: arg :: before)
-		and intern_bl =  after @ (wfarg (before_length + 1) :: before)
-		in
-		let intern_env = push_rel_context intern_bl env0 in
-		let env' = push_rel_context new_bl env0 in
-		let arity = interp_type isevars intern_env arityc in
-		let intern_arity = it_mkProd_or_LetIn arity intern_bl in
-		let arity' = interp_type isevars env' arityc in
-		let arity' = it_mkProd_or_LetIn arity' new_bl in
-		let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
-		let _ = 
-		  let pr c = my_print_constr env c in
-		  let prr = Printer.pr_rel_context env in
-		    try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
-			       str "Intern bl" ++ prr intern_bl ++ spc () ++
-			       str "Extern bl" ++ prr new_bl ++ spc () ++
-			       str "Intern arity: " ++ pr intern_arity)
-		    with _ -> ()
-		in
-		let impl = 
-		  if Impargs.is_implicit_args()
-		  then Impargs.compute_implicits intern_env arity'
-		  else [] in
-		let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
-		  (Environ.push_named (recname,None,arity') env, impls', 
-		   (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
+      (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) -> 
+	 let isevars = ref (Evd.create_evar_defs sigma) in	  
+	 let arityc = Command.generalize_constr_expr arityc bl in
+	 let arity = interp_type isevars env0 arityc in
+	 let impl = 
+	   if Impargs.is_implicit_args()
+	   then Impargs.compute_implicits env0 arity
+	   else [] in
+	 let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+	   (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
       (env0,[],[]) lnameargsardef in
   let arityl = List.rev arityl in
   let notations = 
@@ -283,7 +391,6 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
     collect_non_rec env0 lrecnames recdef arityl nv in
-  let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *)
   let declare arrec defrec =
     let recvec = 
       Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
@@ -293,7 +400,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		  my_print_constr env0 (recvec.(i)));
        with _ -> ());
       let ce = 
-	{ const_entry_body = mkFix ((nvrec',i),recdecls); 
+	{ const_entry_body = mkFix ((nvrec,i),recdecls); 
           const_entry_type = Some arrec.(i);
           const_entry_opaque = false;
           const_entry_boxed = boxed} in
@@ -384,6 +491,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		  match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
       defs
   in
+    match real_evars with
+	[] -> declare (List.rev_map (fun (id, c, _) ->
+				   snd (decompose_lam_n recdefs c)) defs)
+      | l ->
+
     Subtac_utils.and_tac real_evars
       (fun f _ gr ->
 	 let _ = trace (str "Got a proof of: " ++ pr_global gr ++
@@ -431,5 +543,28 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		 Environ.NoBody -> trace (str "Constant has no body")
 	       | Environ.Opaque -> trace (str "Constant is opaque")
       )
+
+let out_n = function
+    Some n -> n
+  | None -> 0
+
+let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+  match lnameargsardef with
+    | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> 
+	build_wellfounded (id, out_n n, bl, typ, body) r false no boxed
+    | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> 
+	build_wellfounded (id, out_n n, bl, typ, body) r true no boxed
+    | l -> 
+	let lnameargsardef = 
+	  List.map (fun ((id, (n, ro), bl, typ, body), no) ->
+		 match ro with
+		     CStructRec -> (id, out_n n, bl, typ, body), no
+		   | CWfRec _ | CMeasureRec _ -> 
+		       errorlabstrm "Subtac_command.build_recursive"
+			 (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
+	    lnameargsardef
+	in
+	  build_mutrec lnameargsardef boxed;
+	  assert(false)
       
       
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index e1bbbbb5..90ffb892 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -38,5 +38,6 @@ val interp_constr_judgment :
   constr_expr -> unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
 val recursive_message : global_reference array -> std_ppcmds
+
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 858fad1a..bb35833f 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -60,7 +60,7 @@ let pr_binder_list b =
 
 
 let rec rewrite_rec_calls l c = c
-
+(*
 let rewrite_fixpoint env l (f, decl) = 
   let (id, (n, ro), bl, typ, body) = f in
   let body = rewrite_rec_calls l body in
@@ -151,3 +151,4 @@ let rewrite_fixpoint env l (f, decl) =
 			 Ppconstr.pr_constr_expr body')
 	  in (id, (succ n, ro), bl', typ, body'), decl
 
+*)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index fafbb2da..149e7580 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -15,14 +15,3 @@ val list_of_local_binders :
 val pr_binder_list :
   (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
 val rewrite_rec_calls : 'a -> 'b -> 'b
-val rewrite_fixpoint :
-  'a ->
-  'b ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c ->
-  (Names.identifier * (int * Topconstr.recursion_order_expr) *
-   Topconstr.local_binder list * Topconstr.constr_expr *
-   Topconstr.constr_expr) *
-  'c
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 59c858a6..d4db7c27 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -22,12 +22,16 @@ let fixsub = lazy (init_constant fixsub_module "Fix_sub")
 let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
 let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
 
-let make_ref s =  Qualid (dummy_loc, (qualid_of_string s))
-let well_founded_ref = make_ref "Init.Wf.Well_founded"
-let acc_ref = make_ref "Init.Wf.Acc"
-let acc_inv_ref = make_ref "Init.Wf.Acc_inv"
-let fix_sub_ref = make_ref "Coq.subtac.FixSub.Fix_sub"
-let lt_wf_ref = make_ref "Coq.Wf_nat.lt_wf"
+let make_ref l s = lazy (init_reference l s)
+let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
+let acc_ref = make_ref  ["Init";"Wf"] "Acc"
+let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
+let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
+let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
+let lt_ref = make_ref ["Init";"Peano"] "lt"
+let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
+
+let make_ref s = Qualid (dummy_loc, qualid_of_string s)
 let sig_ref = make_ref "Init.Specif.sig"
 let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
 let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
@@ -82,18 +86,19 @@ let my_print_evardefs = Evd.pr_evar_defs
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
 
+let debug_level = 2
 
 let debug n s = 
-  if !Options.debug then
+  if !Options.debug && n >= debug_level then
     msgnl s
   else ()
 
 let debug_msg n s = 
-  if !Options.debug then s
+  if !Options.debug  && n >= debug_level then s
   else mt ()
 
 let trace s = 
-  if !Options.debug then msgnl s
+  if !Options.debug  && debug_level > 0 then msgnl s
   else ()
 
 let wf_relations = Hashtbl.create 10
@@ -153,6 +158,9 @@ let non_instanciated_map env evd =
 let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
 let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
+let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
+
 let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
 let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
 
@@ -164,7 +172,7 @@ let build_dependent_sum l =
       (n, t) :: tl ->
 	let t' = mkLambda (Name n, t, typ) in
 	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
-	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
+	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)	    	     
 	   with _ -> ());
 	let tac' = 
 	  tclTHENS (assert_tac true (Name n) t) 
@@ -183,6 +191,39 @@ let build_dependent_sum l =
 	(_, hd) :: tl -> aux (intros, hd) tl
       | [] -> raise (Invalid_argument "build_dependent_sum")
 
+let id x = x
+
+let build_dependent_sum l =
+  let rec aux names conttac conttype = function
+      (n, t) :: ((_ :: _) as tl) ->
+	let hyptype = substl names t in
+	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
+	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
+	   with _ -> ());
+	let tac = assert_tac true (Name n) hyptype in
+	let conttac = 
+	  (fun cont -> 
+	     conttac
+	     (tclTHENS tac
+		([intros;
+		  (tclTHENSEQ 
+		     [constructor_tac (Some 1) 1 
+			(Rawterm.ImplicitBindings [mkVar n]);
+		      cont]);
+		 ])))
+	in
+	let conttype = 
+	  (fun typ -> 
+	     let tex = mkLambda (Name n, t, typ) in
+	       conttype
+		 (mkApp (Lazy.force ex_ind, [| t; tex |])))
+	in
+	  aux (mkVar n :: names) conttac conttype tl
+    | (n, t) :: [] -> 
+	(conttac intros, conttype t)
+    | [] -> raise (Invalid_argument "build_dependent_sum")
+  in aux [] id id (List.rev l)       
+	  
 open Proof_type
 open Tacexpr
 
@@ -251,6 +292,75 @@ let destruct_ex ext ex =
       | _ -> [acc]
   in aux ex ext
 
+open Rawterm
+
+
+let list_mapi f = 
+  let rec aux i = function 
+      hd :: tl -> f i hd :: aux (succ i) tl 
+    | [] -> []
+  in aux 0
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+  let tml = list_mapi (fun i (c, (n, opt)) -> c, 
+		       ((match n with
+			    Name id -> (match c with
+					  | RVar (_, id') when id = id' ->
+					      Name (id_of_string (string_of_id id ^ "'"))
+					  | _ -> n)
+			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
+			opt)) tml 
+  in
+  let mkHole = RHole (dummy_loc, InternalHole) in
+  let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+		       [mkHole; c; n])
+  in
+  let eqs_types = 
+    List.map
+      (fun (c, (n, _)) ->
+	 let id = match n with Name id -> id | _ -> assert false in
+	 let heqid = id_of_string ("Heq" ^ string_of_id id) in
+	   Name heqid, mkeq c (RVar (dummy_loc, id)))
+      tml
+  in
+  let po = 
+    List.fold_right
+      (fun (n,t) acc ->
+	 RProd (dummy_loc, Anonymous, t, acc))
+      eqs_types (match po with 
+		     Some e -> e
+		   | None -> mkHole)
+  in
+  let eqns =   
+    List.map (fun (loc, idl, cpl, c) ->
+		let c' = 
+		  List.fold_left 
+		    (fun acc (n, t) ->
+		       RLambda (dummy_loc, n, mkHole, acc))
+		    c eqs_types
+		in (loc, idl, cpl, c'))
+      eqns
+  in
+  let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+			      [mkHole; c])
+  in
+  let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
+  let case = RCases (loc,Some po,tml,eqns) in
+  let app = RApp (dummy_loc, case, refls) in
+    app
+
+let rec rewrite_cases c = 
+  match c with 
+      RCases _ -> let c' = map_rawconstr rewrite_cases c in
+	(match c' with 
+	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+	   | _ -> assert(false))
+    | _ -> map_rawconstr rewrite_cases c
+	  
+let rewrite_cases env c =
+  let c' = rewrite_cases c in
+  let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+    c'
 
 let list_mapi f = 
   let rec aux i = function 
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a90f281f..4a7e8177 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -18,12 +18,13 @@ val fixsub_module : string list
 val init_constant : string list -> string -> constr
 val init_reference : string list -> string -> global_reference
 val fixsub : constr lazy_t
-val make_ref : string -> reference
-val well_founded_ref : reference
-val acc_ref : reference
-val acc_inv_ref : reference
-val fix_sub_ref : reference
-val lt_wf_ref : reference
+val well_founded_ref : global_reference lazy_t
+val acc_ref : global_reference lazy_t
+val acc_inv_ref : global_reference lazy_t
+val fix_sub_ref : global_reference lazy_t
+val fix_measure_sub_ref : global_reference lazy_t
+val lt_ref : global_reference lazy_t
+val lt_wf_ref : global_reference lazy_t
 val sig_ref : reference
 val proj1_sig_ref : reference
 val proj2_sig_ref : reference
@@ -69,6 +70,8 @@ val string_of_hole_kind : hole_kind -> string
 val non_instanciated_map : env -> evar_defs ref -> evar_map
 val global_kind : logical_kind
 val goal_kind : locality_flag * goal_object_kind
+val global_proof_kind : logical_kind
+val goal_proof_kind : locality_flag * goal_object_kind
 val global_fix_kind : logical_kind
 val goal_fix_kind : locality_flag * goal_object_kind
 
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index a29cd039..8429c267 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -5,12 +5,13 @@ Variable A : Set.
 
 Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
   fun l =>
-    match l with
+    match `l with
     | nil => _
     | hd :: tl => hd
     end.
 Proof.
-  destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+  destruct l ; simpl ; intro H.
+  rewrite H in n ; intuition.
 Defined.
 
 
@@ -24,7 +25,7 @@ Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
     | hd :: tl => tl
     end.
 Proof.
-destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+destruct l ; simpl ; intro H ; rewrite H in n ; intuition.
 Defined.
 
 Extraction mytail.
@@ -50,7 +51,6 @@ Program Fixpoint append (l : list A) (l' : list A) { struct l } :
  | nil => l'
  | hd :: tl => hd :: (append tl l')
  end.
-simpl.
 subst ; auto.
 simpl ; rewrite (subset_simpl (append tl0 l')).
 simpl ; subst.
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index ab200354..0b40ef82 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,7 +1,13 @@
-Fixpoint f (a : nat) : nat := match a with 0 => 0
-| S a' => g a a'
+Program Fixpoint f (a : nat) : nat := 
+  match a with
+  | 0 => 0
+  | S a' => g a a'
   end
 with g (a b : nat) { struct b } : nat := 
-  match b with 0 => 0
+  match b with
+  | 0 => 0
   | S b' => f b'
-  end.
\ No newline at end of file
+  end.
+
+Check f.
+Check g.
\ No newline at end of file
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 481b6708..ba5bdf23 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -12,8 +12,8 @@ reflexivity.
 Defined.
 
 Extraction testsig.
-Extraction sigS.
-Extract Inductive sigS => "" [ "" ].
+Extraction sig.
+Extract Inductive sig => "" [ "" ].
 Extraction testsig.
 
 Require Import Coq.Arith.Compare_dec.
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
new file mode 100644
index 00000000..4764037d
--- /dev/null
+++ b/contrib/subtac/test/measure.v
@@ -0,0 +1,24 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Fixpoint size (a : nat) : nat :=
+  match a with
+  0 => 1
+  | S n => S (size n)
+  end.
+
+Program Fixpoint test_measure (a : nat) {measure a size}  : nat :=
+  match a with
+  | S (S n) => S (test_measure n)
+  | x => x
+  end.
+subst.
+unfold n0.
+auto with arith.
+Qed.
+
+Check test_measure.
+Print test_measure.
\ No newline at end of file
diff --git a/contrib/subtac/test/wf.v b/contrib/subtac/test/wf.v
new file mode 100644
index 00000000..49fec2b8
--- /dev/null
+++ b/contrib/subtac/test/wf.v
@@ -0,0 +1,48 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Ltac one_simpl_hyp :=
+ match goal with
+ | [H : (`exist _ _ _) = _ |- _] => simpl in H
+ | [H : _ = (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) < _ |- _] => simpl in H
+ | [H : _ < (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) <= _ |- _] => simpl in H
+ | [H : _ <= (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) > _ |- _] => simpl in H
+ | [H : _ > (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) >= _ |- _] => simpl in H
+ | [H : _ >= (`exist _ _ _) |- _] => simpl in H
+ end.
+
+Ltac one_simpl_subtac :=
+  destruct_exists ;
+  repeat one_simpl_hyp ; simpl.
+
+Ltac simpl_subtac :=  do 3 one_simpl_subtac ; simpl.
+
+Require Import Omega.
+Require Import Wf_nat.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
+  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
+  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
+  (S q' & r)
+  else (O & a).
+destruct b ; simpl_subtac.
+omega.
+simpl_subtac.
+assert(x0 * S q' = x0 + x0 * q').
+rewrite <- mult_n_Sm.
+omega.
+rewrite H2 ; omega.
+simpl_subtac.
+split ; auto with arith.
+omega.
+apply lt_wf.
+Defined.
+
+Check euclid_evars_proof.
\ No newline at end of file
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 2235be4a..b6b1c7b6 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -474,7 +474,7 @@ let kind_of_global r =
   match r with
   | Ln.IndRef kn | Ln.ConstructRef (kn,_) -> 
       let isrecord =
-	try let _ = Recordops.lookup_structure kn in true
+	try let _ = Recordops.lookup_projections kn in true
         with Not_found -> false in
       kind_of_inductive isrecord (fst kn)
   | Ln.VarRef id -> kind_of_variable id