Imported Upstream version 8.1~gammaupstream/8.1.gamma

13 files changed, 1578 insertions, 317 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 7977d4e0..14e2233f 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -39,12 +39,12 @@ let do_observe_tac s tac g =
 	    Cerrors.explain_exn e ++ str " on goal " ++ goal ); 
    raise e;;
 
-
-let observe_tac s tac g =
+let observe_tac_stream s tac g = 
   if do_observe ()
-  then do_observe_tac (str s) tac g
+  then do_observe_tac  s tac g
   else tac g
 
+let observe_tac s tac g = observe_tac_stream (str s) tac g
 
 let tclTRYD tac = 
   if  !Options.debug  || do_observe ()
@@ -179,10 +179,11 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
   let nochange msg  = 
     begin 
-(*       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    ); *)
+      observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    );
       failwith "NoChange"; 
     end
   in    
+  let eq_constr = Reductionops.is_conv env sigma in 
   if not (noccurn 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp t) then nochange "not an equality";
@@ -194,6 +195,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
     in 
     if not (closed0 t1) then nochange "not a closed lhs";    
     let rec compute_substitution sub t1 t2 = 
+      observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2);
       if isRel t2 
       then 
 	let t2 = destRel t2  in 
@@ -313,9 +315,13 @@ let h_reduce_with_zeta =
 
 
 let rewrite_until_var arg_num eq_ids : tactic =
+  (* tests if the declares recursive argument is neither a Constructor nor 
+     an applied Constructor since such a form for the recursive argument 
+     will break the Guard when trying to save the Lemma. 
+  *)
   let test_var g = 
     let _,args = destApp (pf_concl g) in 
-    not (isConstruct args.(arg_num))
+    not ((isConstruct args.(arg_num)) || isAppConstruct args.(arg_num))
   in
   let rec do_rewrite eq_ids g  = 
     if test_var g 
@@ -499,7 +505,7 @@ let clean_goal_with_heq ptes_infos continue_tac dyn_infos  =
     tclTHENLIST 
       [
 	tac ;
-	(continue_tac new_infos)
+	observe_tac "clean_hyp_with_heq continue" (continue_tac new_infos)
       ]
       g    
 
@@ -779,7 +785,7 @@ let build_proof
       finish_proof dyn_infos)
   in
   observe_tac "build_proof"
-    (build_proof do_finish_proof dyn_infos) 
+    (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) 
 
 
 
@@ -884,7 +890,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 (*   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 type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) 
+    (Typeops.type_of_constant_type (Global.env()) 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
@@ -1332,10 +1339,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
 	      h_intro hid;
 	      Elim.h_decompose_and (mkVar hid); 
 	      backtrack_eqs_until_hrec hrec eqs;
-	      tclCOMPLETE (tclTHENS  (* We must have exactly ONE subgoal !*)
-		(apply (mkVar hrec))
-		[ tclTHENSEQ 
-		    [
+	      observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" )
+		(tclTHENS  (* We must have exactly ONE subgoal !*)
+		   (apply (mkVar hrec))
+		   [ tclTHENSEQ 
+		       [
 			 thin [hrec];
 			 apply (Lazy.force acc_inv);
 			 (fun g -> 
@@ -1344,11 +1352,12 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
 			      unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g 
 			    else tclIDTAC g
 			 );
-			 tclTRY(Recdef.list_rewrite true eqs);
-			 observe_tac "finishing"  (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))
+			 observe_tac "rew_and_finish"
+			   (tclTHEN 
+			      (tclTRY(Recdef.list_rewrite true eqs))
+			      (observe_tac "finishing"  (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))))
 		       ]
-		]
-			  )
+		])
 	    ])
 	    gls
 
@@ -1371,7 +1380,7 @@ let is_valid_hypothesis predicates_name =
 	| _ -> false 
   in
   is_valid_hypothesis 
-
+(*
 let fresh_id avoid na = 
   let id =  
     match na with 
@@ -1450,7 +1459,7 @@ let prove_principle_for_gen
     let wf_tac = 
       if is_mes 
       then 
-	Recdef.tclUSER_if_not_mes 
+	(fun b -> Recdef.tclUSER_if_not_mes b None)
       else fun _ -> prove_with_tcc tcc_lemma_ref []
     in
     let start_tac g = 
@@ -1543,7 +1552,7 @@ let prove_principle_for_gen
 		   let pte_info = 
 		     { proving_tac =
 			 (fun eqs -> 
-			    observe_tac "prove_with_tcc" 
+			    observe_tac "new_prove_with_tcc" 
 			      (new_prove_with_tcc is_mes acc_inv hrec  tcc_lemma_ref (List.map mkVar eqs))
 			 );
 		       is_valid = is_valid_hypothesis predicates_names 
@@ -1583,13 +1592,160 @@ let prove_principle_for_gen
 	 arg_tac;
 	 start_tac
 	] g
+*)
 
-
-
-
-
-
-
+let prove_principle_for_gen
+    (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
+    rec_arg_num rec_arg_type relation gl = 
+  let princ_type = pf_concl gl in 
+  let princ_info = compute_elim_sig princ_type in 
+  let fresh_id = 
+    let avoid = ref (pf_ids_of_hyps gl) in 
+    fun na -> 
+      let new_id = 
+	  match na with 
+	    | Name id -> fresh_id !avoid (string_of_id id) 
+	    | Anonymous -> fresh_id !avoid "H" 
+      in
+      avoid := new_id :: !avoid;
+      Name new_id
+  in
+  let fresh_decl (na,b,t) = (fresh_id na,b,t) in
+  let princ_info : elim_scheme = 
+    { princ_info with 
+	params = List.map fresh_decl princ_info.params;
+	predicates = List.map fresh_decl princ_info.predicates; 
+	branches = List.map fresh_decl princ_info.branches; 
+	args = List.map fresh_decl princ_info.args
+    }
+  in
+  let wf_tac = 
+    if is_mes 
+    then 
+      (fun b -> Recdef.tclUSER_if_not_mes b None)
+    else fun _ -> prove_with_tcc tcc_lemma_ref []
+  in
+  let real_rec_arg_num = rec_arg_num - princ_info.nparams in 
+  let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in 
+  let (post_rec_arg,pre_rec_arg) = 
+    Util.list_chop npost_rec_arg princ_info.args
+  in
+  let rec_arg_id = 
+    match post_rec_arg with 
+      | (Name id,_,_)::_ -> id 
+      | _ -> assert false 
+  in
+  let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in 
+  let relation = substl subst_constrs relation in 
+  let input_type = substl subst_constrs rec_arg_type in 
+  let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in 
+  let acc_rec_arg_id = 
+    Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id)))))
+  in 
+  let revert l = 
+    tclTHEN (h_generalize (List.map mkVar l)) (clear l) 
+  in
+  let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in 
+  let prove_rec_arg_acc g = 
+      (observe_tac "prove_rec_arg_acc" 
+	 (tclCOMPLETE
+	    (tclTHEN
+	       (forward 
+		  (Some ((fun g -> observe_tac "prove wf" (tclCOMPLETE (wf_tac is_mes)) g)))
+		  (Genarg.IntroIdentifier wf_thm_id)
+		  (mkApp (delayed_force well_founded,[|input_type;relation|])))
+	       (
+		 observe_tac 
+		   "apply wf_thm" 
+		   (h_apply ((mkApp(mkVar wf_thm_id,
+				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+		   )
+	       )
+	    )
+	 )
+      )
+      g
+  in
+  let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
+  tclTHENSEQ
+    [ 
+      h_intros 
+	(List.rev_map (fun (na,_,_) -> Nameops.out_name na) 
+	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
+	);
+      observe_tac "" (forward
+	 (Some (prove_rec_arg_acc))
+	 (Genarg.IntroIdentifier acc_rec_arg_id)
+ 	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+      );
+      observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids)));
+      observe_tac "h_fix" (h_fix (Some fix_id) (real_rec_arg_num + 1)); 
+      h_intros (List.rev (acc_rec_arg_id::args_ids));
+      Equality.rewriteLR (mkConst eq_ref);
+      observe_tac "finish" (fun gl' -> 
+	 let body = 
+	   let _,args = destApp (pf_concl gl') in 
+	   array_last args
+	 in
+	 let body_info rec_hyps = 
+	   {
+	     nb_rec_hyps = List.length rec_hyps;
+	     rec_hyps = rec_hyps;
+	     eq_hyps = [];
+	     info = body
+	   }
+	 in 
+	 let acc_inv = 
+	   lazy (
+	     mkApp (
+	       delayed_force acc_inv_id,
+	       [|input_type;relation;mkVar rec_arg_id|]
+	     )
+	   )
+	 in
+	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
+	 let predicates_names = 
+	   List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
+	 in
+	 let pte_info = 
+	   { proving_tac =
+	       (fun eqs -> 
+		  observe_tac "new_prove_with_tcc" 
+		    (new_prove_with_tcc 
+		       is_mes acc_inv fix_id tcc_lemma_ref (List.map mkVar eqs)
+		    )
+	       );
+	     is_valid = is_valid_hypothesis predicates_names
+	   }
+	 in
+	 let ptes_info : pte_info Idmap.t = 
+	   List.fold_left
+	     (fun map pte_id -> 
+		Idmap.add pte_id 
+		  pte_info			       
+		  map
+	     )
+	     Idmap.empty
+	     predicates_names
+	 in
+	 let make_proof rec_hyps = 
+	   build_proof 
+	     false 
+	     [f_ref]
+	     ptes_info
+	     (body_info rec_hyps)
+	 in
+	 observe_tac "instanciate_hyps_with_args" 
+	   (instanciate_hyps_with_args 
+	      make_proof
+	      (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
+	      (List.rev args_ids)
+	   )
+	   gl'
+      )
+			   
+    ]
+    gl    
 
 
 
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index f83eae8d..89ebb75a 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -301,9 +301,18 @@ let pp_dur time time' =
   str (string_of_float (System.time_difference time time'))
 
 (* let qed () = save_named true  *)
-let defined () = Command.save_named false
-
-
+let defined () = 
+  try 
+    Command.save_named false 
+  with 
+    | UserError("extract_proof",msg) ->
+	Util.errorlabstrm
+	  "defined"
+	  ((try
+	      str "On goal : " ++ fnl () ++  pr_open_subgoals () ++ fnl ()
+	    with _ -> mt ()
+	   ) ++msg)
+    | e -> raise e
 
 
 
@@ -346,6 +355,7 @@ let generate_functional_principle
     interactive_proof
     old_princ_type sorts new_princ_name funs i proof_tac
     =
+  try 
   let f = funs.(i) in
   let type_sort = Termops.new_sort_in_family InType in
   let new_sorts =
@@ -384,6 +394,9 @@ let generate_functional_principle
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme)
 	    )
 	);
+	Options.if_verbose 
+	  (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) 
+	  name;
 	names := name :: !names
       in
       register_with_sort InProp;
@@ -393,6 +406,10 @@ let generate_functional_principle
     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
+  with 
+    | Defining_principle _ as e -> raise e
+    | e -> raise (Defining_principle e)
+
 (*   defined  () *)
 
 
@@ -591,13 +608,6 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
     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 bodies_types = 
     make_scheme 
       (List.map 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index dffc8120..82bb2869 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -39,7 +39,8 @@ let functional_induction with_clean c princl pat =
 		      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') )
+			  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
@@ -49,8 +50,9 @@ let functional_induction with_clean c princl pat =
 		    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*)
+			(*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'))
@@ -90,45 +92,45 @@ let functional_induction with_clean c princl pat =
     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
+	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
 	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)
+	 princ_infos
+	 args_as_induction_constr
+	 princ'
+	 pat)
       subst_and_reduce
       g
-
-
+      
+      
 
 
 type annot = 
     Struct of identifier 
-  | Wf of Topconstr.constr_expr * identifier option
-  | Mes of Topconstr.constr_expr * identifier option
+  | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
+  | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
 
 
 type newfixpoint_expr =
@@ -184,7 +186,7 @@ let build_newrecursive
 	States.unfreeze fs; raise e in
     States.unfreeze fs; def
   in
-  recdef
+  recdef,rec_impls
 	
 
 let compute_annot (name,annot,args,types,body) =
@@ -238,29 +240,47 @@ 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 derive_inversion fix_names =
+  try 
+    (* we first transform the fix_names identifier into their corresponding constant *)
+    let fix_names_as_constant = 
+      List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names 
+    in 
+    (* 
+       Then we check that the graphs have been defined 
+       If one of the graphs haven't been defined 
+       we do nothing
+    *)
+    List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ;
+    try
+      Invfun.derive_correctness 
+	Functional_principles_types.make_scheme
+	functional_induction 
+	fix_names_as_constant
+	(*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 built inversion information" ++ 
+	   if do_observe () then Cerrors.explain_exn e else mt ())
+  with _ -> ()
+
 let generate_principle 
-    do_built fix_rec_l recdefs  interactive_proof parametrize 
-    (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit =
+    is_general do_built fix_rec_l recdefs  interactive_proof 
+    (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
   let funs_types =  List.map (function (_,_,_,types,_) -> types) fix_rec_l in
   try 
     (* We then register the Inductive graphs of the functions  *)
-    Rawterm_to_relation.build_inductive parametrize names funs_args funs_types recdefs;
+    Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
     if do_built 
     then
       begin
@@ -286,8 +306,7 @@ let generate_principle
 	  list_map_i
 	    (fun i x ->
 	       let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in 
-	       let princ_type = 
-		 (Global.lookup_constant princ).Declarations.const_type
+	       let princ_type = Typeops.type_of_constant (Global.env()) princ
 	       in
 	       Functional_principles_types.generate_functional_principle
 		 interactive_proof 
@@ -301,12 +320,22 @@ let generate_principle
 	    0
 	    fix_rec_l
 	in 
-	Array.iter add_Function funs_kn;
+	Array.iter (add_Function is_general) funs_kn;
 	()
       end
   with e -> 
-    Pp.msg_warning (Cerrors.explain_exn e) 
-
+    match e with 
+      | Building_graph e -> 
+	    Pp.msg_warning 
+	    (str "Cannot define graph(s) for " ++ 
+	       h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	       if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+      | Defining_principle e -> 
+	    Pp.msg_warning
+	    (str "Cannot define principle(s) for "++ 
+	       h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	       if do_observe () then Cerrors.explain_exn e else mt ())
+      | _ -> anomaly ""
 
 let register_struct is_rec fixpoint_exprl = 
   match fixpoint_exprl with 
@@ -330,7 +359,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
 
 
-let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
+let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook 
     =  
   let type_of_f = Command.generalize_constr_expr ret_type args in 
@@ -349,13 +378,13 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
   in
   let unbounded_eq = 
     let f_app_args = 
-      Topconstr.CApp 
+      Topconstr.CAppExpl 
 	(dummy_loc, 
-	 (None,Topconstr.mkIdentC fname) ,
+	 (None,(Ident (dummy_loc,fname))) ,
 	 (List.map 
 	    (function
 	       | _,Anonymous -> assert false 
-	       | _,Name e -> (Topconstr.mkIdentC e,None)
+	       | _,Name e -> (Topconstr.mkIdentC e)
 	    ) 
 	    (Topconstr.names_of_local_assums args)
 	 )
@@ -365,7 +394,8 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Command.generalize_constr_expr unbounded_eq args in 
-  let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
+  let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
+      nb_args relation =
     try 
       pre_hook 
 	(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
@@ -377,15 +407,16 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
       ()
   in 
   Recdef.recursive_definition 
-    is_mes fname 
+    is_mes fname rec_impls
     type_of_f
     wf_rel_expr
     rec_arg_num
     eq
     hook
+    using_lemmas
 
     
-let register_mes fname wf_mes_expr wf_arg args ret_type body = 
+let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body = 
   let wf_arg_type,wf_arg = 
     match wf_arg with 
       | None -> 
@@ -424,35 +455,38 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body =
   let wf_rel_from_mes = 
     Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
   in
-  register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) args ret_type body
+  register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg) 
+    using_lemmas args ret_type body
 	  
 
 let do_generate_principle register_built interactive_proof fixpoint_exprl  = 
-  let recdefs = build_newrecursive fixpoint_exprl in 
+  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in 
   let _is_struct = 
     match fixpoint_exprl with 
-      | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] -> 
+      | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
+	      true
 	      register_built
 	      fixpoint_exprl 
 	      recdefs
 	      true
-	      false
 	  in 
-	  if register_built then register_wf name wf_rel wf_x args types body pre_hook;
+	  if register_built 
+	  then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
 	  false
-      | [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] -> 
+      | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
+	      true
 	      register_built
 	      fixpoint_exprl 
 	      recdefs
 	      true
-	      false
 	  in 
-	  if register_built then register_mes name wf_mes wf_x args types body pre_hook;
-	  false
+	  if register_built 
+	  then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook;
+	  true
       | _ -> 
 	  let fix_names = 
 	    List.map (function (name,_,_,_,_) -> name) fixpoint_exprl 
@@ -469,7 +503,9 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 		     in 
 		     let annot = 
 		       try Some (list_index (Name id) names - 1), Topconstr.CStructRec 
-		       with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) 
+		       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 -> 
@@ -479,10 +515,11 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 			 (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)
+		       (name,(Some 0, Topconstr.CStructRec),args,types,body),
+		     (None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
-		       ("Cannot use mutual definition with well-founded recursion")
+		       ("Cannot use mutual definition with well-founded recursion or measure")
 	      ) 
 	      (List.combine fixpoint_exprl recdefs)
 	  in
@@ -493,13 +530,13 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	  let is_rec = List.exists (is_rec fix_names) recdefs in
 	  if register_built then register_struct is_rec old_fixpoint_exprl;
 	  generate_principle
+	    false
 	    register_built
 	    fixpoint_exprl
 	    recdefs 
 	    interactive_proof
-	    true
 	    (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
-	  if register_built then derive_inversion  fix_names;
+	  if register_built then derive_inversion fix_names;
 	  true;
   in
   ()
@@ -517,9 +554,13 @@ let rec add_args id new_args b =
   | CArrow(loc,b1,b2) -> 
       CArrow(loc,add_args id new_args  b1, add_args id new_args b2)
   | CProdN(loc,nal,b1) -> 
-      CProdN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, add_args id new_args  b1)
+      CProdN(loc,
+	     List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, 
+	     add_args id new_args  b1)
   | CLambdaN(loc,nal,b1) -> 
-      CLambdaN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args  b2)) nal, add_args id new_args  b1)
+      CLambdaN(loc,
+	       List.map (fun (nal,b2) -> (nal,add_args id new_args  b2)) nal, 
+	       add_args id new_args  b1)
   | CLetIn(loc,na,b1,b2) -> 
       CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
   | CAppExpl(loc,(pf,r),exprl) -> 
@@ -530,10 +571,13 @@ let rec add_args id new_args b =
 	| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
       end
   | 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)
+      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,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 (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) -> 
@@ -558,7 +602,63 @@ let rec add_args id new_args b =
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
   | CDynamic _ -> anomaly "add_args : CDynamic"
+exception Stop of  Topconstr.constr_expr
+
+
+(* [chop_n_arrow n t] chops the [n] first arrows in [t] 
+   Acts on Topconstr.constr_expr 
+*)
+let rec chop_n_arrow n t = 
+  if n <= 0 
+  then t (* If we have already removed all the arrows then return the type *)
+  else (* If not we check the form of [t] *) 
+    match t with 
+      | Topconstr.CArrow(_,_,t) ->  (* If we have an arrow, we discard it and recall [chop_n_arrow] *)
+	  chop_n_arrow (n-1) t
+      | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : 
+					     either we need to discard more than the number of arrows contained
+					     in this product declaration then we just recall [chop_n_arrow] on
+					     the remaining number of arrow to chop and [t'] we discard it and 
+					     recall [chop_n_arrow], either this product contains more arrows 
+					     than the number we need to chop and then we return the new type
+					  *)
+	  begin 
+	    try 
+	      let new_n =
+		let rec aux (n:int) = function 
+		    [] -> n
+		| (nal,t'')::nal_ta' -> 
+		    let nal_l = List.length nal in 
+		    if n >= nal_l
+		    then 
+		      aux (n - nal_l) nal_ta'
+		    else 
+		      let new_t' = Topconstr.CProdN(dummy_loc,((snd (list_chop n nal)),t'')::nal_ta',t')
+		      in 
+		      raise (Stop new_t')
+		in
+		aux n nal_ta'
+	    in 
+	      chop_n_arrow new_n t'
+	    with Stop t -> t
+	  end
+      | _ -> anomaly "Not enough products"
+  
 
+let rec get_args b t : Topconstr.local_binder list * 
+    Topconstr.constr_expr * Topconstr.constr_expr = 
+  match b with 
+    | Topconstr.CLambdaN (loc, (nal_ta), b') -> 
+	begin
+	  let n = 
+	    (List.fold_left (fun n (nal,_) -> 
+			       n+List.length nal) 0 nal_ta )
+	  in
+	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in 
+	  (List.map (fun (nal,ta) -> 
+		       (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' 
+	end
+    | _ -> [],b,t
 
 
 let make_graph (f_ref:global_reference) =
@@ -578,68 +678,14 @@ let make_graph (f_ref:global_reference) =
 	let env = Global.env () in
 	let body = (force b) in
 	let extern_body,extern_type = 
-	  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;
-	  try 
-	    let res =  Constrextern.extern_constr false env body in 
-	    let res' = Constrextern.extern_type false env  c_body.const_type in 
-	    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;
-	    res,res'
-	  with
-	    | UserError(s,msg) as e -> 
-		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;
-		raise e
-	    | e -> 
-		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;
-		raise e
-	in
-	let rec get_args b t : Topconstr.local_binder list * 
-	    Topconstr.constr_expr * Topconstr.constr_expr = 
-(* 	  Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *)
-(* 	  Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *)
-(* 	  Pp.msgnl (fnl ()); *)
-	  match b with 
-	    | Topconstr.CLambdaN (loc, (nal_ta), b') -> 
-		begin
-		  let n = 
-		    (List.fold_left (fun n (nal,_) -> 
-				       n+List.length nal) 0 nal_ta )
-		  in
-		  let rec chop_n_arrow n t = 
-		    if n > 0 
-		    then 
-		      match t with 
-			| Topconstr.CArrow(_,_,t) -> chop_n_arrow (n-1) t 
-			| Topconstr.CProdN(_,nal_ta',t') -> 
-			    let n' = 
-			      List.fold_left 
-				(fun n (nal,t'') -> 
-				   n+List.length nal) n nal_ta' 
-			    in
-(* 			    assert (n'<= n);  *)
-			    chop_n_arrow (n - n') t'
-			| _ -> anomaly "Not enough products"
-		    else t
-		  in 
-		  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in 
-		  (List.map (fun (nal,ta) -> (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' 
-		end
-	    | _ -> [],b,t
+	  with_full_print 
+	    (fun () -> 
+	       (Constrextern.extern_constr false env body, 
+		Constrextern.extern_type false env
+                  (Typeops.type_of_constant_type env c_body.const_type)
+	       )
+	    )
+	    ()
 	in
 	let (nal_tas,b,t)  = get_args extern_body extern_type in
 	let expr_list = 
@@ -659,7 +705,8 @@ let make_graph (f_ref:global_reference) =
 			   )
 		       in 
 		       let rec_id = 
-			 match List.nth bl' (out_some n)  with |(_,Name id) -> id | _ -> anomaly ""
+			 match List.nth bl' (out_some n)  with 
+			   |(_,Name id) -> id | _ -> anomaly ""
 		       in
 		       let new_args = 
 			 List.flatten 
@@ -667,7 +714,10 @@ let make_graph (f_ref:global_reference) =
 			      (function
  				 | Topconstr.LocalRawDef (na,_)-> []
 			      	 | Topconstr.LocalRawAssum (nal,_) -> 
-				     List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
+				     List.map 
+				       (fun (loc,n) -> 
+					  CRef(Libnames.Ident(loc, Nameops.out_name n))) 
+				       nal
 			      )
 			      nal_tas
 			   )
@@ -685,7 +735,9 @@ let make_graph (f_ref:global_reference) =
 	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
+	List.iter 
+	  (fun (id,_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) 
+	  expr_list
 
 
 (* let make_graph _ = assert false	 *)
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index f41aac20..13b242d5 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -5,8 +5,8 @@ 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_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
+let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
 let mk_equation_id id = Nameops.add_suffix id "_equation"
 
 let msgnl m =
@@ -233,6 +233,32 @@ let get_proof_clean do_reduce =
   Pfedit.delete_current_proof ();
   result
 
+let with_full_print f a = 
+  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;
+  try 
+    let res = f a in 
+    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;
+    res
+  with  
+    | e -> 
+	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;
+	raise e
+
+
+
 
 
 
@@ -248,14 +274,18 @@ type function_info =
       rect_lemma : constant option;
       rec_lemma : constant option;
       prop_lemma : constant option;
+      is_general : bool; (* Has this function been defined using general recursive definition *)
     }
       
 
-type function_db  = function_info list
+(* type function_db  = function_info list *)
+
+(* let function_table = ref ([] : function_db) *)
 
-let function_table = ref ([] : function_db)
-  
 
+let from_function = ref Cmap.empty
+let from_graph = ref Indmap.empty
+(*
 let rec do_cache_info finfo = function 
   | [] -> raise Not_found 
   | (finfo'::finfos as l) -> 
@@ -274,6 +304,12 @@ let cache_Function (_,(finfos)) =
   in  
   if new_tbl != !function_table 
   then function_table := new_tbl
+*)
+
+let cache_Function (_,finfos) = 
+  from_function := Cmap.add finfos.function_constant finfos !from_function;
+  from_graph := Indmap.add finfos.graph_ind finfos !from_graph
+
 
 let load_Function _  = cache_Function
 let open_Function _ = cache_Function
@@ -307,6 +343,7 @@ let subst_Function (_,subst,finfos) =
       rect_lemma = rect_lemma' ;
       rec_lemma = rec_lemma';
       prop_lemma = prop_lemma';
+      is_general = finfos.is_general
     }
 
 let classify_Function (_,infos) = Libobject.Substitute infos
@@ -342,6 +379,7 @@ let discharge_Function (_,finfos) =
 	   rect_lemma = rect_lemma';
 	   rec_lemma = rec_lemma';
 	   prop_lemma = prop_lemma' ;
+	   is_general = finfos.is_general
 	 }    
 
 open Term
@@ -357,7 +395,8 @@ let pr_info f_info =
     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 = 
+let pr_table tb = 
+  let l = Cmap.fold (fun k v acc -> v::acc) tb [] in 
   Util.prlist_with_sep fnl pr_info l
 
 let in_Function,out_Function = 
@@ -376,17 +415,16 @@ let in_Function,out_Function =
 
 (* Synchronisation with reset *)
 let freeze () = 
-  let tbl = !function_table in 
-(*   Pp.msgnl (str "freezing function_table : " ++ pr_table tbl); *)
-  tbl
-
-let unfreeze l = 
+  !from_function,!from_graph
+let unfreeze (functions,graphs) = 
 (*   Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
-  function_table :=
- l
+  from_function := functions;
+  from_graph := graphs
+
 let init () = 
 (*   Pp.msgnl (str "reseting function_table");  *)
-  function_table := []
+  from_function := Cmap.empty;
+  from_graph := Indmap.empty
 
 let _ = 
   Summary.declare_summary "functions_db_sum"
@@ -405,18 +443,18 @@ let find_or_none id =
 
 
 let find_Function_infos f = 
-  List.find (fun finfo ->  finfo.function_constant = f) !function_table
+  Cmap.find f !from_function
 
 
 let find_Function_of_graph ind = 
-  List.find (fun finfo ->  finfo.graph_ind = ind) !function_table
+  Indmap.find ind !from_graph
   
 let update_Function finfo = 
 (*   Pp.msgnl (pr_info finfo); *)
   Lib.add_anonymous_leaf (in_Function finfo)
       
   
-let add_Function f = 
+let add_Function is_general 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) 
@@ -436,12 +474,14 @@ let add_Function f =
       rect_lemma = rect_lemma;
       rec_lemma = rec_lemma;
       prop_lemma = prop_lemma;
-      graph_ind = graph_ind
+      graph_ind = graph_ind;
+      is_general = is_general
+      
     }
   in
   update_Function finfos
 
-let pr_table () = pr_table !function_table
+let pr_table () = pr_table !from_function
 (*********************************)
 (* Debuging *)
 let function_debug = ref false 
@@ -464,3 +504,5 @@ let do_observe () =
       
       
     
+exception Building_graph of exn 
+exception Defining_principle of exn
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 00e1ce8d..7da1d6f0 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -73,6 +73,12 @@ val get_proof_clean : bool ->
     
 
 
+(* [with_full_print f a] applies [f] to [a] in full printing environment 
+   
+   This function preserves the print settings 
+*)
+val with_full_print : ('a -> 'b) -> 'a -> 'b
+
 
 (*****************)
 
@@ -86,12 +92,13 @@ type function_info =
       rect_lemma : constant option;
       rec_lemma : constant option;
       prop_lemma : constant option;
+      is_general : bool;
     }
 
 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 add_Function : bool -> constant -> unit
 
 val update_Function : function_info -> unit 
 
@@ -101,5 +108,10 @@ val pr_info : function_info -> Pp.std_ppcmds
 val pr_table : unit -> Pp.std_ppcmds
 
 
-val function_debug : bool ref 
+(* val function_debug : bool ref  *)
 val do_observe : unit -> bool
+
+(* To localize pb *)
+exception Building_graph of exn 
+exception Defining_principle of exn
+
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 00b5f28c..26a1066c 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -103,10 +103,28 @@ TACTIC EXTEND snewfunind
 END
 
 
+let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc
+
+ARGUMENT EXTEND constr_coma_sequence'
+  TYPED AS constr_list
+  PRINTED BY pr_constr_coma_sequence
+| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
+| [ constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+
+ARGUMENT EXTEND auto_using'
+  TYPED AS constr_list
+  PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence'(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
 VERNAC ARGUMENT EXTEND rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
-| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
-| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] 
+| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
+| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] 
 END
 
 
@@ -131,8 +149,8 @@ VERNAC ARGUMENT EXTEND rec_definition2
      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" 
+	   | 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
@@ -214,11 +232,17 @@ END
 (* FINDUCTION *)
 
 (* comment this line to see debug msgs *)
-(* let msg x = () ;; let pr_lconstr c = str "" *)
+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)
+let prNamedConstr s c = 
+  begin
+    msg(str "");
+    msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
+    msg(str "");
+  end
 
 
 
@@ -266,6 +290,55 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
     max_rel = max_rel; onlyvars = List.for_all isVar args } 
     ::subres
 
+let mkEq typ c1 c2 = 
+  mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|])
+
+
+let poseq_unsafe idunsafe cstr gl =
+  let typ = Tacmach.pf_type_of gl cstr in
+  tclTHEN
+    (Tactics.letin_tac true (Name idunsafe) cstr allClauses)
+    (tclTHENFIRST 
+      (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) 
+      Tactics.reflexivity)
+    gl
+  
+
+let poseq id cstr gl =
+  let x = Tactics.fresh_id [] id gl in
+  poseq_unsafe x cstr gl
+
+(* dirty? *)
+
+let list_constr_largs = ref []
+
+let rec poseq_list_ids_rec lcstr gl =
+  match lcstr with
+    | [] -> tclIDTAC gl
+    | c::lcstr' -> 
+	match kind_of_term c with
+	  | Var _ -> 
+	      (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
+	  | _ -> 
+	      let _ = prstr "c = " in
+	      let _ = prconstr c in
+	      let _ = prstr "\n" in
+	      let typ = Tacmach.pf_type_of gl c in
+	      let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in
+	      let x = Tactics.fresh_id [] cname gl in
+	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
+	      let _ = prstr " list_constr_largs = " in
+	      let _ = prlistconstr !list_constr_largs in
+	      let _ = prstr "\n" in
+
+	      tclTHEN
+		(poseq_unsafe x c)
+		(poseq_list_ids_rec lcstr')
+		gl
+
+let poseq_list_ids lcstr gl = 
+  let _ = list_constr_largs := [] in
+  poseq_list_ids_rec lcstr gl
 
 (** [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
@@ -296,11 +369,17 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
   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) 
+      (fun info ->
+	(tclTHEN
+	  (tclTHEN (poseq_list_ids info.largs)
+	    (
+	      fun gl -> 
+		  (functional_induction 
+		    true (applist (info.fname, List.rev !list_constr_largs)) 
+		    None IntroAnonymous) gl)) 
 	  nexttac)) ordered_info_list in
+  (* we try each (f t u v) until one does not fail *)
+  (* TODO: try also to mix functional schemes *)
   tclFIRST taclist g
 
 
@@ -313,9 +392,8 @@ 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
+	(* Default heuristic: put first occurrences 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
@@ -325,6 +403,7 @@ let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
 	List.sort ordering
 
 
+
 TACTIC EXTEND finduction
     ["finduction" ident(id) natural_opt(oi)] -> 
       [ 
@@ -353,3 +432,36 @@ TACTIC EXTEND fauto
 
 END
 
+
+TACTIC EXTEND poseq
+  [ "poseq" ident(x) constr(c) ] -> 
+      [ poseq x c ]
+END
+
+VERNAC COMMAND EXTEND Showindinfo
+  [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
+END
+
+VERNAC COMMAND EXTEND MergeFunind
+  [ "Mergeschemes" lconstr(c) "with" lconstr(c') "using" ident(id) ] -> 
+     [ 
+       let c1 = Constrintern.interp_constr Evd.empty (Global.env()) c in
+       let c2 = Constrintern.interp_constr Evd.empty (Global.env()) c' in
+       let id1,args1 = 
+	 try 
+	   let hd,args = destApp c1 in
+	   if Term.isInd hd then hd , args 
+	   else raise (Util.error "Ill-formed (fst) argument")
+	 with Invalid_argument _ 
+	     -> Util.error ("Bad argument form for merging schemes") in
+       let id2,args2 = 
+	 try
+ 	   let hd,args = destApp c2 in
+	   if isInd hd then hd , args 
+	   else raise (Util.error "Ill-formed (snd) argument")
+	 with Invalid_argument _ 
+	     -> Util.error ("Bad argument form for merging schemes") in
+       (* TOFO: enlever le ignore et declarer l'inductif *)
+       ignore(Merge.merge c1 c2 args1 args2 id)
+     ]
+END
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 084ec7e0..04110ea9 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -44,25 +44,6 @@ let pr_with_bindings prc prlc (c,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
 
@@ -120,7 +101,7 @@ let id_to_constr id =
 
 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 graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph))  in 
   let ctxt,_ = decompose_prod_assum graph_arity in 
   let fun_ctxt,res_type = 
     match ctxt with 
@@ -443,17 +424,17 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       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
+	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
 	     (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
 	  )
-	  ([],[])
+	  ([],pf_ids_of_hyps g)
 	  princ_infos.params
 	  (List.rev params)
       in
       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
+	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in 
 	     (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
@@ -471,7 +452,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	  (observe_tac "functional_induction" (
 	     fun g -> 
 	       observe
-		 (str "princ" ++ pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g))  (mkVar principle_id,bindings));
+		 (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
@@ -493,6 +474,31 @@ let generalize_depedent_of x hyp g =
     (pf_hyps g)
     g
 
+
+
+
+
+
+let rec reflexivity_with_destruct_cases g = 
+  let destruct_case () = 
+    try 
+      match kind_of_term (snd (destApp (pf_concl g))).(2) with 
+	| Case(_,_,v,_) -> 
+	    tclTHENSEQ[
+	      h_case (v,Rawterm.NoBindings);
+	      intros;
+	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases 
+	    ]
+	| _ -> reflexivity
+    with _ -> reflexivity
+  in
+  tclFIRST
+    [ reflexivity;
+      destruct_case ()
+    ]
+    g
+
+
 (* [prove_fun_complete funs graphs schemes lemmas_types_infos i] 
    is the tactic used to prove completness lemma. 
    
@@ -567,11 +573,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let rewrite_tac j ids : tactic = 
       let graph_def = graphs.(j) in 
-      if Rtree.is_infinite graph_def.mind_recargs
+      let infos =  try find_Function_infos (destConst funcs.(j)) with Not_found ->  error "No graph found" in 
+      if infos.is_general ||  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"
+	  try out_some (infos).equation_lemma
+	  with Failure "out_some"  -> anomaly "Cannot find equation lemma"
 	in 
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
@@ -677,8 +684,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
         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)
+	(* The proof is (almost) complete *)
+        observe_tac "reflexivity" (reflexivity_with_destruct_cases)
       ]
 	g
     in
@@ -758,7 +765,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (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));
+	 Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in 
 	 update_Function
@@ -968,10 +975,17 @@ let invfun qhyp f g =
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" -> 
-			     errorlabstrm "" (Ppconstr.pr_id hid ++ str " must contain at leat one function")
+			     errorlabstrm "" (str "Hypothesis" ++ 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" 
+			     if do_observe () 
+			     then
+			       error "Cannot use equivalence with graph for any side of the equality"
+			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			 | Not_found -> 
+			     if do_observe () 
+			     then
+			       error "No graph found for any side of equality" 
+			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 		   end
 	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
 	  )
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
new file mode 100644
index 00000000..1b796a81
--- /dev/null
+++ b/contrib/funind/merge.ml
@@ -0,0 +1,826 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* Merging of induction principles. *)
+
+(*i $Id: i*)
+
+open Util
+open Topconstr
+open Vernacexpr
+open Pp
+open Names
+open Term
+open Declarations
+open Environ
+open Rawterm
+open Rawtermops
+
+(** {1 Utilities}  *)
+
+(** {2 Useful operations on constr and rawconstr} *)
+
+(** Substitutions in constr *)
+let compare_constr_nosub t1 t2 =
+  if compare_constr (fun _ _ -> false) t1 t2 
+  then true
+  else false
+
+let rec compare_constr' t1 t2 =
+  if compare_constr_nosub t1 t2 
+  then true
+  else (compare_constr (compare_constr') t1 t2)
+
+let rec substitterm prof t by_t in_u =
+  if (compare_constr' (lift prof t) in_u)
+  then (lift prof by_t)
+  else map_constr_with_binders succ 
+    (fun i -> substitterm i t by_t) prof in_u
+
+let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
+
+let understand = Pretyping.Default.understand Evd.empty (Global.env())
+
+(** Operations on names and identifiers *)
+let id_of_name = function
+    Anonymous -> id_of_string "H"
+  | Name id   -> id;;
+let name_of_string str = Name (id_of_string str)
+let string_of_name nme = string_of_id (id_of_name nme)
+
+(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
+let isVarf f x = 
+    match x with
+      | RVar (_,x) -> Pervasives.compare x f = 0 
+      | _ -> false
+
+(** [ident_global_exist id] returns true if identifier [id] is linked
+    in global environment. *)
+let ident_global_exist id = 
+  try 
+    let ans = CRef (Libnames.Ident (dummy_loc,id)) in
+    let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
+    true
+  with _ -> false 
+
+(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
+    global env) with base [id]. *)
+let next_ident_fresh (id:identifier) = 
+    let res = ref id in
+    while ident_global_exist !res do res := Nameops.lift_ident !res done;
+    !res
+
+
+(** {2 Debugging} *)
+(* 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)
+let prconstrnl c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+let prNamedConstr s c = 
+  begin
+    msg(str "");
+    msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} ");
+    msg(str "");
+  end
+let prNamedRConstr s c = 
+  begin
+    msg(str "");
+    msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} ");
+    msg(str "");
+  end
+let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
+let prNamedLConstr s lc = 
+  begin
+    prstr "[§§§ ";
+    prstr s;
+    prNamedLConstr_aux lc;
+    prstr " §§§]\n";
+  end
+let prNamedLDecl s lc = 
+  begin
+    prstr s; prstr "\n";
+    List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc;
+    prstr "\n";
+  end
+
+let showind (id:identifier) =
+  let cstrid = Tacinterp.constr_of_id (Global.env()) id in
+  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
+  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
+  List.iter (fun (nm, optcstr, tp) -> 
+    print_string (string_of_name nm^":");
+    prconstr tp; print_string "\n") 
+    ib1.mind_arity_ctxt;
+  (match ib1.mind_arity with
+    | Monomorphic x ->
+        Printf.printf "arity :"; prconstr x.mind_user_arity
+    | Polymorphic x -> 
+        Printf.printf "arity : universe?");
+  Array.iteri 
+    (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
+    ib1.mind_user_lc
+
+(** {2 Misc} *)
+
+exception Found of int
+
+(* Array scanning *)
+let array_find (arr: 'a array) (pred: int -> 'a -> bool): int option = 
+  try
+    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
+    None
+  with Found i -> Some i
+
+let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
+  try
+    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
+    Array.length arr (* all elt are positive *)
+  with Found i -> i
+
+let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a = 
+  let i = ref 0 in 
+  Array.fold_left 
+    (fun acc x -> 
+      let res = f !i acc x in i := !i + 1; res)
+    acc arr
+
+(* Like list_chop but except that [i] is the size of the suffix of [l]. *)
+let list_chop_end i l =
+  let size_prefix = List.length l -i in
+  if size_prefix < 0 then failwith "list_chop_end"
+  else list_chop size_prefix l
+
+let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a = 
+  let i = ref 0 in 
+  List.fold_left 
+    (fun acc x -> 
+      let res = f !i acc x in i := !i + 1; res)
+    acc arr
+
+let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list = 
+  let i = ref 0 in 
+  List.filter (fun x -> let res = f !i x in i := !i + 1; res) l
+
+
+(** Iteration module *)
+module For = 
+struct
+  let rec map i j (f: int -> 'a)  = if i>j then [] else f i :: (map (i+1) j f)
+  let rec foldup i j (f: 'a -> int -> 'a) acc = 
+    if i>j then acc else let newacc = f acc i in foldup (i+1) j f newacc
+  let rec folddown i j (f: 'a -> int -> 'a) acc = 
+    if i>j then acc else let newacc = f acc j in folddown i (j-1) f newacc
+  let fold i j = if i<j then foldup i j else folddown i j
+end
+
+
+(** {1 Parameters shifting and linking information} *)
+
+(** This type is used to deal with debruijn linked indices. When a
+    variable is linked to a previous one, we will ignore it and refer
+    to previous one. *)
+type linked_var =
+    | Linked of int
+    | Unlinked
+    | Funres
+
+(** When merging two graphs, parameters may become regular arguments,
+    and thus be shifted. This type describe the result of computing
+    the changes. *)
+type 'a shifted_params =
+    {
+      nprm1:'a;
+      nprm2:'a;
+      prm2_unlinked:'a list; (* ranks of unlinked params in nprms2 *)
+      nuprm1:'a;
+      nuprm2:'a;
+      nargs1:'a;
+      nargs2:'a;
+    }
+
+
+let prlinked x =
+  match x with
+    | Linked i -> Printf.sprintf "Linked %d" i
+    | Unlinked -> Printf.sprintf "Unlinked"
+    | Funres -> Printf.sprintf "Funres"
+
+let linkmonad f lnkvar = 
+  match lnkvar with
+    | Linked i -> Linked (f i)
+    | Unlinked -> Unlinked
+    | Funres -> Funres
+
+let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar
+
+(* This map is used to deal with debruijn linked indices. *)
+module Link = Map.Make (struct type t = int let compare = Pervasives.compare end)
+
+let pr_links l = 
+  Printf.printf "links:\n";
+  Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l;
+  Printf.printf "_____________\n"
+
+type 'a merged_arg =
+    | Prm_stable of 'a
+    | Prm_linked of 'a
+    | Prm_arg of 'a
+    | Arg_stable of 'a
+    | Arg_linked of 'a
+    | Arg_funres
+
+type merge_infos =
+    {
+      ident:identifier; (* new inductive name *)
+      mib1: mutual_inductive_body;
+      oib1: one_inductive_body; 
+      mib2: mutual_inductive_body;
+      oib2: one_inductive_body; 
+      (* Array of links of the first inductive (should be all stable) *)
+      lnk1: int merged_arg array;
+      (* Array of links of the second inductive (point to the first ind param/args) *)
+      lnk2: int merged_arg array;
+      (* number of rec params of ind1 which remai rec param in merge *)
+      nrecprms1: int;
+      (* number of other rec params of ind1 (which become non parm) *)
+      notherprms1:int;
+      (* number of functional result params of ind2 (which become non parm) *)
+      nfunresprms1:int;
+      (* list of decl of rec parms from ind1 which remain parms *)
+      recprms1: rel_declaration list;
+      (* List of other rec parms from ind1 *)
+      otherprms1: rel_declaration list; (* parms that became args *)
+      funresprms1: rel_declaration list; (* parms that are functional result args *)
+      (* number of rec params of ind2 which remain rec param in merge (and not linked) *)
+      nrecprms2: int;
+      (* number of other params of ind2 (which become non rec parm) *)
+      notherprms2:int;
+      (* number of functional result params of ind2 (which become non parm) *)
+      nfunresprms2:int;
+      (* list of decl of rec parms from ind2 which remain parms (and not linked) *)
+      recprms2: rel_declaration list;
+      (* List of other rec parms from ind2 (which are linked or become non parm) *)
+      otherprms2: rel_declaration list;      
+      funresprms2: rel_declaration list; (* parms that are functional result args *)
+    }
+
+
+let pr_merginfo x =
+  let i,s=
+    match x with 
+      | Prm_linked i -> Some i,"Prm_linked"
+      | Arg_linked i -> Some i,"Arg_linked"
+      | Prm_stable i -> Some i,"Prm_stable"
+      | Prm_arg i -> Some i,"Prm_arg"
+      | Arg_stable i -> Some i,"Arg_stable"
+      | Arg_funres -> None , "Arg_funres" in
+  match i with
+    | Some i -> Printf.sprintf "%s(%d)" s i
+    | None -> Printf.sprintf "%s" s
+
+let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false
+
+let isArg_stable x = match x with Arg_stable _ -> true | _ -> false
+
+let isArg_funres x = match x with Arg_funres -> true | _ -> false
+
+let filter_shift_stable (lnk:int merged_arg array) (l:'a list): 'a list =
+  let prms = list_filteri (fun i _ -> isPrm_stable lnk.(i)) l in
+  let args = list_filteri (fun i _ -> isArg_stable lnk.(i)) l in
+  let fres = list_filteri (fun i _ -> isArg_funres lnk.(i)) l in
+  prms@args@fres
+
+(** Reverse the link map, keeping only linked vars, elements are list
+    of int as several vars may be linked to the same var. *)
+let revlinked lnk =
+  For.fold 0 (Array.length lnk - 1)
+    (fun acc k -> 
+      match lnk.(k) with 
+        | Unlinked | Funres -> acc 
+        | Linked i -> 
+            let old = try Link.find i acc with Not_found -> [] in
+            Link.add i (k::old) acc)
+    Link.empty
+
+let array_switch arr i j = 
+  let aux = arr.(j) in arr.(j) <- arr.(i); arr.(i) <- aux
+
+let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list =
+  let larr = Array.of_list l in
+  let _ =
+    Array.iteri
+      (fun j x -> 
+        match x with
+          | Prm_linked i -> array_switch larr i j
+          | Arg_linked i -> array_switch larr i j
+          | Prm_stable i -> ()
+          | Prm_arg i -> ()
+          | Arg_stable i -> ()
+          | Arg_funres -> ()
+      ) lnk in
+  filter_shift_stable lnk (Array.to_list larr)
+
+
+
+
+(** {1 Utilities for merging} *)
+
+let ind1name = id_of_string "__ind1"
+let ind2name = id_of_string "__ind2"
+
+(** Performs verifications on two graphs before merging: they must not
+    be co-inductive, and for the moment they must not be mutual
+    either. *)
+let verify_inds mib1 mib2 =
+  if not mib1.mind_finite then error "First argument is coinductive";
+  if not mib2.mind_finite then error "Second argument is coinductive";
+  if mib1.mind_ntypes <> 1 then error "First argument is mutual";
+  if mib2.mind_ntypes <> 1 then error "Second argument is mutual";
+  ()
+
+
+(** {1 Merging function graphs} *)
+
+(** [shift_linked_params mib1 mib2 lnk] Computes which parameters (rec
+    uniform and ordinary ones) of mutual inductives [mib1] and [mib2]
+    remain uniform when linked by [lnk]. All parameters are
+    considered, ie we take parameters of the first inductive body of
+    [mib1] and [mib2].
+    
+    Explanation: The two inductives have parameters, some of the first
+    are recursively uniform, some of the last are functional result of
+    the functional graph.
+
+   (I x1 x2 ... xk ... xk' ... xn)
+   (J y1 y2 ... xl ... yl' ... ym)
+
+   Problem is, if some rec unif params are linked to non rec unif
+   ones, they become non rec (and the following too). And functinal
+   argument have to be shifted at the end *)
+let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id =
+  let linked_targets = revlinked lnk2 in
+  let is_param_of_mib1 x = x < mib1.mind_nparams_rec in
+  let is_param_of_mib2 x = x < mib2.mind_nparams_rec in
+  let is_targetted_by_non_recparam_lnk1 i = 
+    try 
+      let targets = Link.find i linked_targets in 
+      List.exists (fun x -> not (is_param_of_mib2 x)) targets
+    with Not_found -> false in
+  let mlnk1 = 
+    Array.mapi
+      (fun i lkv -> 
+        let isprm = is_param_of_mib1 i in
+        let prmlost = is_targetted_by_non_recparam_lnk1 i in
+        match isprm , prmlost, lnk1.(i) with
+          | true , true , _ -> Prm_arg i (* recparam becoming ordinary *)
+          | true , false , _-> Prm_stable i (* recparam remains recparam*)
+          | false , false , Funres -> Arg_funres
+          | _ , _ , Funres -> assert false (* fun res cannot be a rec param or lost *)
+          | false , _ , _ -> Arg_stable i) (* Args of lnk1 are not linked *)
+      lnk1 in
+  let mlnk2 = 
+    Array.mapi
+      (fun i lkv -> 
+        (* Is this correct if some param of ind2 is lost? *)
+        let isprm = is_param_of_mib2 i in
+        match isprm , lnk2.(i) with
+          | true , Linked j when not (is_param_of_mib1 j) -> 
+              Prm_arg j (* recparam becoming ordinary *)
+          | true , Linked j -> Prm_linked j (*recparam linked to recparam*)
+          | true , Unlinked -> Prm_stable i (* recparam remains recparam*)
+          | false , Linked j -> Arg_linked j (* Args of lnk2 lost *)
+          | false , Unlinked -> Arg_stable i (* Args of lnk2 remains *)
+          | false , Funres -> Arg_funres
+          | true , Funres -> assert false (* fun res cannot be a rec param *)
+      )
+      lnk2 in
+  let oib1 = mib1.mind_packets.(0) in
+  let oib2 = mib2.mind_packets.(0) in
+  (* count params remaining params *)
+  let n_params1 = array_prfx mlnk1 (fun i x -> not (isPrm_stable x)) in
+  let n_params2 = array_prfx mlnk2 (fun i x -> not (isPrm_stable x)) in
+  let bldprms arity_ctxt mlnk = 
+    list_fold_lefti
+      (fun i (acc1,acc2,acc3) x -> 
+        match mlnk.(i) with
+          | Prm_stable _ -> x::acc1 , acc2 , acc3
+          | Prm_arg _ | Arg_stable _ -> acc1 , x::acc2 , acc3
+          | Arg_funres -> acc1 , acc2 , x::acc3
+          | _ -> acc1 , acc2 , acc3) (* Prm_linked and Arg_xxx = forget it *)
+      ([],[],[]) arity_ctxt in
+  let recprms1,otherprms1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
+  let recprms2,otherprms2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
+  {
+    ident=id;
+    mib1=mib1;
+    oib1 = oib1;
+    mib2=mib2;
+    oib2 = oib2;
+    lnk1 = mlnk1;
+    lnk2 = mlnk2;
+    nrecprms1 = n_params1;
+    recprms1 = recprms1;
+    otherprms1 = otherprms1;
+    funresprms1 = funresprms1;
+    notherprms1 = Array.length mlnk1 - n_params1;
+    nfunresprms1 = List.length funresprms1;
+    nrecprms2 = n_params2;
+    recprms2 = recprms2;
+    otherprms2 = otherprms2;
+    funresprms2 = funresprms2;
+    notherprms2 = Array.length mlnk2 - n_params2;
+    nfunresprms2 = List.length funresprms2;
+  }
+
+
+
+
+(** {1 Merging functions} *)
+
+exception NoMerge
+
+(* lnk is an link array of *all* args (from 1 and 2) *)
+let merge_app c1 c2 id1 id2 shift filter_shift_stable = 
+  let lnk = Array.append shift.lnk1 shift.lnk2 in
+  match c1 , c2 with
+    | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> 
+        let args = filter_shift_stable lnk (arr1 @ arr2) in
+        RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args)
+    | RApp(_,f1, arr1), RApp(_,f2,arr2)  -> raise NoMerge
+    | _ -> raise NoMerge
+
+let merge_app_unsafe c1 c2 shift filter_shift_stable = 
+  let lnk = Array.append shift.lnk1 shift.lnk2 in
+  match c1 , c2 with
+    | RApp(_,f1, arr1), RApp(_,f2,arr2) -> 
+        let args = filter_shift_stable lnk (arr1 @ arr2) in
+        RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args)
+    | _ -> raise NoMerge
+
+
+
+(* Heuristic when merging two lists of hypothesis: merge every rec
+   calls of nrach 1 with all rec calls of branch 2. *)
+(* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
+let onefoud = ref false (* Ugly *)
+
+let rec merge_rec_hyps shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list) 
+    filter_shift_stable =
+  match ltyp with
+    | [] -> []
+    | (nme,(RApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> 
+        let _ = onefoud := true in
+        let rechyps = 
+          List.map 
+            (fun (nme,ind) -> 
+              match ind with
+                | RApp(_,i,args) -> 
+                    nme, merge_app_unsafe ind t shift filter_shift_stable
+                | _ -> assert false)
+            accrec in
+        rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
+    | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
+
+
+let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift = 
+  List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
+
+
+let find_app (nme:identifier) (ltyp: (name * rawconstr) list) = 
+  try
+    ignore
+      (List.map
+          (fun x -> 
+            match x with
+              | _,(RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+              | _ -> ())
+          ltyp);
+    false
+  with Found _ -> true
+        
+let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list)
+    concl1 (ltyp2:(name * rawconstr) list) concl2
+    : (name * rawconstr) list * rawconstr = 
+  let _ = prstr "MERGE_TYPES\n" in
+  let _ = prstr "ltyp 1 : " in
+  let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp1 in
+  let _ = prstr "\nltyp 2 : " in
+  let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp2 in
+  let _ = prstr "\n" in
+
+
+  let res =
+    match ltyp1 with
+      | [] -> 
+          let isrec1 = (accrec1<>[]) in
+          let isrec2 = find_app ind2name ltyp2 in
+          let _ = if isrec2 then prstr "  ISREC2 TRUE" else prstr "  ISREC2 FALSE" in
+          let _ = if isrec1 then prstr "  ISREC1 TRUE\n" else prstr "  ISREC1 FALSE\n" in
+          let rechyps =
+            if isrec1 && isrec2 
+            then merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable
+            else if isrec1 
+                (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *)
+            then merge_rec_hyps shift accrec1 (ltyp2@[name_of_string "concl2",concl2])
+              filter_shift_stable
+            else if isrec2
+            then merge_rec_hyps shift [name_of_string "concl1",concl1] ltyp2
+              filter_shift_stable_right
+            else [] in
+          let _ = prstr"\nrechyps : " in
+          let _ = List.iter 
+            (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) rechyps in
+          let _ = prstr "MERGE CONCL :  " in
+          let _ = prNamedRConstr "concl1" concl1 in
+          let _ = prstr " with " in
+          let _ = prNamedRConstr "concl2" concl2 in
+          let _ = prstr "\n" in
+          let concl = 
+            merge_app concl1 concl2 ind1name ind2name shift filter_shift_stable in
+          let _ = prstr "FIN " in
+          let _ = prNamedRConstr "concl" concl in
+          let _ = prstr "\n" in
+          rechyps , concl
+      | (nme,t1)as e ::lt1 -> 
+          match t1 with
+            | RApp(_,f,carr) when isVarf ind1name f -> 
+                merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 
+            | _ -> 
+                let recres, recconcl2 =
+                  merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
+                ((nme,t1) :: recres) , recconcl2
+  in
+  res
+
+
+(** [build_link_map_aux allargs1 allargs2 shift] returns the mapping of
+    linked args [allargs2] to target args of [allargs1] as specified
+    in [shift]. [allargs1] and [allargs2] are in reverse order.  Also
+    returns the list of unlinked vars of [allargs2]. *)
+let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
+    (lnk:int merged_arg array) =
+  array_fold_lefti
+    (fun i acc e -> 
+      if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *)
+      else 
+        match e with 
+          | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc
+          | _ -> acc)
+    Idmap.empty lnk
+
+let build_link_map allargs1 allargs2 lnk =
+  let allargs1 =
+    Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs1)) in
+  let allargs2 =
+    Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs2)) in
+  build_link_map_aux allargs1 allargs2 lnk
+
+
+(** [merge_one_constructor lnk shift typcstr1 typcstr2] merges the two
+    constructor rawtypes [typcstr1] and [typcstr2].  [typcstr1] and
+    [typcstr2] contain all parameters (including rec. unif. ones) of
+    their inductive.
+
+    if  [typcstr1] and [typcstr2] are of the form:
+
+    forall recparams1, forall ordparams1, H1a -> H2a... (I1 x1 y1 ... z1)
+    forall recparams2, forall ordparams2, H2b -> H2b... (I2 x2 y2 ... z2)
+
+    we build:
+
+    forall recparams1 (recparams2 without linked params),
+     forall ordparams1 (ordparams2 without linked params),
+      H1a' -> H2a' -> ...  -> H2a' -> H2b' -> ... 
+        -> (newI x1 ... z1 x2 y2 ...z2 without linked params)
+
+    where Hix' have been adapted, ie: 
+      - linked vars have been changed,
+      - rec calls to I1 and I2 have been replaced by rec calls to
+        newI. More precisely calls to I1 and I2 have been merge by an
+        experimental heuristic (in particular if n o rec calls for I1
+        or I2 is found, we use the conclusion as a rec call). See
+        [merge_types] above.
+
+    Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint.
+
+    TODO: return nothing if equalities (after linking) are contradictory. *)
+let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
+    (typcstr2:rawconstr) : rawconstr =
+  (* FIXME: les noms des parametres corerspondent en principe au
+     parametres du niveau mib, mais il faudrait s'en assurer *)
+  (* shift.nfunresprmsx last args are functional result *)
+  let nargs1 = 
+    shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in
+  let nargs2 =
+    shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in
+  let allargs1,rest1 = raw_decompose_prod_n nargs1 typcstr1 in
+  let allargs2,rest2 = raw_decompose_prod_n nargs2 typcstr2 in  
+  (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *)
+  let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in
+  let rest2 = change_vars linked_map rest2 in
+  let hyps1,concl1 = raw_decompose_prod rest1 in
+  let hyps2,concl2' = raw_decompose_prod rest2 in
+  let ltyp,concl2 = 
+    merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
+  let typ = raw_compose_prod concl2 (List.rev ltyp) in
+  let revargs1 = 
+    list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in
+  let revargs2 = 
+    list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in
+  let typwithprms = raw_compose_prod typ (List.rev revargs2 @ List.rev revargs1) in
+  typwithprms
+
+
+(** constructor numbering *)
+let fresh_cstror_suffix , cstror_suffix_init =
+  let cstror_num = ref 0 in
+  (fun () -> 
+    let res = string_of_int !cstror_num in
+    cstror_num := !cstror_num + 1;
+    res) ,
+  (fun () -> cstror_num := 0)
+
+(** [merge_constructor_id id1 id2 shift] returns the identifier of the
+    new constructor from the id of the two merged constructor and
+    the merging info. *)
+let merge_constructor_id id1 id2 shift:identifier = 
+  let id = string_of_id shift.ident ^ "_" ^ fresh_cstror_suffix () in
+  next_ident_fresh (id_of_string id)
+
+
+
+(** [merge_constructors lnk shift avoid] merges the two list of
+    constructor [(name*type)]. These are translated to rawterms
+    first, each of them having distinct var names. *)
+let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
+    (typcstr1:(identifier * types) list) 
+    (typcstr2:(identifier * types) list) : (identifier * rawconstr) list =
+  List.flatten 
+    (List.map
+        (fun (id1,typ1) -> 
+          let typ1 = substitterm 0 (mkRel 1) (mkVar ind1name) typ1 in
+          let rawtyp1 = Detyping.detype false (Idset.elements avoid) [] typ1 in
+          let idsoftyp1:Idset.t = ids_of_rawterm rawtyp1 in
+          List.map
+            (fun (id2,typ2) -> 
+              let typ2 = substitterm 0 (mkRel 1) (mkVar ind2name) typ2 in
+              (* Avoid also rawtyp1 names *)
+              let avoid2 = Idset.union avoid idsoftyp1 in
+              let rawtyp2 = Detyping.detype false (Idset.elements avoid2) [] typ2 in
+              let typ = merge_one_constructor shift rawtyp1 rawtyp2 in
+              let newcstror_id = merge_constructor_id id1 id2 shift in
+              newcstror_id , typ)
+            typcstr2)
+        typcstr1)
+    
+(** [merge_inductive_body lnk shift avoid oib1 oib2] merges two
+    inductive bodies [oib1] and [oib2], linking with [lnk], params
+    info in [shift], avoiding identifiers in [avoid]. *)
+let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
+    (oib2:one_inductive_body) : (identifier * rawconstr) list =
+  let lcstr1 = Array.to_list oib1.mind_user_lc in
+  let lcstr2 = Array.to_list oib2.mind_user_lc in
+  let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
+  let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
+  cstror_suffix_init();
+  merge_constructors shift avoid lcstr1 lcstr2
+
+(** [build_raw_params prms_decl avoid] returns a list of variables
+    attributed to the list of decl [prms_decl], avoiding names in
+    [avoid]. *)
+let build_raw_params prms_decl avoid =
+  let dummy_constr = compose_prod prms_decl mkProp in
+  let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in
+  let res,_ = raw_decompose_prod dummy_rawconstr in
+  res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr)))
+
+(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual
+    inductive bodies [mib1] and [mib2] linking vars with
+    [lnk]. [shift] information on parameters of the new inductive.
+    For the moment, inductives are supposed to be non mutual.
+*)
+let rec merge_mutual_inductive_body
+    (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) 
+    (shift:merge_infos) =
+  (* Mutual not treated, we take first ind body of each. *)
+  let nprms1 = mib1.mind_nparams_rec in (* n# of rec uniform parms of mib1 *)
+  let prms1 = (* rec uniform parms of mib1 *)
+    List.map (fun (x,_,y) -> x,y) (fst (list_chop nprms1 mib1.mind_params_ctxt)) in
+
+  (* useless: *)
+  let prms1_named,avoid' = build_raw_params prms1 [] in
+  let prms2_named,avoid = build_raw_params prms1 avoid' in
+  let avoid:Idset.t = List.fold_right Idset.add avoid Idset.empty in  
+  (* *** *)
+
+  merge_inductive_body shift avoid mib1.mind_packets.(0) mib2.mind_packets.(0) 
+
+  
+
+let merge_rec_params_and_arity params1 params2 shift (concl:constr) = 
+  let params = shift.recprms1 @ shift.recprms2 in
+  let resparams, _ =
+    List.fold_left
+      (fun (acc,env) (nme,_,tp) -> 
+        let typ = Constrextern.extern_constr false env tp in
+        let newenv = Environ.push_rel (nme,None,tp) env in
+        LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc , newenv)
+      ([],Global.env())
+      params in
+  let concl = Constrextern.extern_constr false (Global.env()) concl in
+  let arity,_ = 
+    List.fold_left 
+      (fun (acc,env) (nm,_,c) -> 
+        let typ = Constrextern.extern_constr false env c in
+        let newenv = Environ.push_rel (nm,None,c) env in
+        CProdN (dummy_loc, [[(dummy_loc,nm)],typ] , acc) , newenv)
+      (concl,Global.env())
+      (shift.otherprms1@shift.otherprms2@shift.funresprms1@shift.funresprms2) in  
+  resparams,arity
+
+  
+
+(** [rawterm_list_to_inductive_expr ident rawlist] returns the
+    induct_expr corresponding to the the list of constructor types
+    [rawlist], named ident.
+    FIXME: params et cstr_expr (arity) *)
+let rawterm_list_to_inductive_expr mib1 mib2 shift
+    (rawlist:(identifier * rawconstr) list):inductive_expr =
+  let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *)
+    Options.with_option Options.raw_print (Constrextern.extern_rawtype Idset.empty) x in
+  let lident = dummy_loc, shift.ident in
+  let bindlist , cstr_expr = (* params , arities *)
+    merge_rec_params_and_arity 
+      mib1.mind_params_ctxt mib2.mind_params_ctxt shift mkSet in
+  let lcstor_expr : (bool * (lident * constr_expr)) list  = 
+    List.map (* zeta_normalize t ? *)
+      (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
+      rawlist in  
+  lident , bindlist , cstr_expr , lcstor_expr
+
+(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
+    variables specified in [lnk]. Graphs are not supposed to be mutual
+    inductives for the moment. *)
+let merge_inductive (ind1: inductive) (ind2: inductive) 
+    (lnk1: linked_var array) (lnk2: linked_var array) id =
+  let env = Global.env() in
+  let mib1,_ = Inductive.lookup_mind_specif env ind1 in
+  let mib2,_ = Inductive.lookup_mind_specif env ind2 in
+  let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *)
+  (* compute params that become ordinary args (because linked to ord. args) *)
+  let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in
+  let rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
+  let indexpr = rawterm_list_to_inductive_expr mib1 mib2 shift_prm rawlist in
+  (* Declare inductive *)
+  Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
+
+
+
+let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array) id =
+  let env = Global.env() in
+  let ind1,_cstrlist1 = Inductiveops.find_inductive env Evd.empty cstr1 in
+  let ind2,_cstrlist2 = Inductiveops.find_inductive env Evd.empty cstr2 in
+  let lnk1 = (* args1 are unlinked. FIXME? mergescheme (G x x) ?? *)
+    Array.mapi (fun i c -> Unlinked) args1 in
+  let _ = lnk1.(Array.length lnk1 - 1) <- Funres in (* last arg is functional result *)
+  let lnk2 = (* args2 may be linked to args1 members. FIXME: same 
+                as above: vars may be linked inside args2?? *)
+    Array.mapi
+      (fun i c -> 
+        match array_find args1 (fun i x -> x=c) with
+          | Some j -> Linked j
+          | None -> Unlinked) 
+      args2 in
+  let _ = lnk2.(Array.length lnk2 - 1) <- Funres in (* last arg is functional result *)
+  let resa = merge_inductive ind1 ind2 lnk1 lnk2 id in
+  resa
+
+
+
+
+
+(* @article{ bundy93rippling,
+    author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill",
+    title = "Rippling: A Heuristic for Guiding Inductive Proofs",
+    journal = "Artificial Intelligence",
+    volume = "62",
+    number = "2",
+    pages = "185-253",
+    year = "1993",
+    url = "citeseer.ist.psu.edu/bundy93rippling.html" }
+
+ *)
+(* 
+*** Local Variables: ***
+*** compile-command: "make -C ../.. contrib/funind/merge.cmo" ***
+*** indent-tabs-mode: nil ***
+*** End: ***
+*)
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index dbf2f944..aca84f06 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -789,7 +789,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	    avoid
 	    matched_expr
 	in
-	(* We know create the precondition of this branch i.e.
+	(* We now 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 ...)
@@ -1074,8 +1074,8 @@ let rec rebuild_return_type rt =
     | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None))
 
 
-let build_inductive 
-    parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list)  
+let do_build_inductive 
+    funnames (funsargs: (Names.name * rawconstr * bool) list list)  
     returned_types 
     (rtl:rawconstr list) =
   let _time1 = System.get_time () in
@@ -1085,7 +1085,7 @@ let build_inductive
   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 rtl_alpha = List.map (function rt ->  expand_as (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
@@ -1108,19 +1108,7 @@ let build_inductive
       (function result (* (args',concl') *) -> 
 	 let rt = compose_raw_context result.context result.value in 
 	 let nb_args = List.length funsargs.(i) 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 *)
-(* 	   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; *)
+	 (*  with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
 	 fst (
 	   rebuild_cons nb_args relnames.(i)
 	     []
@@ -1145,12 +1133,7 @@ let build_inductive
   in
   let rel_constructors = Array.mapi rel_constructors resa in
   (* Computing the set of parameters if asked *)
-  let rels_params = 
-    if parametrize 
-    then
-      compute_params_name relnames_as_set funsargs  rel_constructors 
-    else []
-  in
+  let rels_params = compute_params_name relnames_as_set funsargs  rel_constructors in
   let nrel_params = List.length rels_params in
   let rel_constructors = (* Taking into account the parameters in constructors *)
     Array.map (List.map 
@@ -1182,8 +1165,6 @@ let build_inductive
      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;
   let rel_params =  
     List.map 
       (fun (n,t,is_defined) -> 
@@ -1199,16 +1180,19 @@ let build_inductive
   let ext_rels_constructors = 
     Array.map (List.map 
       (fun (id,t) -> 
-	 false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty ((* zeta_normalize *) t))
+	 false,((dummy_loc,id),
+		Options.with_option
+		  Options.raw_print
+		  (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t)
+	       )
       ))
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors = 
-    (dummy_loc,relnames.(i)),
-    None,
+    ((dummy_loc,relnames.(i)),
     rel_params,
     rel_arities.(i),
-    ext_rel_constructors
+    ext_rel_constructors),None
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
   let rel_inds = Array.to_list ext_rel_constructors in 
@@ -1232,58 +1216,36 @@ let build_inductive
 (* 	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
-  Impargs.make_implicit_args false;
-  Impargs.make_strict_implicit_args false;
-  Impargs.make_contextual_implicit_args false;
   let _time2 = System.get_time () in 
-(*   Pp.msgnl (str "Bulding Inductive : " ++ str (string_of_float (System.time_difference time1 time2))); *)
   try 
-    Options.silently (Command.build_mutual rel_inds) true;
-    let _time3 = System.get_time () in 
-(*     Pp.msgnl (str "Bulding Done: "++ str (string_of_float (System.time_difference time2 time3)));  *)
-(* 	let msg = *)
-(* 	  str "while trying to define"++ spc () ++ *)
-(* 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () *)
-(* 	in *)
-(*  	Pp.msgnl msg; *)
-    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;
-  with
-    | UserError(s,msg) ->
+    with_full_print (Options.silently (Command.build_mutual rel_inds)) true
+  with 
+    | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	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;
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
 	    msg
 	in
 	observe (msg);
-	raise 
-	  (UserError(s, msg))
+	raise e
     | e -> 
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
-	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;
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
 	    Cerrors.explain_exn e
 	in
  	observe msg;
-	raise 
-	  (UserError("",msg))
+	raise e
 
 
 
+let build_inductive funnames funsargs returned_types rtl = 
+  try 
+    do_build_inductive funnames funsargs returned_types rtl
+  with e -> raise (Building_graph e)
+      
+
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 9cd04123..0075fb0a 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -1,5 +1,6 @@
 
 
+
 (*
   [build_inductive parametrize funnames funargs returned_types bodies] 
   constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments 
@@ -7,7 +8,6 @@
 *)
 
 val build_inductive :
-  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 *)
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 14805cf4..ed46ec72 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -35,6 +35,18 @@ let raw_decompose_prod =
 let raw_compose_prod = 
   List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
 
+let raw_decompose_prod_n n = 
+  let rec raw_decompose_prod i args c = 
+    if i<=0 then args,c
+    else
+      match c with
+	| RProd(_,n,t,b) -> 
+	    raw_decompose_prod (i-1) ((n,t)::args) b 
+	| rt -> args,rt
+  in
+  raw_decompose_prod n []
+
+
 let raw_decompose_app = 
   let rec decompose_rapp acc rt =
 (*     msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
@@ -321,14 +333,6 @@ let rec alpha_rt excluded rt =
 	     List.map (alpha_rt excluded) args
 	    )
   in 
-  if Indfun_common.do_observe ()  && false 
-  then
-    Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
-	      prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++
-	      str "]" ++ spc () ++ str "," ++ spc () ++
-	      Printer.pr_rawconstr rt ++ spc () ++ str ")" ++ spc () ++ str "=" ++
-	      spc () ++ Printer.pr_rawconstr new_rt
-	   );
   new_rt
 
 and alpha_br excluded (loc,ids,patl,res) = 
@@ -339,12 +343,6 @@ and alpha_br excluded (loc,ids,patl,res) =
   let new_res = alpha_rt new_excluded renamed_res in 
   (loc,new_ids,new_patl,new_res)
     
-
-
-
-
-
-
 (* 
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
@@ -541,6 +539,33 @@ let ids_of_pat =
   in
   ids_of_pat Idset.empty 
   
+let id_of_name = function 
+  | Names.Anonymous -> id_of_string "x" 
+  | Names.Name x -> x
+
+(* TODO: finish Rec caes *)
+let ids_of_rawterm c = 
+  let rec ids_of_rawterm acc c = 
+    let idof = id_of_name in
+    match c with
+      | RVar (_,id) -> id::acc
+      | RApp (loc,g,args) -> 
+          ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
+      | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
+      | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
+      | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
+      | RLetTuple (_,nal,(na,po),b,c) -> 
+          List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
+      | RCases (loc,rtntypopt,tml,brchl) -> 
+	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
+      | RRec _ -> failwith "Fix inside a constructor branch"
+      | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> []
+  in
+  (* build the set *)
+  List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c)
+  
 
 
 
@@ -601,3 +626,46 @@ let zeta_normalize =
     (loc,idl,patl,zeta_normalize_term res)
   in
   zeta_normalize_term 
+
+
+
+
+let expand_as = 
+  
+  let rec add_as map pat = 
+    match pat with 
+      | PatVar _ -> map 
+      | PatCstr(_,_,patl,Name id) -> 
+	  Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl)
+      | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
+  in 
+  let rec expand_as map rt = 
+    match rt with 
+      | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt 
+      | RVar(_,id) -> 
+	  begin
+	    try 
+	      Idmap.find id map
+	    with Not_found -> rt 
+	  end
+      | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
+      | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b)
+      | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
+      | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
+      | RLetTuple(loc,nal,(na,po),v,b) ->
+	  RLetTuple(loc,nal,(na,option_map (expand_as map) po),
+		    expand_as map v, expand_as map b)
+      | RIf(loc,e,(na,po),br1,br2) ->
+	  RIf(loc,expand_as map e,(na,option_map (expand_as map) po),
+	      expand_as map br1, expand_as map br2)
+      | RRec _ ->  error "Not handled RRec"
+      | RDynamic _ -> error "Not handled RDynamic"
+      | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t)
+      | RCases(loc,po,el,brl) ->
+	  RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+		List.map (expand_as_br map) brl)
+	    
+  and expand_as_br map (loc,idl,cpl,rt) = 
+    (loc,idl,cpl,    expand_as (List.fold_left add_as map cpl) rt)
+  in
+  expand_as Idmap.empty 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index aa355485..9647640c 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -31,6 +31,7 @@ val mkRCast : rawconstr* rawconstr -> rawconstr
   These are analogous to the ones constrs
 *)
 val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr
+val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr
 val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list  ->  rawconstr 
 val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
 
@@ -107,8 +108,13 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
 *)
 val   ids_of_pat : cases_pattern -> Names.Idset.t 
 
+(* TODO: finish this function (Fix not treated) *)
+val ids_of_rawterm: rawconstr -> Names.Idset.t
 
 (* 
    removing let_in construction in a rawterm 
 *)
 val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
+
+
+val expand_as : rawconstr -> rawconstr
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 2877c19d..ce775e0b 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -72,10 +72,11 @@ let  rec mkevarmap_from_listex lex =
 		  let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in
 		  let _ = prstr "OF TYPE: " in
 		  let _ = prconstr typ in*)
-		  let info ={
+		  let info = {
 			 evar_concl = typ;
 			 evar_hyps = empty_named_context_val;
-			 evar_body = Evar_empty} in
+			 evar_body = Evar_empty;
+		         evar_extra = None} in
 		  Evd.add (mkevarmap_from_listex lex') ex info
 
 let mkEq typ c1 c2 =