Merge PR #6650: Remove dead code from funind.

9 files changed, 22 insertions, 1227 deletions

diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index a3315f22c..ad396a2cb 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -29,10 +29,6 @@ val generate_functional_principle :
   (EConstr.constr array -> int -> Tacmach.tactic) ->
   unit
 
-val compute_new_princ_type_from_rel : constr array -> Sorts.t array ->
-  types -> types
-
-
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0666ab4f1..be8abb92e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -17,69 +17,12 @@ let mkGLambda(n,t,b)    = DAst.make @@ GLambda(n,Explicit,t,b)
 let mkGProd(n,t,b)      = DAst.make @@ GProd(n,Explicit,t,b)
 let mkGLetIn(n,b,t,c)   = DAst.make @@ GLetIn(n,b,t,c)
 let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
-let mkGSort s           = DAst.make @@ GSort(s)
 let mkGHole ()          = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
-let mkGCast(b,t)        = DAst.make @@ GCast(b,CastConv t)
 
 (*
   Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
 *)
-let glob_decompose_prod =
-  let rec glob_decompose_prod args c = match DAst.get c with
-  | GProd(n,k,t,b) ->
-      glob_decompose_prod ((n,t)::args) b
-  | _ -> args,c
-  in
-  glob_decompose_prod []
-
-let glob_decompose_prod_or_letin =
-  let rec glob_decompose_prod args rt = match DAst.get rt with
-  | GProd(n,k,t,b) ->
-      glob_decompose_prod ((n,None,Some t)::args) b
-  | GLetIn(n,b,t,c) ->
-      glob_decompose_prod ((n,Some b,t)::args) c
-  | _ -> args,rt
-  in
-  glob_decompose_prod []
-
-let glob_compose_prod =
-  List.fold_left (fun b (n,t) -> mkGProd(n,t,b))
-
-let glob_compose_prod_or_letin =
-  List.fold_left (
-      fun concl decl ->
-	match decl with
-	  | (n,None,Some t) -> mkGProd(n,t,concl)
-	  | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl)
-	  | _ -> assert false)
-
-let glob_decompose_prod_n n =
-  let rec glob_decompose_prod i args c =
-    if i<=0 then args,c
-    else
-      match DAst.get c with
-	| GProd(n,_,t,b) ->
-	    glob_decompose_prod (i-1) ((n,t)::args) b
-	| _ -> args,c
-  in
-  glob_decompose_prod n []
-
-
-let glob_decompose_prod_or_letin_n n =
-  let rec glob_decompose_prod i args c =
-    if i<=0 then args,c
-    else
-      match DAst.get c with
-	| GProd(n,_,t,b) ->
-	    glob_decompose_prod (i-1) ((n,None,Some t)::args) b
-	| GLetIn(n,b,t,c) ->
-	    glob_decompose_prod (i-1) ((n,Some b,t)::args) c
-	| _ -> args,c
-  in
-  glob_decompose_prod n []
-
-
 let glob_decompose_app =
   let rec decompose_rapp acc rt =
 (*     msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *)
@@ -101,18 +44,6 @@ let glob_make_eq ?(typ= mkGHole ()) t1 t2  =
 let glob_make_neq t1 t2 =
   mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2])
 
-(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
-let glob_make_or t1 t2 = mkGApp (mkGRef(Lazy.force Coqlib.coq_or_ref),[t1;t2])
-
-(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
-   to [P1 \/ ( .... \/ Pn)]
-*)
-let rec glob_make_or_list = function
-  | [] -> invalid_arg "mk_or"
-  | [e] -> e
-  | e::l -> glob_make_or e (glob_make_or_list l)
-
-
 let remove_name_from_mapping mapping na =
   match na with
     | Anonymous -> mapping
@@ -575,97 +506,6 @@ let ids_of_pat =
   in
   ids_of_pat Id.Set.empty
 
-let id_of_name = function
-  | Anonymous -> Id.of_string "x"
-  | Name x -> x
-
-(* TODO: finish Rec caes *)
-let ids_of_glob_constr c =
-  let rec ids_of_glob_constr acc c =
-    let idof = id_of_name in
-    match DAst.get c with
-      | GVar id -> id::acc
-      | GApp (g,args) ->
-          ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
-      | GLambda (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
-      | GProd (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
-      | GLetIn (na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc
-      | GCast (c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
-      | GCast (c,CastCoerce) -> ids_of_glob_constr [] c @ acc
-      | GIf (c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
-      | GLetTuple (nal,(na,po),b,c) ->
-          List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
-      | GCases (sty,rtntypopt,tml,brchl) ->
-	  List.flatten (List.map (fun (_,(idl,patl,c)) -> idl @ ids_of_glob_constr [] c) brchl)
-      | GRec _ -> failwith "Fix inside a constructor branch"
-      | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
-  in
-  (* build the set *)
-  List.fold_left (fun acc x -> Id.Set.add x acc) Id.Set.empty (ids_of_glob_constr [] c)
-
-
-
-
-
-let zeta_normalize =
-  let rec zeta_normalize_term x = DAst.map (function
-      | GRef _
-      | GVar _
-      | GEvar _
-      | GPatVar _ as rt -> rt
-      | GApp(rt',rtl) ->
-	  GApp(zeta_normalize_term rt',
-	       List.map zeta_normalize_term rtl
-	      )
-      | GLambda(name,k,t,b) ->
-	  GLambda(name,
-		  k,
-		  zeta_normalize_term t,
-		  zeta_normalize_term b
-		 )
-      | GProd(name,k,t,b) ->
-	  GProd(name,
-	        k,
-		zeta_normalize_term t,
-		zeta_normalize_term b
-		 )
-      | GLetIn(Name id,def,typ,b) ->
-	  DAst.get (zeta_normalize_term (replace_var_by_term id def b))
-      | GLetIn(Anonymous,def,typ,b) ->
-          DAst.get (zeta_normalize_term b)
-      | GLetTuple(nal,(na,rto),def,b) ->
-	  GLetTuple(nal,
-		    (na,Option.map zeta_normalize_term rto),
-		    zeta_normalize_term def,
-		    zeta_normalize_term b
-		   )
-      | GCases(sty,infos,el,brl) ->
-	  GCases(sty,
-		 infos,
-		 List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
-		 List.map zeta_normalize_br brl
-		)
-      | GIf(b,(na,e_option),lhs,rhs) ->
-	  GIf(zeta_normalize_term b,
-	      (na,Option.map zeta_normalize_term e_option),
-	      zeta_normalize_term lhs,
-	      zeta_normalize_term rhs
-	     )
-      | GRec _ -> raise (UserError(None,str "Not handled GRec"))
-      | GSort _
-      | GHole _ as rt -> rt
-      | GCast(b,c) ->
-	  GCast(zeta_normalize_term b,
-                Miscops.map_cast_type zeta_normalize_term c)
-    ) x
-  and zeta_normalize_br (loc,(idl,patl,res)) =
-    (loc,(idl,patl,zeta_normalize_term res))
-  in
-  zeta_normalize_term
-
-
-
-
 let expand_as =
 
   let rec add_as map rt =
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 99a258de9..7088ae596 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,6 +1,5 @@
 open Names
 open Glob_term
-open Misctypes
 
 (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
 val get_pattern_id : cases_pattern -> Id.t list
@@ -21,22 +20,11 @@ val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr
 val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr
 val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr
 val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
-val mkGSort : glob_sort -> glob_constr
 val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
-val mkGCast : glob_constr* glob_constr -> glob_constr
 (*
   Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
 *)
-val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr
-val glob_decompose_prod_or_letin :
-  glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr
-val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr
-val glob_decompose_prod_or_letin_n : int -> glob_constr ->
-  (Name.t*glob_constr option*glob_constr option) list * glob_constr
-val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list  ->  glob_constr
-val glob_compose_prod_or_letin: glob_constr ->
-  (Name.t*glob_constr option*glob_constr option) list  ->  glob_constr
 val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)
 
 
@@ -44,14 +32,6 @@ val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)
 val  glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr
 (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
 val  glob_make_neq : glob_constr -> glob_constr -> glob_constr
-(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
-val  glob_make_or : glob_constr -> glob_constr -> glob_constr
-
-(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
-   to [P1 \/ ( .... \/ Pn)]
-*)
-val  glob_make_or_list : glob_constr list -> glob_constr
-
 
 (* alpha_conversion functions *)
 
@@ -109,18 +89,8 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
 *)
 val   ids_of_pat : cases_pattern -> Id.Set.t
 
-(* TODO: finish this function (Fix not treated) *)
-val ids_of_glob_constr: glob_constr -> Id.Set.t
-
-(*
-   removing let_in construction in a glob_constr
-*)
-val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr
-
-
 val expand_as : glob_constr -> glob_constr
 
-
 (* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution 
  *)
 val resolve_and_replace_implicits :
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 071599d9c..071bab2f3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -282,7 +282,6 @@ let derive_inversion fix_names =
       in
       Invfun.derive_correctness
 	Functional_principles_types.make_scheme
-	functional_induction
 	fix_names_as_constant
 	lind;
       with e when CErrors.noncritical e ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 694c80051..4acf82d00 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -56,12 +56,6 @@ let do_observe_tac s tac g =
 	     CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
 
-
-let observe_tac_strm s tac g =
-  if do_observe ()
-  then do_observe_tac s tac g
-  else tac g
-
 let observe_tac s tac g =
   if do_observe ()
   then do_observe_tac (str s) tac g
@@ -87,10 +81,6 @@ let make_eq () =
   try
     EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
   with _ -> assert false 
-let make_eq_refl () =
-  try
-    EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
-  with _ -> assert false
 
 	  
 (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
@@ -194,10 +184,9 @@ let rec generate_fresh_id x avoid i =
     id::(generate_fresh_id x (id::avoid) (pred i))
 
 
-(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ]
+(* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ]
    is the tactic used to prove correctness lemma.
 
-   [functional_induction] is the tactic defined in [indfun] (dependency problem)
    [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions
    (resp. graphs of the functions and principles and correctness lemma types) to prove correct.
 
@@ -218,7 +207,7 @@ let rec generate_fresh_id x avoid i =
    \end{enumerate}
 
 *)
-let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
+let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
   fun g ->
     (* first of all we recreate the lemmas types to be used as predicates of the induction principle
        that is~:
@@ -752,14 +741,13 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
       g
 
 
-(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
+(* [derive_correctness make_scheme funs graphs] create correctness and completeness
    lemmas for each function in [funs] w.r.t. [graphs]
 
    [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and
-   [functional_induction] is Indfun.functional_induction (same pb)
 *)
 
-let derive_correctness make_scheme functional_induction (funs: pconstant list) (graphs:inductive list) =
+let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list) =
   assert (funs <> []);
   assert (graphs <> []);
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
@@ -809,7 +797,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	)
     in
     let proving_tac =
-      prove_fun_correct !evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos
+      prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos
     in
     Array.iteri
       (fun i f_as_constant ->
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
new file mode 100644
index 000000000..e07138596
--- /dev/null
+++ b/plugins/funind/invfun.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val invfun :
+  Misctypes.quantified_hypothesis ->
+  Globnames.global_reference option ->
+  Evar.t Evd.sigma -> Evar.t list Evd.sigma
+val derive_correctness :
+  (Evd.evar_map ref ->
+   (Constr.pconstant * Sorts.family) list ->
+   'a Entries.definition_entry list) ->
+   Constr.pconstant list -> Names.inductive list -> unit
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
deleted file mode 100644
index 8f5d3f22f..000000000
--- a/plugins/funind/merge.ml
+++ /dev/null
@@ -1,1013 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Merging of induction principles. *)
-
-open Globnames
-open Tactics
-open Indfun_common
-open CErrors
-open Util
-open Constrexpr
-open Vernacexpr
-open Pp
-open Names
-open Term
-open Constr
-open Vars
-open Glob_term
-open Glob_termops
-open Decl_kinds
-open Declarations
-open Context.Rel.Declaration
-
-module RelDecl = Context.Rel.Declaration
-
-(** {1 Utilities}  *)
-
-(** {2 Useful operations on constr and glob_constr} *)
-
-let pop c = Vars.lift (-1) c
-let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
-
-(** Substitutions in constr *)
-let compare_constr_nosub t1 t2 =
-  if Constr.compare_head (fun _ _ -> false) t1 t2
-  then true
-  else false
-
-let rec compare_constr' t1 t2 =
-  if compare_constr_nosub t1 t2
-  then true
-  else (Constr.compare_head (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 Constr.map_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.understand (Global.env()) Evd.empty
-
-(** Operations on names and identifiers *)
-let id_of_name = function
-    Anonymous -> Id.of_string "H"
-  | Name id   -> id;;
-let name_of_string = Id.of_string %> Name.mk_name
-let string_of_name = id_of_name %> Id.to_string
-
-(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
-let isVarf f x =
-    match DAst.get x with
-      | GVar x -> Id.equal x f
-      | _ -> false
-
-(** [ident_global_exist id] returns true if identifier [id] is linked
-    in global environment. *)
-let ident_global_exist id =
-  try
-    let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in
-    let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
-    true
-  with e when CErrors.noncritical e -> false
-
-(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
-    global env) with base [id]. *)
-let next_ident_fresh (id:Id.t) =
-    let res = ref id in
-    while ident_global_exist !res do res := Nameops.increment_subscript !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   =
-  let sigma, env = Pfedit.get_current_context () in
-  msg (str"  " ++ Printer.pr_lconstr_env env sigma c)
-
-let prconstrnl c =
-  let sigma, env = Pfedit.get_current_context () in
-  msg (str"  " ++ Printer.pr_lconstr_env env sigma c ++ str"\n")
-
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
-let prNamedConstr s c =
-  let sigma, env = Pfedit.get_current_context () in
-  begin
-    msg(str "");
-    msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} ");
-    msg(str "");
-  end
-let prNamedRConstr s c =
-  let sigma, env = Pfedit.get_current_context () in
-  begin
-    msg(str "");
-    msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env 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 prNamedRLDecl s lc =
-  begin
-    prstr s; prstr "\n"; prstr "{§§ ";
-    List.iter
-      (fun x ->
-        match x with
-          | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp
-          | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy
-          | _ -> assert false
-        ) lc;
-    prstr " §§}\n";
-    prstr "\n";
-  end
-
-(** {2 Misc} *)
-
-exception Found of int
-
-(* Array scanning *)
-
-let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
-match Array.findi pred arr with
-| None -> Array.length arr (* all elt are positive *)
-| Some i -> i
-
-(* 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 describes 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 (Int)
-
-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
-
-(** Information about graph merging of two inductives.
-   All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *)
-
-type merge_infos =
-    {
-      ident:Id.t; (** 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;
-
-      (** rec params which remain rec param (ie not linked) *)
-      recprms1: Context.Rel.Declaration.t list;
-      recprms2: Context.Rel.Declaration.t list;
-      nrecprms1: int;
-      nrecprms2: int;
-
-      (** rec parms which became non parm (either linked to something
-         or because after a rec parm that became non parm) *)
-      otherprms1: Context.Rel.Declaration.t list;
-      otherprms2: Context.Rel.Declaration.t list;
-      notherprms1:int;
-      notherprms2:int;
-
-      (** args which remain args in merge *)
-      args1:Context.Rel.Declaration.t list;
-      args2:Context.Rel.Declaration.t list;
-      nargs1:int;
-      nargs2:int;
-
-      (** functional result args *)
-      funresprms1: Context.Rel.Declaration.t list;
-      funresprms2: Context.Rel.Declaration.t list;
-      nfunresprms1:int;
-      nfunresprms2:int;
-    }
-
-
-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
-
-(* ?? prm_linked?? *)
-let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false
-
-let is_stable x =
-  match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> 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)
-
-
-let error msg = user_err Pp.(str msg)
-
-(** {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 mib1.mind_finite == CoFinite then error "First argument is coinductive";
-  if mib2.mind_finite == CoFinite then error "Second argument is coinductive";
-  if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual";
-  if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual";
-  ()
-
-(*
-(** [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 (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in
-  let _ = prNamedConstr "DUMMY" dummy_constr in
-  let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in
-  let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in
-  let res,_ = glob_decompose_prod dummy_glob_constr in
-  let comblist = List.combine prms_decl res in
-  comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr)))
-*)
-
-let ids_of_rawlist avoid rawl =
-    List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl)
-
-
-
-(** {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 _ = prstr "\nYOUHOU shift\n" in
-  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,acc4) x ->
-        prstr (pr_merginfo mlnk.(i));prstr "\n";
-        match mlnk.(i) with
-          | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4
-          | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4
-          | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4
-          | Arg_funres -> acc1 , acc2 , acc3, x::acc4
-          | _ -> acc1 , acc2 , acc3, acc4)
-      ([],[],[],[]) arity_ctxt in
-(*  let arity_ctxt2 =
-    build_raw_params oib2.mind_arity_ctxt
-      (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
-  let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
-  let _ = prstr "\n\n\n" in
-  let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
-  let _ = prstr "\notherprms1:\n" in
-  let _ =
-    List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : ");
-			   prconstr (RelDecl.get_type decl); prstr "\n")
-    otherprms1 in
-  let _ = prstr "\notherprms2:\n" in
-  let _ =
-    List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n")
-    otherprms2 in
-  {
-    ident=id;
-    mib1=mib1;
-    oib1 = oib1;
-    mib2=mib2;
-    oib2 = oib2;
-    lnk1 = mlnk1;
-    lnk2 = mlnk2;
-    nrecprms1 = n_params1;
-    recprms1 = recprms1;
-    otherprms1 = otherprms1;
-    args1 = args1;
-    funresprms1 = funresprms1;
-    notherprms1 = Array.length mlnk1 - n_params1;
-    nfunresprms1 = List.length funresprms1;
-    nargs1 = List.length args1;
-    nrecprms2 = n_params2;
-    recprms2 = recprms2;
-    otherprms2 = otherprms2;
-    args2 = args2;
-    funresprms2 = funresprms2;
-    notherprms2 = Array.length mlnk2 - n_params2;
-    nargs2 = List.length args2;
-    nfunresprms2 = List.length funresprms2;
-  }
-
-
-
-
-(** {1 Merging functions} *)
-
-exception NoMerge
-
-let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
-  let lnk = Array.append shift.lnk1 shift.lnk2 in
-  match DAst.get c1, DAst.get c2 with
-    | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
-        let _ = prstr "\nICI1!\n" in
-        let args = filter_shift_stable lnk (arr1 @ arr2) in
-        DAst.make @@ GApp ((DAst.make @@ GVar shift.ident) , args)
-    | GApp(f1, arr1), GApp(f2,arr2)  -> raise NoMerge
-    | GLetIn(nme,bdy,typ,trm) , _ ->
-        let _ = prstr "\nICI2!\n" in
-        let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
-        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
-    | _, GLetIn(nme,bdy,typ,trm) ->
-        let _ = prstr "\nICI3!\n" in
-        let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
-        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
-    | _ -> let _ = prstr "\nICI4!\n" in
-           raise NoMerge
-
-let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
-  let lnk = Array.append shift.lnk1 shift.lnk2 in
-  match DAst.get c1, DAst.get c2 with
-    | GApp(f1, arr1), GApp(f2,arr2) ->
-        let args = filter_shift_stable lnk (arr1 @ arr2) in
-        DAst.make @@ GApp (DAst.make @@ GVar shift.ident, args)
-          (* FIXME: what if the function appears in the body of the let? *)
-    | GLetIn(nme,bdy,typ,trm) , _ ->
-      let _ = prstr "\nICI2 '!\n" in
-        let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
-        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
-    | _, GLetIn(nme,bdy,typ,trm) ->
-        let _ = prstr "\nICI3 '!\n" in
-        let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
-        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
-    | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
-
-
-
-(* Heuristic when merging two lists of hypothesis: merge every rec
-   calls of branch 1 with all rec calls of branch 2. *)
-(* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
-let rec merge_rec_hyps shift accrec
-    (ltyp:(Name.t * glob_constr option * glob_constr option) list)
-    filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list =
-  let is_app c = match DAst.get c with GApp _ -> true | _ -> false in
-  let mergeonehyp t reldecl =
-    match reldecl with
-      | (nme,x,Some ind) when is_app ind
-        -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
-      | (nme,Some _,None) -> error "letins with recursive calls not treated yet"
-      | (nme,None,Some _) -> assert false
-      | (nme,None,None) | (nme,Some _,Some _) -> assert false in
-  let is_app c = match DAst.get c with GApp (f, _) -> isVarf ind2name f | _ -> false in
-  match ltyp with
-    | [] -> []
-    | (nme,None,Some t) :: lt when is_app t ->
-        let rechyps = List.map (mergeonehyp t) 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 build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift =
-  List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
-
-
-let find_app (nme:Id.t) ltyp =
-  let is_app c = match DAst.get c with GApp (f, _) -> isVarf nme f | _ -> false in
-  try
-    ignore
-      (List.map
-          (fun x ->
-            match x with
-              | _,None,Some c when is_app c -> raise (Found 0)
-              | _ -> ())
-          ltyp);
-    false
-  with Found _ -> true
-
-let prnt_prod_or_letin nm letbdy typ =
-  match letbdy , typ with
-    | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy
-    | None , Some tp -> prNamedRConstr (string_of_name nm) tp
-    | _ , _ -> assert false
-
-
-let rec merge_types shift accrec1
-    (ltyp1:(Name.t * glob_constr option * glob_constr option) list)
-    (concl1:glob_constr) (ltyp2:(Name.t * glob_constr option * glob_constr option) list) concl2
-    : (Name.t * glob_constr option * glob_constr option) list * glob_constr =
-  let _ = prstr "MERGE_TYPES\n" in
-  let _ = prstr "ltyp 1 : " in
-  let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in
-  let _ = prstr "\nltyp 2 : " in
-  let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in
-  let _ = prstr "\n" in
-  let res =
-    match ltyp1 with
-      | [] ->
-          let isrec1 = not (List.is_empty accrec1) in
-          let isrec2 = find_app ind2name ltyp2 in
-          let rechyps =
-            if isrec1 && isrec2
-            then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *)
-              merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
-                filter_shift_stable_right
-              @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2]
-                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",None,Some concl2]) filter_shift_stable
-            else if isrec2
-            then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
-              filter_shift_stable_right
-            else ltyp2 in
-          let _ = prstr"\nrechyps : " in
-          let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy 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,None, Some t1)as e ::lt1 ->
-          (match DAst.get t1 with
-            | GApp(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,None,Some t1) :: recres) , recconcl2)
-      | (nme,Some bd, None) ::lt1 ->
-          (* FIXME: what if ind1name appears in bd? *)
-          let recres, recconcl2 =
-            merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
-          ((nme,Some bd,None) :: recres) , recconcl2
-      | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false
-  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:Id.t array) (allargs2:Id.t array)
-    (lnk:int merged_arg array) =
-  Array.fold_left_i
-    (fun i acc e ->
-      if Int.equal i (Array.length lnk - 1) then acc (* functional arg, not in allargs *)
-      else
-        match e with
-          | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc
-          | _ -> acc)
-    Id.Map.empty lnk
-
-let build_link_map allargs1 allargs2 lnk =
-  let allargs1 =
-    Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs1) in
-  let allargs2 =
-    Array.of_list (List.rev_map (fun (x,_,_) -> 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'(shifted) -> ...
-        -> (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:glob_constr)
-    (typcstr2:glob_constr) : glob_constr =
-  (* 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 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in
-  let allargs2,rest2 = glob_decompose_prod_or_letin_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 = glob_decompose_prod_or_letin rest1 in
-  let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in
-  let ltyp,concl2 =
-    merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
-  let _ = prNamedRLDecl "ltyp result:" ltyp in
-  let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in
-  let revargs1 =
-    list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in
-  let _ = prNamedRLDecl "ltyp allargs1" allargs1 in
-  let _ = prNamedRLDecl "ltyp revargs1" revargs1 in
-  let revargs2 =
-    list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in
-  let _ = prNamedRLDecl "ltyp allargs2" allargs2 in
-  let _ = prNamedRLDecl "ltyp revargs2" revargs2 in
-  let typwithprms =
-    glob_compose_prod_or_letin 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:Id.t =
-  let id = Id.to_string 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 glob_constr
-    first, each of them having distinct var names. *)
-let merge_constructors (shift:merge_infos) (avoid:Id.Set.t)
-    (typcstr1:(Id.t * glob_constr) list)
-    (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list =
-  List.flatten
-    (List.map
-        (fun (id1,rawtyp1) ->
-          List.map
-            (fun (id2,rawtyp2) ->
-              let typ = merge_one_constructor shift rawtyp1 rawtyp2 in
-              let newcstror_id = merge_constructor_id id1 id2 shift in
-              let _ = prstr "\n**************\n" 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 merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
-    (oib2:one_inductive_body) =
-  (* building glob_constr type of constructors *)
-  let mkrawcor nme avoid typ =
-    (* first replace rel 1 by a varname *)
-    let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
-    let substindtyp = EConstr.of_constr substindtyp in
-    Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in
-  let lcstr1: glob_constr list =
-    Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
-  (* add  to avoid all indentifiers of lcstr1 *)
-  let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in
-  let lcstr2 =
-    Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in
-  let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in
-
-  let params1 =
-    try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
-    with e when CErrors.noncritical e -> [] in
-  let params2 =
-    try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
-    with e when CErrors.noncritical e -> [] 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();
-  params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2
-
-
-(** [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 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. *)
-  merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
-
-
-let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *)
-  Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x
-
-let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
-  let params = prms2 @ prms1 in
-  let resparams =
-    List.fold_left
-      (fun acc (nme,tp) ->
-        let _ = prstr "param :" in
-        let _ = prNamedRConstr (string_of_name nme) tp in
-        let _ = prstr "  ;  " in
-        let typ = glob_constr_to_constr_expr tp in
-        CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
-      [] params in
-  let concl = Constrextern.extern_constr false (Global.env()) Evd.empty (EConstr.of_constr concl) in
-  let arity,_ =
-    List.fold_left
-      (fun (acc,env) decl ->
-        let nm = Context.Rel.Declaration.get_name decl in
-        let c = RelDecl.get_type decl in
-        let typ = Constrextern.extern_constr false env Evd.empty (EConstr.of_constr c) in
-        let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
-        CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
-      (concl,Global.env())
-      (shift.funresprms2 @ shift.funresprms1
-        @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
-  resparams,arity
-
-
-
-(** [glob_constr_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 glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
-    (rawlist:(Id.t * glob_constr) list) =
-  let lident = (Loc.tag shift.ident), None in
-  let bindlist , cstr_expr = (* params , arities *)
-    merge_rec_params_and_arity prms1 prms2 shift mkSet in
-  let lcstor_expr : (bool * (lident * constr_expr)) list  =
-    List.map (* zeta_normalize t ? *)
-      (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t))
-      rawlist in
-  lident , bindlist , Some cstr_expr , lcstor_expr
-
-
-let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
-  match rdecl with
-    | LocalAssum (nme,t) ->
-        let t = EConstr.of_constr t in
-        let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
-        DAst.make @@ GProd (nme,Explicit,traw,t2)
-    | LocalDef _ -> assert false
-
-
-(** [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 prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
-  let _ = prstr "\nrawlist : " in
-  let _ =
-    List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string 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 *)
-  let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
-  (* Declare inductive *)
-  let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,pl,impls = ComInductive.interp_mutual_inductive indl []
-          false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Finite (* means: not coinductive *) in
-  (* Declare the mutual inductive block with its associated schemes *)
-  ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls)
-
-
-(* Find infos on identifier id. *)
-let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
-  let kn_of_id x =
-    let f_ref = Libnames.Ident (Loc.tag x) in
-    locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
-      locate_constant f_ref in
-    try find_Function_infos (kn_of_id id)
-    with Not_found ->
-      user_err ~hdr:"indfun" (Id.print 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 occurring in both arrays [args1] and
-    [args2] are considered linked (i.e. are the same variable) in the
-    new graph.
-
-    Warning: For the moment, repetitions of an id in [args1] or
-    [args2] are not supported. *)
-let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array)
-    (args2:Id.t array) id : unit =
-  let finfo1 = find_Function_infos_safe id1 in
-  let finfo2 = find_Function_infos_safe id2 in
-  (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *)
-  (* We add one arg (functional arg of the graph) *)
-  let lnk1 = Array.make (Array.length args1 + 1) Unlinked in
-  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.findi (fun i x -> Id.equal x c) args1 with
-          | Some j -> Linked j
-          | None -> Unlinked)
-      args2 in
-  (* We add one arg (functional arg of the graph) *)
-  let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in
-  (* setting functional results *)
-  let _ = lnk1.(Array.length lnk1 - 1) <- Funres in
-  let _ = lnk2.(Array.length lnk2 - 1) <- Funres in
-  merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id
-
-
-let remove_last_arg c =
-  let (x,y) = decompose_prod c in
-  let xnolast = List.rev (List.tl (List.rev x)) in
-  compose_prod xnolast y
-
-let rec remove_n_fst_list n l = if Int.equal n 0 then l else remove_n_fst_list (n-1) (List.tl l)
-let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l))
-
-let remove_last_n_arg n c =
-  let (x,y) = decompose_prod c in
-  let xnolast = remove_n_last_list n x in
-  compose_prod xnolast y
-
-(* [funify_branches relinfo nfuns branch] returns the branch [branch]
-   of the relinfo [relinfo] modified to fit in a functional principle.
-   Things to do:
-    - remove indargs from rel applications
-    - replace *variables only* corresponding to function (recursive)
-      results by the actual function application. *)
-let funify_branches relinfo nfuns branch =
-  let mut_induct, induct =
-    match relinfo.indref with
-      | None -> assert false
-      | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
-      | _ -> assert false in
-  let is_dom c =
-    match Constr.kind c with
-      | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
-      | _ -> false in
-  let _dom_i c =
-    assert (is_dom c);
-    match Constr.kind c with
-      | Ind((u,i)) | Construct((u,_),i) -> i
-      | _ -> assert false in
-  let _is_pred c shift =
-    match Constr.kind c with
-      | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
-      | _ -> false in
-  (* FIXME: *)
-  LocalDef (Anonymous,EConstr.mkProp,EConstr.mkProp)
-
-
-let relprinctype_to_funprinctype relprinctype nfuns =
-  let relprinctype = EConstr.of_constr relprinctype in
-  let relinfo = compute_elim_sig Evd.empty (** FIXME*) relprinctype in
-  assert (not relinfo.farg_in_concl);
-  assert (relinfo.indarg_in_concl);
-  (* first remove indarg and indarg_in_concl *)
-  let relinfo_noindarg = { relinfo with
-    indarg_in_concl = false; indarg = None;
-    concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in
-  (* the nfuns last induction arguments are functional ones: remove them *)
-  let relinfo_argsok = { relinfo_noindarg with
-    nargs = relinfo_noindarg.nargs - nfuns;
-    (* args is in reverse order, so remove fst *)
-    args = remove_n_fst_list nfuns relinfo_noindarg.args;
-    concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl));
-  } in
-  let new_branches =
-    List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
-  let relinfo_branches = { relinfo_argsok with branches = new_branches } in
-  relinfo_branches
-
-(* @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" }
-
- *)
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 50b84731b..b95d64ce9 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,6 +1,5 @@
 open Constr
 
-(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes : 
   Tacmach.tactic ->
   bool -> 
diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack
index 2b443f2a1..755fa4f87 100644
--- a/plugins/funind/recdef_plugin.mlpack
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -6,5 +6,4 @@ Functional_principles_proofs
 Functional_principles_types
 Invfun
 Indfun
-Merge
 G_indfun