Backtrack wrong commit.

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

5 files changed, 256 insertions, 249 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 15d64155b..160764799 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -54,88 +54,101 @@ let observe s =
   if do_observe () 
   then Pp.msgnl s 
 
-type rel_to_fun_info = { thefun:constr; theargs: int array }
-
-let array_lasts a n =
-  let res = ref [] in
-  for i = Array.length a - n - 1 to Array.length a - 1 do 
-    res := a.(i) :: !res
-  done;
-  List.rev !res
-
-(** [compute_new_princ_type_from_rel rel_to_fun sorts princ_type]
-    transforms the inductive induction principle [princ_type] from a
-    graph relation into a functional one. The array [rel_to_fun]
-    contains the functions corresponding to each (mutual), that is:
-    the ith function corresponds to the ith mutul relation. [sorts]
-    contains the sort asked for each mutual principle. *)  
-let compute_new_princ_type_from_rel (rel_to_fun: (rel_to_fun_info list) Link.t)
-    sorts princ_type =
+(* 
+   Transform an inductive induction principle into 
+   a functional one
+*)  
+let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let princ_type_info = compute_elim_sig princ_type in 
   let env = Global.env () in 
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:identifier list) 
-      (predicates:Sign.rel_context)  : Sign.rel_context = 
+  let rec change_predicates_names (avoid:identifier list) (predicates:Sign.rel_context)  : Sign.rel_context = 
     match predicates with 
     | [] -> []
     |(Name x,v,t)::predicates -> 
        let id =  Nameops.next_ident_away x avoid in 
        Hashtbl.add tbl id x;
        (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
-    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder " in
+    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
+  in
   let avoid = (Termops.ids_of_context env_with_params ) in
   let princ_type_info = 
     { princ_type_info with
-	predicates = change_predicates_names avoid princ_type_info.predicates} in 
-  (* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
-  (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
+	predicates = change_predicates_names avoid princ_type_info.predicates
+    }
+  in 
+(*   observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *)
+(*   observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
   let change_predicate_sort i (x,_,t) = 
     let new_sort = sorts.(i) in
     let args,_ = decompose_prod t in 
     let real_args = 
-      if princ_type_info.indarg_in_concl then List.tl args else args in
-    Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) in
+      if princ_type_info.indarg_in_concl 
+      then List.tl args 
+      else args
+    in
+    Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) 
+  in
   let new_predicates = 
-    list_map_i change_predicate_sort 0 princ_type_info.predicates in
-  let env_with_params_and_predicates = 
-    List.fold_right Environ.push_named new_predicates env_with_params in
+    list_map_i
+      change_predicate_sort 
+      0
+      princ_type_info.predicates
+  in
+  let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
   let rel_as_kn = 
     fst (match princ_type_info.indref with
 	   | Some (Libnames.IndRef ind) -> ind 
-	   | _ -> error "Not a valid predicate") in
+	   | _ -> error "Not a valid predicate"
+	)
+  in
   let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
   let is_pte = 
     let set = List.fold_right Idset.add ptes_vars Idset.empty in 
     fun t -> 
       match kind_of_term t with 
 	| Var id -> Idset.mem id set 
-	| _ -> false in
+	| _ -> false 
+  in
   let pre_princ = 
     it_mkProd_or_LetIn 
       ~init:
       (it_mkProd_or_LetIn 
-	~init:(Option.fold_right mkProd_or_LetIn princ_type_info.indarg 
-	  princ_type_info.concl)
-	princ_type_info.args)
-      princ_type_info.branches in
+	 ~init:(Option.fold_right
+			   mkProd_or_LetIn
+			   princ_type_info.indarg
+			   princ_type_info.concl
+			)
+	 princ_type_info.args
+      )
+      princ_type_info.branches
+  in
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
     match kind_of_term c with
-      | Ind((u,_)) | Construct((u,_),_) -> u = rel_as_kn
-      | _ -> false in
+      | Ind((u,_)) -> u = rel_as_kn
+      | Construct((u,_),_) -> u = rel_as_kn
+      | _ -> false
+  in
   let get_fun_num c =
     match kind_of_term c with
-      | Ind(_,num) | Construct((_,num),_) -> num
-      | _ -> assert false in
+      | Ind(_,num) -> num
+      | Construct((_,num),_) -> num
+      | _ -> assert false
+  in
   let dummy_var = mkVar (id_of_string "________") in
   let mk_replacement c i args =
-    let res = mkApp((Link.find i rel_to_fun).thefun,Array.map pop (array_get_start args)) in 
-    (* observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
-    res in
+    let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in 
+(*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
+    res
+  in
   let rec has_dummy_var t  =
-    fold_constr (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
-      false t in
+    fold_constr
+      (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
+      false
+      t
+  in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
     let (new_princ_type,_) as res =
       match kind_of_term pre_princ with
@@ -143,19 +156,17 @@ let compute_new_princ_type_from_rel (rel_to_fun: (rel_to_fun_info list) Link.t)
 	    begin
 	      try match Environ.lookup_rel n env with
 		| _,_,t when is_dom t -> raise Toberemoved
-		| _ -> pre_princ,[] 
-	      with Not_found -> assert false
+		| _ -> pre_princ,[] with Not_found -> assert false
 	    end
-	| Prod(x,t,b) -> compute_new_princ_type_for_binder remove mkProd env x t b
+	| Prod(x,t,b) ->
+	    compute_new_princ_type_for_binder remove mkProd env x t b
 	| Lambda(x,t,b) ->
 	    compute_new_princ_type_for_binder  remove mkLambda env x t b
 	| Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
 	| App(f,args) when is_dom f ->
-	    (* let var_to_be_removed = destRel (array_last args) in *)
-	    let vars_to_be_removed = 
-	      List.map destRel (array_lasts args) in
+	    let var_to_be_removed = destRel (array_last args) in
 	    let num = get_fun_num f in
-	    raise (Toberemoved_with_rel (vars_to_be_removed,mk_replacement pre_princ num args))
+	    raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args))
 	| App(f,args) ->
 	    let args = 
 	      if is_pte f && remove 
@@ -190,23 +201,26 @@ let compute_new_princ_type_from_rel (rel_to_fun: (rel_to_fun_info list) Link.t)
 	let new_x : name = get_name (ids_of_context env) x in
 	let new_env = Environ.push_rel (x,None,t) env in
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
-	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
-	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
-	else (
-	  bind_fun(new_x,new_t,new_b),
-	  list_union_eq eq_constr binders_to_remove_from_t
-	    (List.map pop binders_to_remove_from_b))
-      with
-	| Toberemoved ->
-	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	 if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+	 then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+	 else
+	   (
+	     bind_fun(new_x,new_t,new_b),
+	     list_union_eq
+	       eq_constr
+	       binders_to_remove_from_t
+	       (List.map pop binders_to_remove_from_b)
+	   )
+
+       with
+	 | Toberemoved ->
+(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = 
-	      compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b, 
-	    list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and compute_new_princ_type_for_letin remove env x v t b =
     begin
@@ -218,39 +232,44 @@ let compute_new_princ_type_from_rel (rel_to_fun: (rel_to_fun_info list) Link.t)
 	let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
 	if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
 	then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
-	else (
-	  mkLetIn(new_x,new_v,new_t,new_b),
-	  list_union_eq eq_constr
-	    (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
-	    (List.map pop binders_to_remove_from_b))
+	else
+	  (
+	    mkLetIn(new_x,new_v,new_t,new_b),
+	    list_union_eq
+	      eq_constr
+	      (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+	      (List.map pop binders_to_remove_from_b)
+	  )
+	
       with
 	| Toberemoved ->
-	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = 
-	      compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
+(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-	    (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
-	    let new_b,binders_to_remove_from_b = 
-	      compute_new_princ_type remove env (substnl [c] n b)  in
-	    new_b,
-	    list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
+	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
   and  compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc)  =
-    let new_e,to_remove_from_e = compute_new_princ_type remove env e in
-    new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc in
-  (* observe (str "Computing new principe from " 
-              ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
+    let new_e,to_remove_from_e = compute_new_princ_type remove env e
+    in
+    new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+  in
+(*   observe (str "Computing new principe from " ++ pr_lconstr_env  env_with_params_and_predicates pre_princ); *)
   let pre_res,_ = 
-    compute_new_princ_type princ_type_info.indarg_in_concl 
-      env_with_params_and_predicates pre_princ in 
+    compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ 
+  in 
   let pre_res = 
-    replace_vars (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
-      (lift (List.length ptes_vars) pre_res) in
-  it_mkProd_or_LetIn
+    replace_vars 
+      (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
+      (lift (List.length ptes_vars) pre_res)
+  in
+  it_mkProd_or_LetIn  	 
     ~init:(it_mkProd_or_LetIn 
-      ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) 
-	new_predicates))
+	     ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) 
+			      new_predicates)
+	  )
     princ_type_info.params
     
   
@@ -297,22 +316,16 @@ let defined () =
 
 
 
-let build_rel_to_fun_info funs =
-  let rel2funinfoAUX = ref Link.empty in
-  let _ = 
-    Array.iteri 
-      (fun i x -> rel2funinfoAUX := Link.add i {thefun=mkConst x; theargs=[||]} !rel2funinfoAUX)
-      funs in
-  !rel2funinfoAUX
-  
-
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (compute_elim_sig old_princ_type).nparams in 
   (*   let time1 = System.get_time ()  in *)
-  let rel2funinfo = build_rel_to_fun_info funs in
   let new_principle_type =
-    compute_new_princ_type_from_rel rel2funinfo sorts old_princ_type in
+    compute_new_princ_type_from_rel
+      (Array.map mkConst funs)
+      sorts
+      old_princ_type
+  in
   (*    let time2 = System.get_time ()  in *)
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
   (*    observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
@@ -320,9 +333,11 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     next_global_ident_away true (id_of_string "___________princ_________") []
   in
   begin
-    Command.start_proof new_princ_name
+    Command.start_proof
+      new_princ_name
       (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
-      new_principle_type (hook new_principle_type)
+      new_principle_type
+      (hook new_principle_type)
     ;
     (*       let _tim1 = System.get_time ()  in *)
     Pfedit.by  (proof_tac (Array.map mkConst funs) mutr_nparams);
@@ -487,110 +502,140 @@ let get_funs_constant mp dp =
 exception No_graph_found 
 exception Found_type of int 
 
-let make_scheme (fas:(constant*Rawterm.rawsort)list): Entries.definition_entry list =
-  let env = Global.env ()
+let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = 
+  let env = Global.env () 
   and sigma = Evd.empty in
-  let funs = List.map fst fas in
-  let first_fun = List.hd funs in
+  let funs = List.map fst fas in 
+  let first_fun = List.hd funs in 
+
+
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = 
-    try fst (find_Function_infos  first_fun).graph_ind 
-    with Not_found -> raise No_graph_found in
+    try 
+      fst (find_Function_infos  first_fun).graph_ind 
+    with Not_found -> raise No_graph_found 
+  in
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
   let this_block_funs = Array.map fst this_block_funs_indexes in 
   let prop_sort = InProp in
   let funs_indexes = 
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
-    List.map (fun const -> List.assoc const this_block_funs_indexes) funs in
+    List.map
+      (function const -> List.assoc const this_block_funs_indexes)
+      funs
+  in
   let ind_list = 
     List.map 
       (fun (idx) -> 
 	 let ind = first_fun_kn,idx in 
 	 let (mib,mip) = Global.lookup_inductive ind in
-	 ind,mib,mip,true,prop_sort) funs_indexes in
+	 ind,mib,mip,true,prop_sort
+      )
+      funs_indexes
+  in
   let l_schemes = 
-    List.map (Typing.type_of env sigma) 
-      (Indrec.build_mutual_indrec env sigma ind_list) in 
+    List.map
+      (Typing.type_of env sigma) 
+      (Indrec.build_mutual_indrec env sigma ind_list)
+  in 
   let i = ref (-1) in
   let sorts = 
     List.rev_map (fun (_,x) -> 
-      Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)) 
-      fas in
+		Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+	     ) 
+      fas 
+  in
   (* We create the first priciple by tactic *)
   let first_type,other_princ_types = 
     match l_schemes with 
 	s::l_schemes -> s,l_schemes
-      | _ -> anomaly "" in
+      | _ -> anomaly ""
+  in
   let (_,(const,_,_)) = 
     build_functional_principle false
-      first_type (Array.of_list sorts) this_block_funs 0
+      first_type
+      (Array.of_list sorts)
+      this_block_funs
+      0
       (prove_princ_for_struct false 0 (Array.of_list funs))
-      (fun _ _ _ -> ()) in      
+      (fun _ _ _ -> ())
+  in      
   incr i;
   let opacity = 
     let finfos = find_Function_infos this_block_funs.(0) in 
     try 
       let equation =  Option.get finfos.equation_lemma in  
       (Global.lookup_constant equation).Declarations.const_opaque 
-    with Option.IsNone -> false in (* non recursive definition *) 
+    with Option.IsNone -> (* non recursive definition *) 
+      false
+  in
   let const = {const with const_entry_opaque = opacity } in 
   (* The others are just deduced *)
   if other_princ_types = [] 
-  then [const]
+  then
+    [const]
   else
     let other_fun_princ_types = 
+      let funs = Array.map mkConst this_block_funs in 
       let sorts = Array.of_list sorts in 
-      List.map (compute_new_princ_type_from_rel 
-		   (build_rel_to_fun_info this_block_funs) sorts)
-	other_princ_types in
-    let first_princ_body,first_princ_type = 
-      const.Entries.const_entry_body, const.Entries.const_entry_type in 
-    (* the principle has form forall ...., fix .*)
-    let ctxt,fix = Sign.decompose_lam_assum first_princ_body in 
+      List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
+    in
+    let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in 
+    let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in 
     let other_result = 
       List.map (* we can now compute the other principles *)
 	(fun scheme_type -> 
-	  incr i;
-	  observe (Printer.pr_lconstr scheme_type);
-	  let type_concl = snd (Sign.decompose_prod_assum scheme_type) in 
-	  let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in 
-	  let f = fst (decompose_app applied_f) in
-	  try (* we search the number of the function in the fix block (name of
-		 the function) *)
-	    Array.iteri 
-	      (fun j t -> 
+	   incr i;
+	   observe (Printer.pr_lconstr scheme_type);
+	   let type_concl = snd (Sign.decompose_prod_assum scheme_type) in 
+	   let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in 
+	   let f = fst (decompose_app applied_f) in
+	   try (* we search the number of the function in the fix block (name of the function) *)
+	     Array.iteri 
+	     (fun j t -> 
 		let t =  snd (Sign.decompose_prod_assum t) in 
 		let applied_g = List.hd (List.rev (snd (decompose_app t))) in 
 		let g = fst (decompose_app applied_g) in
 		if eq_constr f g
 		then raise (Found_type j); 
 		observe (Printer.pr_lconstr f ++ str " <> " ++
-			    Printer.pr_lconstr g))
-	      ta;
-	    (* If we reach this point, the two principle are not mutually recursive 
-	       We fall back to the previous method *)
-	    let (_,(const,_,_)) = 
-	      build_functional_principle
-		false (List.nth other_princ_types (!i - 1)) 
-		(Array.of_list sorts) this_block_funs !i
-		(prove_princ_for_struct false !i (Array.of_list funs))
-		(fun _ _ _ -> ()) in 
-	    const
-	  with Found_type i -> 
-	    let princ_body = 
-	      Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt in 
-	    {const with 
+			   Printer.pr_lconstr g)
+		  
+	     )
+	     ta;
+	   (* If we reach this point, the two principle are not mutually recursive 
+	      We fall back to the previous method 
+	   *)
+	     let (_,(const,_,_)) = 
+	       build_functional_principle
+		 false 
+		 (List.nth other_princ_types (!i - 1))
+		 (Array.of_list sorts)
+		 this_block_funs
+		 !i
+		 (prove_princ_for_struct false !i (Array.of_list funs))
+		 (fun _ _ _ -> ())
+	     in 
+	     const
+	 with Found_type i -> 
+	   let princ_body = 
+	     Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt
+	   in 
+	   {const with 
 	      Entries.const_entry_body = princ_body; 
-	      Entries.const_entry_type = Some scheme_type})
-	other_fun_princ_types in
+	      Entries.const_entry_type = Some scheme_type
+	   }
+      )
+      other_fun_princ_types
+    in
     const::other_result
 
 let build_scheme fas = 
   let bodies_types = 
     make_scheme 
       (List.map 
-	  (fun (_,f,sort) -> 
+	 (fun (_,f,sort) -> 
 	    let f_as_constant =
 	      try
 		match Nametab.global f with 
@@ -599,54 +644,72 @@ let build_scheme fas =
 	      with Not_found ->
 	      	Util.error ("Cannot find "^ Libnames.string_of_reference f)
 	    in
-	    (f_as_constant,sort)) 
-	  fas) in 
+	    (f_as_constant,sort)
+	 ) 
+	 fas
+      ) 
+  in 
   List.iter2 
     (fun (princ_id,_,_) def_entry -> 
-      ignore 
-	(Declare.declare_constant 
+       ignore 
+	 (Declare.declare_constant 
 	    princ_id 
 	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
-      Flags.if_verbose 
-	(fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id)
-    fas bodies_types
+       Flags.if_verbose 
+	 (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
+    )
+    fas
+    bodies_types
   
 
 
 let build_case_scheme fa = 
   let env = Global.env () 
   and sigma = Evd.empty in
-  (* let id_to_constr id = Tacinterp.constr_of_id env  id in  *)
-  let funs = 
-    (fun (_,f,_) ->  
-      try Libnames.constr_of_global (Nametab.global f)
-      with Not_found -> 
-	Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in 
+(*   let id_to_constr id =  *)
+(*     Tacinterp.constr_of_id env  id *)
+(*   in  *)
+  let funs =  (fun (_,f,_) ->  
+		 try Libnames.constr_of_global (Nametab.global f)
+		 with Not_found -> 
+		   Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in 
   let first_fun = destConst  funs in 
+
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
-  let first_fun_kn = 
-    try fst (find_Function_infos  first_fun).graph_ind
-    with Not_found -> raise No_graph_found in
+  let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
+
+
+
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
   let this_block_funs = Array.map fst this_block_funs_indexes in 
   let prop_sort = InProp in
   let funs_indexes = 
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in 
-    List.assoc (destConst funs) this_block_funs_indexes in
-  let ind_fun = let ind = first_fun_kn,funs_indexes in ind,prop_sort in
-  let scheme_type =  
-    (Typing.type_of env sigma) 
-      ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in 
+    List.assoc (destConst funs) this_block_funs_indexes
+  in
+  let ind_fun = 
+	 let ind = first_fun_kn,funs_indexes in 
+	 ind,prop_sort
+  in
+  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in 
   let sorts =
-    (fun (_,_,x) -> 
-      Termops.new_sort_in_family (Pretyping.interp_elimination_sort x))
-      fa in
+    (fun (_,_,x) ->
+       Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+    )
+      fa
+  in
   let princ_name =  (fun (x,_,_) -> x) fa in
   let _ = 
 (*     observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
 (* 	       pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
 (* 	    ); *)
-    generate_functional_principle false scheme_type (Some ([|sorts|]))
-      (Some princ_name) this_block_funs 0 
-      (prove_princ_for_struct false 0 [|destConst funs|]) in
+    generate_functional_principle
+      false
+      scheme_type
+      (Some ([|sorts|]))
+      (Some princ_name)
+      this_block_funs
+      0
+      (prove_princ_for_struct false 0 [|destConst funs|])
+  in
   ()
diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
index 6fa4fa70c..cf28c6e6c 100644
--- a/contrib/funind/functional_principles_types.mli
+++ b/contrib/funind/functional_principles_types.mli
@@ -21,11 +21,8 @@ val generate_functional_principle :
   (constr array -> int -> Tacmach.tactic) -> 
   unit
 
-(* TODO: hide [rel_to_fun_info] and [compute_new_princ_type_from_rel]. *)
-type rel_to_fun_info = { thefun:constr; theargs: int array }
-
-val compute_new_princ_type_from_rel : (rel_to_fun_info list) Indfun_common.Link.t
-  -> sorts array -> types -> types
+val compute_new_princ_type_from_rel : constr array -> sorts array -> 
+  types -> types
 
 
 exception No_graph_found
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index c02a483a1..78e2c4408 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -3,9 +3,6 @@ open Pp
 
 open Libnames
 
-(* This map is used to deal with debruijn linked indices. *)
-module Link = Map.Make (struct type t = int let compare = Pervasives.compare end)
-
 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 (mk_rel_id id) "_correct"
@@ -509,20 +506,3 @@ let do_observe () =
     
 exception Building_graph of exn 
 exception Defining_principle of exn
-
-
-(* type 'a ctactic = 'a -> Proof_type.goal Evd.sigma -> (('a * Proof_type.goal) list Evd.sigma * Proof_type.validation) *)
-open Proof_type
-open Evd
-let ctclThen (tac1:tactic) (tac2:tactic): tactic =
-  (fun g -> 
-    let _gls,_valid = tac1 g in
-    Tacticals.tclTHEN tac1 tac2 g
-  )
-(* 
-   let lres = List.map (fun g -> tac2 {it=g;sigma=sig_sig gls}) (sig_it gls) in
-   let lgls,lvalid = List.split lres in
-   let newvalid = 
-     (fun lpftree -> List.map2 (fun x y -> x y) lvalid lpftree) in
-   lgls,newvalid
-*)
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index dd7078f4c..7da1d6f0b 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -1,9 +1,6 @@
 open Names
 open Pp
 
-(* This map is used to deal with debruijn linked indices. *)
-module Link : Map.S with type key = int
-
 (* 
    The mk_?_id function build different name w.r.t. a function 
    Each of their use is justified in the code 
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 94bb3779d..adec67e36 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -21,7 +21,6 @@ open Declarations
 open Environ
 open Rawterm
 open Rawtermops
-open Functional_principles_types
 
 (** {1 Utilities}  *)
 
@@ -80,7 +79,7 @@ let next_ident_fresh (id:identifier) =
 
 (** {2 Debugging} *)
 (* 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)
 let prconstrnl c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
@@ -196,16 +195,6 @@ struct
   let fold i j = if i<j then foldup i j else folddown i j
 end
 
-(** Inductive lookup *)
-let lookup_induct_princ id: Names.constant*constr =
-  let ind_kn =
-    fst (locate_with_msg
-      (Libnames.pr_reference (Libnames.Ident (dummy_loc , id)) ++ str ": Not an inductive type!")
-      locate_ind (Libnames.Ident (dummy_loc , id))) in  
-  (* TODO: replace 0 by the mutual number *)
-  let princ = destConst (Indrec.lookup_eliminator (ind_kn,0) (InProp)) in 
-  let princ_type = Typeops.type_of_constant (Global.env()) princ in
-  princ,princ_type
 
 (** {1 Parameters shifting and linking information} *)
 
@@ -246,6 +235,8 @@ let linkmonad f lnkvar =
 
 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";
@@ -906,12 +897,16 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let _ = 
     List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in
   let _ = prstr "\nend rawlist\n" in
-  (* FIX: retransformer en constr ici
-     let shift_prm = { shift_prm with recprms1=prms1; recprms1=prms1; } in *)
+(* FIX: retransformer en constr ici
+   let shift_prm = 
+    { shift_prm with
+      recprms1=prms1;
+      recprms1=prms1;    
+    } in *)
   let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
-  let _ = Command.build_mutual [(indexpr,None)] true (* means: not coinductive *) in
-  ()
+  Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
+
 
 (* Find infos on identifier id. *)
 let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
@@ -923,7 +918,6 @@ let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
     with Not_found ->
       errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
 
-
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
     [ind1] and [ind2]. identifiers occuring in both arrays [args1] and
@@ -952,31 +946,7 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array)
   (* setting functional results *)
   let _ = lnk1.(Array.length lnk1 - 1) <- Funres in 
   let _ = lnk2.(Array.length lnk2 - 1) <- Funres in
-  let res = merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id in  
-  let princ,princ_type= lookup_induct_princ id in
-  prconstr princ_type;  
-  let argnums1 = Array.mapi (fun i _ -> i) args1 in
-  let cpt = ref 0 in
-  let argnums2 = Array.mapi 
-    (fun i x -> 
-      match x with
-        | Unlinked -> !cpt + Array.length argnums1
-        | Linked j -> j 
-        | Funres -> assert false) 
-    lnk2 in
-  let rel2funinfo = 
-    Link.add 0 { thefun = mkConst finfo2.function_constant; theargs = argnums1}
-      (Link.add 0 { thefun = mkConst finfo1.function_constant; theargs = argnums2}
-        Link.empty) in
-  let _type_scheme = 
-    Functional_principles_types.compute_new_princ_type_from_rel 
-      rel2funinfo
-      [|Termops.new_sort_in_family InProp|] (* FIXME: la sort doit être réglable *)
-      princ_type
-  in
-  prstr "AFTER COMPUTATION OF MERGED TYPE SCHEME\n";
-  (* prconstr type_scheme; *)
-  res
+  merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id