menage dans funind + deplaceemnt de recdef dans funind

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

6 files changed, 1478 insertions, 1233 deletions

diff --git a/contrib/funind/Recdef.v b/contrib/funind/Recdef.v
new file mode 100644
index 000000000..2d206220e
--- /dev/null
+++ b/contrib/funind/Recdef.v
@@ -0,0 +1,48 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+Require Compare_dec.
+Require Wf_nat.
+
+Section Iter.
+Variable A : Type.
+
+Fixpoint iter (n : nat) : (A -> A) -> A -> A :=
+  fun (fl : A -> A) (def : A) =>
+  match n with
+  | O => def
+  | S m => fl (iter m fl def)
+  end.
+End Iter.
+
+Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')).
+  intro p; intro p'; change (S p <= S (S (p + p'))); 
+    apply le_S; apply Gt.gt_le_S; change (p < S (p + p')); 
+    apply Lt.le_lt_n_Sm; apply Plus.le_plus_l.
+Qed.
+ 
+
+Theorem Splus_lt : forall p p' : nat, p' < S (p + p').
+  intro p; intro p'; change (S p' <= S (p + p')); 
+    apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm;
+       apply Plus.le_plus_r.
+Qed.
+
+Theorem le_lt_SS : forall x y, x <= y -> x < S (S y).
+intro x; intro y; intro H; change (S x <= S (S y)); 
+    apply le_S; apply Gt.gt_le_S; change (x < S y); 
+    apply Lt.le_lt_n_Sm; exact H.
+Qed.
+
+Inductive max_type (m n:nat) : Set :=
+  cmt : forall v, m <= v -> n <= v -> max_type m n.
+
+Definition max : forall m n:nat, max_type m n.
+intros m n; case (Compare_dec.le_gt_dec m n).
+intros h; exists n; [exact h | apply le_n].
+intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h].
+Defined.
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/g_indfun.ml4
index 4b3492b12..4b3492b12 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/g_indfun.ml4
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
new file mode 100644
index 000000000..49c07ff72
--- /dev/null
+++ b/contrib/funind/recdef.ml
@@ -0,0 +1,1430 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Term
+open Termops
+open Environ
+open Declarations
+open Entries
+open Pp
+open Names
+open Libnames
+open Nameops
+open Util
+open Closure
+open RedFlags
+open Tacticals
+open Typing
+open Tacmach
+open Tactics
+open Nametab
+open Decls
+open Declare
+open Decl_kinds
+open Tacred
+open Proof_type
+open Vernacinterp
+open Pfedit
+open Topconstr
+open Rawterm
+open Pretyping
+open Pretyping.Default
+open Safe_typing
+open Constrintern
+open Hiddentac
+
+open Equality
+open Auto
+open Eauto
+
+open Genarg
+
+
+let compute_renamed_type gls c = 
+  rename_bound_var (pf_env gls) [] (pf_type_of gls c)
+
+let qed () = Command.save_named true 
+let defined () = Command.save_named false
+
+let pf_get_new_ids idl g = 
+  let ids = pf_ids_of_hyps g in 
+  List.fold_right
+    (fun id acc -> next_global_ident_away false id (acc@ids)::acc)
+    idl 
+    []
+
+let pf_get_new_id id g = 
+  List.hd (pf_get_new_ids [id] g)
+
+let h_intros l = 
+  tclMAP h_intro l
+
+let do_observe_tac s tac g =
+  let goal = begin (Printer.pr_goal (sig_it g)) end in
+ try let v = tac g in msgnl (goal ++ fnl () ++ (str "recdef ") ++
+    (str s)++(str " ")++(str "finished")); v
+ with e ->
+   msgnl (str "observation "++str s++str " raised exception " ++ 
+	    Cerrors.explain_exn e ++ str " on goal " ++ goal ); 
+   raise e;;
+
+
+let observe_tac s tac g = 
+  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+  then do_observe_tac s tac g
+  else tac g
+
+let hyp_ids = List.map id_of_string
+    ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res";
+     "hspec";"heq"; "hrec"; "hex"; "teq"; "pmax";"hle"];;
+
+let rec nthtl = function
+    l, 0 -> l  | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];;
+
+let hyp_id n l = List.nth l n;;
+
+let (x_id:identifier) = hyp_id 0 hyp_ids;;
+let (v_id:identifier) = hyp_id 1 hyp_ids;;
+let (k_id:identifier) = hyp_id 2 hyp_ids;;
+let (def_id:identifier) = hyp_id 3 hyp_ids;;
+let (p_id:identifier) = hyp_id 4 hyp_ids;;
+let (h_id:identifier) = hyp_id 5 hyp_ids;;
+let (n_id:identifier) = hyp_id 6 hyp_ids;;
+let (h'_id:identifier) = hyp_id 7 hyp_ids;;
+let (ano_id:identifier) = hyp_id 8 hyp_ids;;
+let (rec_res_id:identifier) = hyp_id 10 hyp_ids;;
+let (hspec_id:identifier) = hyp_id 11 hyp_ids;;
+let (heq_id:identifier) = hyp_id 12 hyp_ids;;
+let (hrec_id:identifier) = hyp_id 13 hyp_ids;;
+let (hex_id:identifier) = hyp_id 14 hyp_ids;;
+let (teq_id:identifier) = hyp_id 15 hyp_ids;;
+let (pmax_id:identifier) = hyp_id 16 hyp_ids;;
+let (hle_id:identifier) = hyp_id 17 hyp_ids;;
+
+let message s = if Flags.is_verbose () then msgnl(str s);;
+
+let def_of_const t =
+   match (kind_of_term t) with
+    Const sp -> 
+      (try (match (Global.lookup_constant sp) with
+             {const_body=Some c} -> Declarations.force c
+	     |_ -> assert false)
+       with _ -> 
+	 anomaly ("Cannot find definition of constant "^
+		    (string_of_id (id_of_label (con_label sp))))
+      )
+     |_ -> assert false
+
+let type_of_const t =
+   match (kind_of_term t) with
+    Const sp -> Typeops.type_of_constant (Global.env()) sp
+    |_ -> assert false
+
+let arg_type t =
+  match kind_of_term (def_of_const t) with
+      Lambda(a,b,c) -> b
+    | _ -> assert false;;
+
+let evaluable_of_global_reference r =
+  match r with 
+      ConstRef sp -> EvalConstRef sp
+    | VarRef id -> EvalVarRef id
+    | _ -> assert false;;
+
+
+let rank_for_arg_list h = 
+  let predicate a b = 
+      try List.for_all2 eq_constr a b with
+        Invalid_argument _ -> false in
+  let rec rank_aux i = function
+  | [] -> None
+  | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in
+  rank_aux 0;;
+
+let rec (find_call_occs : int -> constr -> constr -> 
+  (constr list -> constr) * constr list list) =
+ fun nb_lam f expr ->
+  match (kind_of_term expr) with
+    App (g, args) when g = f -> 
+      (fun l -> List.hd l), [Array.to_list args]
+  | App (g, args) ->
+     let (largs: constr list) = Array.to_list args in
+     let rec find_aux = function
+	 []    -> (fun x -> []), []
+       | a::upper_tl ->
+         (match find_aux upper_tl with
+          (cf, ((arg1::args) as args_for_upper_tl)) -> 
+           (match find_call_occs nb_lam f a with
+             cf2, (_ :: _ as other_args) ->
+               let rec avoid_duplicates args =
+                  match args with
+                  | [] -> (fun _ -> []), []
+                  | h::tl -> 
+                      let recomb_tl, args_for_tl =
+                          avoid_duplicates tl in
+                    match rank_for_arg_list h args_for_upper_tl with
+                    | None -> 
+                        (fun l -> List.hd l::recomb_tl(List.tl l)),
+                        h::args_for_tl
+                    | Some i ->
+                        (fun l -> List.nth l (i+List.length args_for_tl)::
+                            recomb_tl l),
+                        args_for_tl
+               in
+               let recombine, other_args' =
+                   avoid_duplicates other_args in
+	       let len1 = List.length other_args' in                   
+                   (fun l -> cf2 (recombine l)::cf(nthtl(l,len1))),
+                     other_args'@args_for_upper_tl
+           | _, [] -> (fun x -> a::cf x), args_for_upper_tl)
+	 | _, [] ->
+	   (match find_call_occs nb_lam f a with
+	     cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args)
+	   | _, [] -> (fun x -> a::upper_tl), [])) in
+     begin
+       match (find_aux largs) with
+	   cf, [] -> (fun l -> mkApp(g, args)), []
+	 | cf, args ->
+	     (fun l -> mkApp (g, Array.of_list (cf l))), args
+     end
+  | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[])
+  | Var(id) -> (fun l -> expr), []
+  | Meta(_) -> error "find_call_occs : Meta"
+  | Evar(_) -> error "find_call_occs : Evar"
+  | Sort(_)  -> (fun l -> expr), []
+  | Cast(b,_,_) -> find_call_occs nb_lam f b
+  | Prod(_,_,_) -> error "find_call_occs : Prod"
+  | Lambda(na,t,b) -> 
+      begin
+	match find_call_occs (succ nb_lam) f b with 
+	  | _, [] ->  (* Lambda are authorized as long as they do not contain 
+			 recursives calls *)
+	      (fun l -> expr),[]
+	  | _ ->  error "find_call_occs : Lambda"
+      end
+  | LetIn(na,v,t,b) -> 
+      begin
+	match find_call_occs nb_lam f v, find_call_occs (succ nb_lam) f b with 
+	  | (_,[]),(_,[]) -> 
+	      ((fun l -> expr), [])
+	  | (_,[]),(cf,(_::_ as l)) -> 
+	      ((fun  l -> mkLetIn(na,v,t,cf l)),l)
+	  | (cf,(_::_ as l)),(_,[]) -> 
+	      ((fun l -> mkLetIn(na,cf l,t,b)), l)
+	  | _ -> error "find_call_occs : LetIn"
+      end
+  | Const(_) -> (fun l -> expr), []
+  | Ind(_) -> (fun l -> expr), []
+  | Construct (_, _) -> (fun l -> expr), []
+  | Case(i,t,a,r) ->
+      (match find_call_occs nb_lam f a with
+	cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
+      | _ -> (fun l -> expr),[])
+  | Fix(_) -> error "find_call_occs : Fix"
+  | CoFix(_) -> error "find_call_occs : CoFix";;
+
+let coq_constant s =
+  Coqlib.gen_constant_in_modules "RecursiveDefinition" 
+    (Coqlib.init_modules @ Coqlib.arith_modules) s;;
+
+let constant sl s =
+  constr_of_global
+    (locate (make_qualid(Names.make_dirpath 
+			   (List.map id_of_string (List.rev sl)))
+	       (id_of_string s)));;
+
+let find_reference sl s =
+    (locate (make_qualid(Names.make_dirpath 
+			   (List.map id_of_string (List.rev sl)))
+	       (id_of_string s)));;
+
+let delayed_force f = f ()
+
+let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
+let le_lt_n_Sm = function () -> (coq_constant "le_lt_n_Sm")
+
+let le_trans = function () -> (coq_constant "le_trans")
+let le_lt_trans = function () -> (coq_constant "le_lt_trans")
+let lt_S_n = function () -> (coq_constant "lt_S_n")
+let le_n = function () -> (coq_constant "le_n")
+let refl_equal = function () -> (coq_constant "refl_equal")
+let eq = function () -> (coq_constant "eq")
+let ex = function () -> (coq_constant "ex")
+let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
+let coq_sig = function () -> (coq_constant "sig")
+let coq_O = function () -> (coq_constant "O")
+let coq_S = function () -> (coq_constant "S")
+
+let gt_antirefl = function () -> (coq_constant "gt_irrefl")
+let lt_n_O = function () -> (coq_constant "lt_n_O")
+let lt_n_Sn = function () -> (coq_constant "lt_n_Sn")
+
+let f_equal = function () -> (coq_constant "f_equal")
+let well_founded_induction = function () -> (coq_constant "well_founded_induction")
+let well_founded = function () -> (coq_constant "well_founded")
+let acc_rel = function () -> (coq_constant "Acc")
+let acc_inv_id = function () -> (coq_constant "Acc_inv")
+let well_founded_ltof = function () ->  (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
+let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded")
+let max_ref = function () -> (find_reference ["Recdef"] "max")
+let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let max_constr = function () -> (constr_of_global (delayed_force max_ref))
+
+let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
+let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
+
+(* These are specific to experiments in nat with lt as well_founded_relation, *)
+(*    but this should be made more general. *)
+let nat = function () -> (coq_constant "nat")
+let lt = function () -> (coq_constant "lt")
+
+(* This is simply an implementation of the case_eq tactic.  this code
+  should be replaced with the tactic defined in Ltac in Init/Tactics.v *)
+let  mkCaseEq a  : tactic =
+     (fun g ->
+       let type_of_a = pf_type_of g a in
+       tclTHENLIST
+         [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
+          (fun g2 ->
+	    change_in_concl None 
+	      (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2))
+		  g2);
+	  simplest_case a] g);;
+
+(* This is like the previous one except that it also rewrite on all
+  hypotheses except the ones given in the first argument.  All the
+  modified hypotheses are generalized in the process and should be
+  introduced back later; the result is the pair of the tactic and the
+  list of hypotheses that have been generalized and cleared. *)
+let mkDestructEq :
+  identifier list -> constr -> goal sigma -> tactic * identifier list =
+  fun not_on_hyp expr g ->
+  let hyps = pf_hyps g in 
+  let to_revert = 
+    Util.map_succeed 
+      (fun (id,_,t) -> 
+        if List.mem id not_on_hyp || not (Termops.occur_term expr t)
+        then failwith "is_expr_context";
+        id) hyps in
+  let to_revert_constr = List.rev_map mkVar to_revert in 
+  let type_of_expr = pf_type_of g expr in
+  let new_hyps = mkApp(delayed_force refl_equal, [|type_of_expr; expr|])::
+           to_revert_constr in
+    tclTHENLIST
+     [h_generalize new_hyps;
+      (fun g2 ->
+	change_in_concl None 
+	  (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+      simplest_case expr], to_revert
+
+let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
+    cont_function (eqs:constr list) nb_lam (expr:constr) g =
+  let finalize () =  	if extra_eqn then
+	  let teq = pf_get_new_id teq_id g in
+	    tclTHENLIST
+	      [ h_intro teq;
+		thin thin_intros;
+		h_intros thin_intros;
+		
+		tclMAP 
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false)) 
+		  (List.rev eqs);
+		(fun g1 -> 
+		   let ty_teq = pf_type_of g1 (mkVar teq) in 
+		   let teq_lhs,teq_rhs = 
+		     let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in 
+		     args.(1),args.(2) 
+		   in
+	           cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1
+		)
+	      ]
+	      g
+	else
+	  tclTHENSEQ[
+	    thin thin_intros;
+	    h_intros thin_intros;
+	    cont_function eqs expr 
+	  ] g
+  in
+  if nb_lam = 0 
+  then finalize () 
+  else
+    match kind_of_term expr with
+      | Lambda (n, _, b) -> 
+     	  let n1 = 
+	    match n with
+      		Name x -> x
+              | Anonymous -> ano_id
+	  in
+     	  let new_n = pf_get_new_id n1 g in
+	  tclTHEN (h_intro new_n)
+	    (mk_intros_and_continue thin_intros extra_eqn cont_function eqs 
+	       (pred nb_lam) (subst1 (mkVar new_n) b)) g
+      | _ -> 
+	  assert false 
+(* 	  finalize () *)
+let const_of_ref = function
+    ConstRef kn -> kn
+  | _ -> anomaly "ConstRef expected"
+
+let simpl_iter clause =
+  reduce 
+    (Lazy
+       {rBeta=true;rIota=true;rZeta= true; rDelta=false;
+        rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
+(*     (Simpl (Some ([],mkConst (const_of_ref (delayed_force iter_ref))))) *)
+    clause
+
+(* The boolean value is_mes expresses that the termination is expressed
+  using a measure function instead of a well-founded relation. *)
+let tclUSER tac is_mes l g = 
+  let clear_tac = 
+    match l with 
+      | None -> h_clear true []
+      | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l)
+  in
+  tclTHENSEQ 
+    [
+      clear_tac;
+      if is_mes 
+      then tclTHEN
+             (unfold_in_concl [([], evaluable_of_global_reference
+                                      (delayed_force ltof_ref))])
+             tac
+      else tac
+    ]
+    g
+    
+    
+let list_rewrite (rev:bool) (eqs: constr list) =
+  tclREPEAT
+    (List.fold_right
+       (fun eq i -> tclORELSE (rewriteLR eq) i)
+       (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
+
+let base_leaf_terminate (func:global_reference) eqs expr =
+(*  let _ = msgnl (str "entering base_leaf") in *)
+  (fun g ->
+     let k',h = 
+       match pf_get_new_ids [k_id;h_id] g with 
+	   [k';h] -> k',h
+	 | _ -> assert false
+     in
+     tclTHENLIST
+     [observe_tac "first split" (split (ImplicitBindings [expr]));
+      observe_tac "second split"
+        (split (ImplicitBindings [delayed_force coq_O]));
+      observe_tac "intro k" (h_intro k');
+      observe_tac "case on k" 
+        (tclTHENS (simplest_case (mkVar k'))
+        [(tclTHEN (h_intro h) 
+          (tclTHEN (simplest_elim (mkApp (delayed_force gt_antirefl,
+					 [| delayed_force coq_O |])))
+            default_auto)); tclIDTAC ]);
+      intros;
+      simpl_iter onConcl;
+      unfold_constr func;
+      list_rewrite true eqs;
+      default_auto] g);;
+
+(* La fonction est donnee en premier argument a la 
+   fonctionnelle suivie d'autres Lambdas et de Case ...
+   Pour recuperer la fonction f a partir de la 
+   fonctionnelle *)
+
+let get_f foncl = 
+  match (kind_of_term (def_of_const foncl)) with
+      Lambda (Name f, _, _) -> f  
+    |_ -> error "la fonctionnelle est mal definie";;
+
+
+let rec compute_le_proofs = function
+    [] -> assumption
+  | a::tl ->
+      tclORELSE assumption 
+	(tclTHENS
+	   (fun g -> 
+	      let le_trans = delayed_force le_trans in 
+	      let t_le_trans = compute_renamed_type g le_trans in 
+	      let m_id = 
+		let _,_,t = destProd t_le_trans in 
+		let na,_,_ = destProd t in 
+		Nameops.out_name na
+	      in
+	      apply_with_bindings
+		(le_trans,
+		 ExplicitBindings[dummy_loc,NamedHyp m_id,a])
+		g)
+	   [compute_le_proofs tl; 
+            tclORELSE (apply (delayed_force le_n)) assumption])
+
+let make_lt_proof pmax le_proof =
+  tclTHENS
+    (fun g -> 
+       let le_lt_trans = delayed_force le_lt_trans in 
+       let t_le_lt_trans = compute_renamed_type g le_lt_trans in 
+       let m_id = 
+	 let _,_,t = destProd t_le_lt_trans in 
+	 let na,_,_ = destProd t in 
+	 Nameops.out_name na
+       in
+       apply_with_bindings
+	 (le_lt_trans,
+	  ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g)
+    [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); 
+     tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];;
+
+let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
+  match cond_eqs with
+    [] -> tclIDTAC
+  | eq::eqs ->
+      (fun g -> 
+	 let t_eq = compute_renamed_type g (mkVar eq) in 
+	 let k_id,def_id = 
+	   let k_na,_,t = destProd t_eq in 
+	   let _,_,t  = destProd t in 
+	   let def_na,_,_ = destProd t in 
+	   Nameops.out_name k_na,Nameops.out_name def_na
+	 in
+	 tclTHENS
+	   (general_rewrite_bindings false []
+	      (mkVar eq,
+	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
+				dummy_loc, NamedHyp def_id, mkVar def]) false)
+	   [list_cond_rewrite k def pmax eqs le_proofs;
+            observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
+      ) 
+
+let rec introduce_all_equalities func eqs values specs bound le_proofs 
+    cond_eqs =
+  match specs with
+    [] -> 
+      fun g ->
+	let ids = pf_ids_of_hyps g in
+	let s_max = mkApp(delayed_force coq_S, [|bound|]) in
+	let k = next_global_ident_away true k_id ids in
+        let ids = k::ids in
+	let h' = next_global_ident_away true (h'_id) ids in
+        let ids = h'::ids in
+	let def = next_global_ident_away true def_id ids in
+	tclTHENLIST
+	  [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
+	   observe_tac "introduce_all_equalities_final intro k" (h_intro  k);
+	   tclTHENS
+	     (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k)))
+	     [
+	       tclTHENLIST[h_intro h';
+			   simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
+			   default_full_auto];
+	       tclIDTAC
+	     ];
+	   observe_tac "clearing k " (clear [k]);
+	   observe_tac "intros k h' def" (h_intros [k;h';def]);
+	   observe_tac "simple_iter" (simpl_iter onConcl);
+	   observe_tac "unfold functional" 
+	     (unfold_in_concl[([1],evaluable_of_global_reference func)]);
+	   observe_tac "rewriting equations" 
+	     (list_rewrite true eqs);
+           observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite  k def bound cond_eqs le_proofs);
+	   observe_tac "refl equal" (apply (delayed_force refl_equal))] g
+  | spec1::specs ->
+      fun g ->
+	let ids = ids_of_named_context (pf_hyps g) in
+	let p = next_global_ident_away true p_id ids in
+        let ids = p::ids in
+	let pmax = next_global_ident_away true pmax_id ids in
+        let ids = pmax::ids in
+	let hle1 = next_global_ident_away true hle_id ids in
+        let ids = hle1::ids in
+	let hle2 = next_global_ident_away true  hle_id ids in
+	let ids = hle2::ids in
+	let heq = next_global_ident_away true heq_id ids in
+	tclTHENLIST
+	  [simplest_elim (mkVar spec1);
+	   list_rewrite true eqs;
+	   h_intros [p; heq];
+	   simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|]));
+	   h_intros [pmax; hle1; hle2];
+	   introduce_all_equalities func eqs values specs 
+	     (mkVar pmax) ((mkVar pmax)::le_proofs)
+	     (heq::cond_eqs)] g;;
+    
+let string_match s =
+  if String.length s < 3 then failwith "string_match";
+  try 
+    for i = 0 to 3  do
+      if String.get s i <> String.get "Acc_" i then failwith "string_match"
+    done;
+  with Invalid_argument _ -> failwith "string_match"
+	  
+let retrieve_acc_var g = 
+  (* Julien: I don't like this version .... *) 
+  let hyps = pf_ids_of_hyps g  in 
+  map_succeed 
+    (fun id -> string_match (string_of_id id);id)
+    hyps 
+
+let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
+    eqs  hrec args values specs =
+    (match args with
+    [] -> 
+      tclTHENLIST
+	[observe_tac "split" (split(ImplicitBindings
+		 [context_fn (List.map mkVar (List.rev values))]));
+	 observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs
+	   (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
+  | arg::args ->
+      (fun g ->
+	let ids = ids_of_named_context (pf_hyps g) in
+	let rec_res = next_global_ident_away true rec_res_id ids in
+        let ids = rec_res::ids in
+	let hspec = next_global_ident_away true hspec_id ids in
+	let tac =  
+	  observe_tac "introduce_all_values" (
+	    introduce_all_values concl_tac is_mes acc_inv func context_fn eqs
+	      hrec args
+	      (rec_res::values)(hspec::specs)) in
+	(tclTHENS
+	   (observe_tac "elim h_rec" 
+	      (simplest_elim (mkApp(mkVar hrec, Array.of_list arg)))
+	   )
+	   [tclTHENLIST [h_intros [rec_res; hspec];
+			 tac]; 
+	    (tclTHENS
+		 (observe_tac "acc_inv" (apply (Lazy.force acc_inv)))
+		 [(* tclTHEN (tclTRY(list_rewrite true eqs)) *)
+		    (observe_tac "h_assumption" h_assumption)
+		 ;
+		  tclTHENLIST
+		    [
+		      tclTRY(list_rewrite true eqs);
+		      observe_tac "user proof" 
+			(fun g ->  
+			   tclUSER
+			     concl_tac
+			     is_mes
+			     (Some (hrec::hspec::(retrieve_acc_var g)@specs))
+			     g
+			)		     
+		    ]
+		 ]
+	    )
+	   ]) g)
+	
+    )
+ 
+	   
+let rec_leaf_terminate concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr =
+  match find_call_occs 0 (mkVar (get_f (constr_of_global func))) expr with
+  | context_fn, args ->
+      observe_tac "introduce_all_values" 
+	(introduce_all_values concl_tac is_mes acc_inv func context_fn eqs  hrec args  [] [])
+
+let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)  
+  (f_constr:constr) (func:global_reference) base_leaf rec_leaf = 
+  let rec proveterminate (eqs:constr list) (expr:constr)  =
+    try
+      (*  let _ = msgnl (str "entering proveterminate") in *)
+      let v =
+        match (kind_of_term expr) with
+	  Case (ci, t, a, l) -> 
+	  (match find_call_occs 0 f_constr a with
+	    _,[] ->
+	    (fun g -> 
+	      let destruct_tac, rev_to_thin_intro =
+                mkDestructEq rec_arg_id a g in 
+		tclTHENS destruct_tac
+		  (list_map_i 
+		    (fun i -> mk_intros_and_continue 
+				(List.rev rev_to_thin_intro) 
+				true 
+				proveterminate 
+				eqs
+				ci.ci_cstr_nargs.(i))
+		    0 (Array.to_list l)) g)
+		  | _, _::_ -> 
+		    (match find_call_occs  0 f_constr expr with
+	     	      _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr)
+		    | _, _:: _ -> 
+		      observe_tac "rec_leaf" 
+		      (rec_leaf is_mes acc_inv hrec  func eqs expr)))
+	  | _ ->
+            (match find_call_occs  0 f_constr expr with
+	      _,[] -> 
+	      (try observe_tac "base_leaf" (base_leaf func eqs expr)
+	       with e -> (msgerrnl (str "failure in base case");raise e ))
+	    | _, _::_ -> 
+	      observe_tac "rec_leaf"
+	        (rec_leaf is_mes acc_inv hrec func eqs expr)) in
+      v
+    with e -> begin msgerrnl(str "failure in proveterminate"); raise e end
+  in 
+  proveterminate 
+
+let hyp_terminates nb_args func = 
+  let a_arrow_b = arg_type (constr_of_global func) in 
+  let rev_args,b = decompose_prod_n nb_args a_arrow_b in 
+  let left = 
+    mkApp(delayed_force iter, 
+	  Array.of_list 
+	    (lift 5 a_arrow_b:: mkRel 3::
+	       constr_of_global func::mkRel 1::
+	       List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
+	    )
+	 )
+  in
+  let right = mkRel 5 in 
+  let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in
+  let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in
+  let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in
+  let nb_iter =
+    mkApp(delayed_force ex,
+	  [|delayed_force nat;
+	    (mkLambda 
+	       (Name
+		  p_id,
+		  delayed_force nat, 
+		  (mkProd (Name k_id, delayed_force nat, 
+			   mkArrow cond result))))|])in
+  let value = mkApp(delayed_force coq_sig, 
+		    [|b;
+		      (mkLambda (Name v_id, b, nb_iter))|]) in
+  compose_prod rev_args value
+	     
+
+
+let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = 
+  if is_mes 
+  then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof))
+  else tclUSER concl_tac is_mes names_to_suppress
+
+let termination_proof_header is_mes input_type ids args_id relation
+    rec_arg_num rec_arg_id tac wf_tac : tactic = 
+  begin 
+    fun g -> 
+      let nargs = List.length args_id in
+      let pre_rec_args = 
+	List.rev_map
+	  mkVar (fst (list_chop (rec_arg_num - 1) args_id)) 
+      in 
+      let relation = substl pre_rec_args relation in 
+      let input_type = substl pre_rec_args input_type in 
+      let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in 
+      let wf_rec_arg = 
+	next_global_ident_away true 
+	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
+	  (wf_thm::ids) 
+      in 
+      let hrec = next_global_ident_away true hrec_id
+	(wf_rec_arg::wf_thm::ids) in 
+      let acc_inv = 
+	  lazy (
+	    mkApp (
+	      delayed_force acc_inv_id,
+	      [|input_type;relation;mkVar rec_arg_id|]
+	    )
+	  )
+      in
+      tclTHEN
+	(h_intros args_id)
+	(tclTHENS
+	   (observe_tac 
+	      "first assert" 
+	      (assert_tac 
+		 true (* the assert thm is in first subgoal *)
+		 (Name wf_rec_arg) 
+		 (mkApp (delayed_force acc_rel,
+			 [|input_type;relation;mkVar rec_arg_id|])
+		 )
+	      )
+	   )
+	   [
+	     (* accesibility proof *) 
+	     tclTHENS 
+	       (observe_tac 
+		  "second assert" 
+		  (assert_tac 
+		     true 
+		     (Name wf_thm)
+		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
+		  )
+	       )
+	       [ 
+		 (* interactive proof that the relation is well_founded *)
+		 observe_tac "wf_tac" (wf_tac is_mes (Some args_id));
+		 (* this gives the accessibility argument *)
+		 observe_tac 
+		   "apply wf_thm" 
+		   (h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
+		   )
+	       ]
+	     ;
+	     (* rest of the proof *)
+	     tclTHENSEQ 
+	       [observe_tac "generalize" 
+		  (onNLastHyps (nargs+1)
+		     (fun (id,_,_) -> 
+			tclTHEN (h_generalize [mkVar id]) (h_clear false [id])
+		     ))
+	       ;
+		observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
+		h_intros args_id;
+		h_intro wf_rec_arg;
+		observe_tac "tac" (tac wf_rec_arg hrec acc_inv)
+	       ]
+	   ]
+	) g  
+  end
+
+
+
+let rec instantiate_lambda t l = 
+  match l with
+  | [] -> t
+  | a::l -> 
+      let (bound_name, _, body) = destLambda t in
+      instantiate_lambda (subst1 a body) l
+;;
+
+
+let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num  : tactic = 
+  begin 
+    fun g -> 
+      let ids = ids_of_named_context (pf_hyps g) in
+      let func_body = (def_of_const (constr_of_global func)) in
+      let (f_name, _, body1) = destLambda func_body in
+      let f_id =
+	match f_name with
+	  | Name f_id -> next_global_ident_away true f_id ids
+	  | Anonymous -> anomaly "Anonymous function"
+      in
+      let n_names_types,_ = decompose_lam_n nb_args body1 in 
+      let n_ids,ids = 
+	List.fold_left 
+	  (fun (n_ids,ids) (n_name,_) -> 
+	     match n_name with 
+	       | Name id -> 
+		   let n_id = next_global_ident_away true id ids in 
+		   n_id::n_ids,n_id::ids
+	       | _ -> anomaly "anonymous argument"
+	  )
+	  ([],(f_id::ids))
+	  n_names_types
+      in
+      let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
+      let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in 
+      termination_proof_header 
+	is_mes
+	input_type
+	ids
+	n_ids
+	relation 
+	rec_arg_num
+	rec_arg_id
+	(fun rec_arg_id hrec acc_inv g ->  
+           (proveterminate 
+	      [rec_arg_id]
+	      is_mes
+	      acc_inv 
+	      hrec
+	      (mkVar f_id)
+	      func
+	      base_leaf_terminate 
+	      (rec_leaf_terminate concl_tac)
+	      []
+	      expr
+	   )
+	     g 
+	)
+	(tclUSER_if_not_mes concl_tac)
+	g 
+  end
+
+let get_current_subgoals_types () = 
+  let pts =  get_pftreestate () in 
+  let _,subs = extract_open_pftreestate pts in 
+  List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs )
+
+let build_and_l l = 
+  let and_constr =  Coqlib.build_coq_and () in 
+  let conj_constr = coq_conj () in 
+  let mk_and p1 p2 = 
+    Term.mkApp(and_constr,[|p1;p2|]) in 
+  let rec f  = function 
+    | [] -> failwith "empty list of subgoals!" 
+    | [p] -> p,tclIDTAC,1 
+    | p1::pl -> 
+	let c,tac,nb = f pl in 
+	mk_and p1 c, 
+	tclTHENS
+	  (apply (constr_of_global conj_constr)) 
+	  [tclIDTAC;
+	   tac
+	  ],nb+1
+  in f l
+
+
+let is_rec_res id = 
+  let rec_res_name = string_of_id rec_res_id   in 
+  let id_name = string_of_id id in 
+  try 
+    String.sub id_name 0 (String.length rec_res_name) = rec_res_name 
+  with _ -> false
+
+let clear_goals = 
+  let rec clear_goal t = 
+    match kind_of_term t with 
+      | Prod(Name id as na,t,b) -> 
+	  let b' = clear_goal b in 
+	  if noccurn 1 b' && (is_rec_res id) 
+	  then pop b' 
+	  else if b' == b then t 
+	  else mkProd(na,t,b')
+      | _ -> map_constr clear_goal t
+  in 
+  List.map clear_goal 
+
+
+let build_new_goal_type () = 
+  let sub_gls_types = get_current_subgoals_types () in 
+  let sub_gls_types = clear_goals sub_gls_types in 
+  let res = build_and_l sub_gls_types in 
+  res
+  
+
+    (*
+let prove_with_tcc lemma _ : tactic = 
+  fun gls ->
+    let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in 
+    tclTHENSEQ 
+      [
+	h_generalize [lemma];
+	h_intro hid;
+	Elim.h_decompose_and (mkVar hid); 
+	gen_eauto(* default_eauto *) false (false,5) [] (Some [])
+	  (* 	      default_auto *)
+      ]
+      gls
+    *)
+      
+	     
+
+let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   = 
+  let current_proof_name = get_current_proof_name () in
+  let name = match goal_name with 
+    | Some s -> s 
+    | None   ->  
+	try (add_suffix current_proof_name "_subproof") 
+	with _ -> anomaly "open_new_goal with an unamed theorem"
+  in  
+  let sign = Global.named_context () in
+  let sign = clear_proofs sign in
+  let na = next_global_ident_away false name [] in
+  if occur_existential gls_type then
+    Util.error "\"abstract\" cannot handle existentials";
+  let hook _ _ = 
+    let opacity = 
+      let na_ref = Libnames.Ident (dummy_loc,na) in 
+      let na_global = Nametab.global na_ref in
+      match na_global with 
+	  ConstRef c -> 
+	    let cb = Global.lookup_constant c in 
+	    if cb.Declarations.const_opaque then true 
+	    else begin  match cb.const_body with None -> true | _ -> false end 
+	| _ -> anomaly "equation_lemma: not a constant"
+    in
+    let lemma = mkConst (Lib.make_con na) in 
+    ref_ := Some lemma ;
+    let lid = ref [] in 
+    let h_num = ref (-1) in 
+    Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
+    build_proof 
+      (  fun gls ->
+	   let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in 
+	   tclTHENSEQ 
+	     [
+	       h_generalize [lemma];
+	       h_intro hid;
+	       (fun g -> 
+		  let ids = pf_ids_of_hyps g in 
+		  tclTHEN
+		    (Elim.h_decompose_and (mkVar hid))
+		    (fun g -> 
+		       let ids' = pf_ids_of_hyps g in 
+		       lid := List.rev (list_subtract ids' ids);
+		       if !lid = [] then lid := [hid];
+(* 		       list_iter_i  *)
+(* 			 (fun i v ->  *)
+(* 			    msgnl (str "hyp" ++ int i ++ str " " ++  *)
+(* 				     Nameops.pr_id v ++ fnl () ++ fnl())) *)
+(* 			      !lid; *)
+		       tclIDTAC g
+		    )
+		    g
+	       ); 
+	     ] gls)
+      (fun g ->
+	 match kind_of_term (pf_concl g) with
+	   | App(f,_) when eq_constr f (well_founded ()) ->
+	       Auto.h_auto None [] (Some [])  g
+	   | _ ->
+	       incr h_num;
+	       tclTHEN
+		 (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+		 e_assumption
+      		 g)
+;
+    Command.save_named opacity;
+  in
+  start_proof
+    na
+    (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) 
+    sign
+    gls_type 
+    hook ;
+  by (
+    fun g -> 
+      tclTHEN 
+	(decompose_and_tac)
+	(tclORELSE 
+	(tclFIRST 
+	   (List.map
+	      (fun c -> 
+		 tclTHENSEQ
+		   [intros; 
+		    h_simplest_apply (interp_constr Evd.empty (Global.env()) c); 
+		    tclCOMPLETE Auto.default_auto
+		   ]
+	      )
+	      using_lemmas)
+	) tclIDTAC)
+	g);
+  try
+    by tclIDTAC; (* raises UserError _ if the proof is complete *)
+    if Flags.is_verbose () then (pp (Printer.pr_open_subgoals()))
+  with UserError _ -> 
+    defined ()
+  
+;;    
+
+
+let com_terminate 
+    tcc_lemma_name 
+    tcc_lemma_ref 
+    is_mes 
+    fonctional_ref
+    input_type
+    relation 
+    rec_arg_num
+    thm_name using_lemmas 
+    nb_args
+    hook =
+  let start_proof (tac_start:tactic) (tac_end:tactic) = 
+    let (evmap, env) = Command.get_current_context() in
+    start_proof thm_name
+      (Global, Proof Lemma) (Environ.named_context_val env)
+      (hyp_terminates nb_args fonctional_ref) hook;
+    by (observe_tac "starting_tac" tac_start);
+    by (observe_tac "whole_start" (whole_start tac_end nb_args is_mes fonctional_ref
+				   input_type relation rec_arg_num ))
+    
+  in
+  start_proof tclIDTAC tclIDTAC;
+  try 
+    let new_goal_type = build_new_goal_type () in 
+    open_new_goal start_proof using_lemmas tcc_lemma_ref
+      (Some tcc_lemma_name)
+      (new_goal_type)
+  with Failure "empty list of subgoals!" -> 
+    (* a non recursive function declared with measure ! *)
+    defined ()
+    
+
+    
+
+let ind_of_ref = function 
+  | IndRef (ind,i) -> (ind,i)
+  | _ -> anomaly "IndRef expected"
+
+let (value_f:constr list -> global_reference -> constr) =
+  fun al fterm ->
+    let d0 = dummy_loc in 
+    let rev_x_id_l =  
+      (
+	List.fold_left 
+	  (fun x_id_l _ -> 
+	     let x_id = next_global_ident_away true x_id x_id_l in 
+	     x_id::x_id_l
+	  )
+	  []
+	  al
+      )
+    in
+    let fun_body = 
+      RCases
+	(d0,RegularStyle,None,
+	 [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l),
+	  (Anonymous,None)],
+	 [d0, [v_id], [PatCstr(d0,(ind_of_ref 
+				     (delayed_force coq_sig_ref),1),
+			       [PatVar(d0, Name v_id);
+				PatVar(d0, Anonymous)],
+			       Anonymous)],
+	  RVar(d0,v_id)])
+    in
+    let value =
+      List.fold_left2 
+	(fun acc x_id a -> 
+	   RLambda
+      	     (d0, Name x_id, Explicit, RDynamic(d0, constr_in a),
+	      acc
+	     ) 
+	)
+	fun_body
+	rev_x_id_l
+	(List.rev al)
+    in
+    understand Evd.empty (Global.env()) value;;
+
+let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
+  fun f_id kind value ->
+    let ce = {const_entry_body = value;
+	      const_entry_type = None;
+	      const_entry_opaque = false;
+              const_entry_boxed = true} in
+      ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+
+let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
+  fun f_id kind input_type fterm_ref ->
+    declare_fun f_id kind (value_f input_type fterm_ref);;
+
+let rec n_x_id ids n =
+  if n = 0 then []
+  else let x = next_global_ident_away true x_id ids in
+          x::n_x_id (x::ids) (n-1);;
+
+let start_equation (f:global_reference) (term_f:global_reference) 
+  (cont_tactic:identifier list -> tactic) g =
+  let ids = pf_ids_of_hyps g in
+  let terminate_constr = constr_of_global term_f in 
+  let nargs = nb_prod (type_of_const terminate_constr) in 
+  let x = n_x_id ids nargs in
+  tclTHENLIST [
+    h_intros x;
+    unfold_in_concl [([], evaluable_of_global_reference f)];
+    observe_tac "simplest_case" 
+      (simplest_case (mkApp (terminate_constr,
+                             Array.of_list (List.map mkVar x))));
+    observe_tac "prove_eq" (cont_tactic x)] g;;
+
+let base_leaf_eq func eqs f_id g =
+  let ids = pf_ids_of_hyps g in
+  let k = next_global_ident_away true k_id ids in
+  let p = next_global_ident_away true p_id (k::ids) in
+  let v = next_global_ident_away true v_id (p::k::ids) in
+  let heq = next_global_ident_away true heq_id (v::p::k::ids) in
+  let heq1 = next_global_ident_away true heq_id (heq::v::p::k::ids) in
+  let hex = next_global_ident_away true hex_id (heq1::heq::v::p::k::ids) in
+    tclTHENLIST [
+      h_intros [v; hex]; 
+      simplest_elim (mkVar hex);
+      h_intros [p;heq1];
+      tclTRY
+	(rewriteRL 
+	   (mkApp(mkVar heq1, 
+		  [|mkApp (delayed_force coq_S, [|mkVar p|]);
+		    mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|])));
+      simpl_iter onConcl;
+      tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]);
+      list_rewrite true eqs;
+      apply (delayed_force refl_equal)] g;;
+
+let f_S t = mkApp(delayed_force coq_S, [|t|]);;
+
+
+let rec introduce_all_values_eq cont_tac functional termine 
+    f p heq1 pmax bounds le_proofs eqs ids =
+  function
+      [] ->
+       let heq2 = next_global_ident_away true heq_id ids in
+	tclTHENLIST
+	  [forward None (IntroIdentifier heq2)
+             (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
+           simpl_iter (onHyp heq2);
+           unfold_in_hyp [([1], evaluable_of_global_reference 
+                             (global_of_constr functional))]
+             (([], heq2), Tacexpr.InHyp);
+           tclTHENS
+	     (fun gls -> 
+		let t_eq = compute_renamed_type gls (mkVar heq2) in 
+		let def_id = 
+		  let _,_,t  = destProd t_eq in let def_na,_,_ = destProd t in 
+		  Nameops.out_name def_na
+		in
+		observe_tac "rewrite heq" (general_rewrite_bindings false []
+		(mkVar heq2,
+		 ExplicitBindings[dummy_loc,NamedHyp def_id,
+				  f]) false) gls)
+	     [tclTHENLIST
+		[observe_tac "list_rewrite" (list_rewrite true eqs);
+                 cont_tac pmax le_proofs];
+	      tclTHENLIST[apply (delayed_force le_lt_SS);
+			compute_le_proofs le_proofs]]]
+    | arg::args ->
+	let v' = next_global_ident_away true v_id ids in
+        let ids = v'::ids in
+	let hex' = next_global_ident_away true hex_id ids in
+        let ids = hex'::ids in
+	let p' = next_global_ident_away true p_id ids in
+        let ids = p'::ids in
+	let new_pmax = next_global_ident_away true pmax_id ids in
+        let ids = pmax::ids in
+	let hle1 = next_global_ident_away true hle_id ids in
+        let ids = hle1::ids in
+	let hle2 = next_global_ident_away true hle_id ids in
+        let ids = hle2::ids in
+	let heq = next_global_ident_away true heq_id ids in
+        let ids = heq::ids in
+	let heq2 = next_global_ident_away true heq_id ids in
+        let ids = heq2::ids in
+	tclTHENLIST
+	  [mkCaseEq(mkApp(termine, Array.of_list arg));
+	   h_intros [v'; hex'];
+	   simplest_elim(mkVar hex');
+	   h_intros [p'];
+	   simplest_elim(mkApp(delayed_force max_constr, [|mkVar pmax;
+							mkVar p'|]));
+	   h_intros [new_pmax;hle1;hle2];
+           introduce_all_values_eq 
+              (fun pmax' le_proofs'->
+		tclTHENLIST
+		  [cont_tac pmax' le_proofs';
+		   h_intros [heq;heq2];
+		   observe_tac ("rewriteRL " ^ (string_of_id heq2))
+                     (tclTRY (rewriteLR (mkVar heq2)));
+		   tclTRY (tclTHENS
+		     ( fun g -> 
+			 let t_eq = compute_renamed_type g (mkVar heq) in 
+			 let k_id,def_id = 
+			   let k_na,_,t = destProd t_eq in 
+			   let _,_,t  = destProd t in 
+			   let def_na,_,_ = destProd t in 
+			   Nameops.out_name k_na,Nameops.out_name def_na
+			 in
+			 let c_b = (mkVar heq,
+			    ExplicitBindings
+			      [dummy_loc, NamedHyp k_id,
+			       f_S(mkVar pmax');
+			       dummy_loc, NamedHyp def_id, f])
+			 in
+			   observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false []
+								       c_b false))
+			     g
+		     )
+		     [tclIDTAC;
+		      tclTHENLIST
+			[apply (delayed_force le_lt_n_Sm);
+			 compute_le_proofs le_proofs']])])
+	     functional termine f p heq1 new_pmax
+	     (p'::bounds)((mkVar pmax)::le_proofs) eqs
+             (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args]
+  
+
+let rec_leaf_eq termine f ids functional eqs expr fn args =
+  let p = next_global_ident_away true p_id ids in
+  let ids = p::ids in
+  let v = next_global_ident_away true v_id ids in
+  let ids = v::ids in
+  let hex = next_global_ident_away true hex_id ids in
+  let ids = hex::ids in
+  let heq1 = next_global_ident_away true heq_id ids in
+  let ids = heq1::ids in
+  let hle1 = next_global_ident_away true hle_id ids in
+  let ids = hle1::ids in
+    tclTHENLIST
+      [observe_tac "intros v hex" (h_intros [v;hex]);
+       simplest_elim (mkVar hex);
+       h_intros [p;heq1];
+       h_generalize [mkApp(delayed_force le_n,[|mkVar p|])];
+       h_intros [hle1];
+       observe_tac "introduce_all_values_eq" (introduce_all_values_eq
+	 (fun _ _ -> tclIDTAC)
+	 functional termine f p heq1 p [] [] eqs ids args);
+       observe_tac "failing here" (apply (delayed_force refl_equal))]
+
+let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
+    (eqs:constr list) (expr:constr) =
+(*   tclTRY *)
+  (match kind_of_term expr with
+     Case(ci,t,a,l) ->
+     (match find_call_occs 0 f a with
+	_,[] -> 
+	(fun g -> 
+	  let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in 
+	  tclTHENS
+            destruct_tac
+	    (list_map_i  
+	       (fun i -> mk_intros_and_continue
+                          (List.rev rev_to_thin_intro) true 
+			  (prove_eq termine f functional)  
+			  eqs ci.ci_cstr_nargs.(i))
+	       0 (Array.to_list l)) g)
+	   | _,_::_ ->
+	      (match find_call_occs 0 f expr with
+		_,[] -> base_leaf_eq functional eqs f
+	      | fn,args ->
+	        fun g ->
+		  let ids = ids_of_named_context (pf_hyps g) in
+	          rec_leaf_eq termine f ids
+		    (constr_of_global functional)
+		    eqs expr fn args g))
+       | _ -> 
+	   (match find_call_occs 0 f expr with
+		_,[] -> base_leaf_eq functional eqs f
+	      | fn,args ->
+		  fun g ->
+		    let ids = ids_of_named_context (pf_hyps g) in
+		    observe_tac "rec_leaf_eq" (rec_leaf_eq  
+		      termine f ids (constr_of_global functional)
+		      eqs expr fn args) g));;
+
+let (com_eqn : identifier ->
+       global_reference -> global_reference -> global_reference
+	 -> constr -> unit) =
+  fun eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
+    let opacity = 
+      match terminate_ref with 
+	| ConstRef c -> 	      
+	    let cb = Global.lookup_constant c in 
+	    if cb.Declarations.const_opaque then true 
+	    else begin match cb.const_body with None -> true | _ -> false end 
+	| _ -> anomaly "terminate_lemma: not a constant"
+    in 
+    let (evmap, env) = Command.get_current_context() in
+    let f_constr = (constr_of_global f_ref) in
+    let equation_lemma_type = subst1 f_constr equation_lemma_type in
+    (start_proof eq_name (Global, Proof Lemma)
+       (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+     by
+       (start_equation f_ref terminate_ref
+	  (fun  x ->
+	     prove_eq 
+	       (constr_of_global terminate_ref)
+	       f_constr 
+	       functional_ref
+	       []
+	       (instantiate_lambda
+	       	  (def_of_const (constr_of_global functional_ref))
+	       	  (f_constr::List.map mkVar x)
+	       )
+	  )
+       );
+(*      (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
+(*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
+     Flags.silently (fun () ->Command.save_named opacity) () ;  
+(*      Pp.msgnl (str "eqn finished"); *)
+    
+    );;
+
+let nf_zeta env =       
+  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+    env
+    Evd.empty
+
+let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq 
+    generate_induction_principle using_lemmas : unit =
+  let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
+  let env = push_named (function_name,None,function_type) (Global.env()) in
+(*   Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
+  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in 
+(*   Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
+  let res_vars,eq' = decompose_prod equation_lemma_type in 
+  let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
+  let eq' = nf_zeta env_eq' eq'  in 
+  let res = 
+(*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
+(*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
+(*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
+    match kind_of_term eq' with 
+      | App(e,[|_;_;eq_fix|]) -> 
+	  mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
+      | _ -> failwith "Recursive Definition (res not eq)"
+  in
+  let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in 
+  let (_, rec_arg_type, _) = destProd function_type_before_rec_arg in
+  let arg_types = List.rev_map snd (fst (decompose_prod_n (List.length res_vars) function_type)) in
+  let equation_id = add_suffix function_name "_equation" in
+  let functional_id =  add_suffix function_name "_F" in
+  let term_id = add_suffix function_name "_terminate" in
+  let functional_ref = declare_fun functional_id (IsDefinition Definition) res in
+  let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in 
+  let relation = 
+    interp_constr
+      Evd.empty 
+      env_with_pre_rec_args
+      r
+  in 
+  let tcc_lemma_name = add_suffix function_name "_tcc" in
+  let tcc_lemma_constr = ref None in 
+(*   let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
+  let hook _ _ =   
+    let term_ref = Nametab.locate (make_short_qualid term_id) in
+    let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
+(*     message "start second proof"; *)
+    let stop = ref false in 
+    begin 
+      try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
+      with e -> 
+	begin 
+	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+	  then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e)
+	  else anomaly "Cannot create equation Lemma"
+	  ;
+(* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
+	  stop := true;
+	end
+    end;
+    if not !stop
+    then
+      let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+      let f_ref = destConst (constr_of_global f_ref) 
+      and functional_ref = destConst (constr_of_global functional_ref) 
+      and eq_ref = destConst (constr_of_global eq_ref) in
+      generate_induction_principle f_ref tcc_lemma_constr
+	functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
+      if Flags.is_verbose ()
+      then msgnl (h 1 (Ppconstr.pr_id function_name ++ 
+			 spc () ++ str"is defined" )++ fnl () ++ 
+		    h 1 (Ppconstr.pr_id equation_id ++ 
+			   spc () ++ str"is defined" )
+		 )
+  in
+  try 
+    com_terminate 
+      tcc_lemma_name
+      tcc_lemma_constr
+      is_mes functional_ref
+      rec_arg_type
+      relation rec_arg_num
+      term_id
+      using_lemmas
+      (List.length res_vars)
+      hook
+  with e -> 
+    begin
+      ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
+(*       anomaly "Cannot create termination Lemma" *)
+      raise e
+    end
+
+
+
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
deleted file mode 100644
index 4dc4f1fd3..000000000
--- a/contrib/funind/tacinv.ml4
+++ /dev/null
@@ -1,869 +0,0 @@
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(*s FunInv Tactic: inversion following the shape of a function.  *)
-
-(* Deprecated: see indfun_main.ml4 instead *)
-
-(* Don't delete this file yet, it may be used for other purposes *)
-
-(*i*)
-open Termops
-open Equality
-open Names
-open Pp
-open Tacmach
-open Proof_type
-open Tacinterp
-open Tactics
-open Tacticals
-open Term
-open Util
-open Printer
-open Reductionops
-open Inductiveops
-open Coqlib
-open Refine
-open Typing
-open Declare
-open Decl_kinds
-open Safe_typing
-open Vernacinterp
-open Evd
-open Environ
-open Entries
-open Setoid_replace
-open Tacinvutils
-(*i*)
-
-module Smap = Map.Make(struct type t = constr let compare = compare end)
-let smap_to_list m = Smap.fold (fun c cb l -> (c,cb)::l) m []
-let merge_smap m1 m2 = Smap.fold (fun c cb m -> Smap.add c cb m) m1 m2
-let rec listsuf i l = if i<=0 then l else listsuf (i-1) (List.tl l)
-let rec listpref i l = if i<=0 then [] else List.hd l :: listpref (i-1) (List.tl l)
-let rec split3 l = 
-  List.fold_right (fun (e1,e2,e3) (a,b,c) -> (e1::a),(e2::b),(e3::c)) l ([],[],[])
-
-let mkthesort = mkProp (* would like to put Type here, but with which index? *)
-
-(*  this is the prefix used to name equality hypothesis generated by
-    case analysis*)
-let equality_hyp_string = "_eg_"
-
-(* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur
-   initiale au debut de l'appel a la fonction proofPrinc: 1. *)
-let nthhyp = ref 1
-
-let debug i = prstr ("DEBUG "^ string_of_int i ^"\n")
-let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2)
-(* Operations on names *)
-let id_of_name = function
-    Anonymous -> id_of_string "H"
-  | Name id   -> id;;
-let string_of_name nme = string_of_id (id_of_name nme)
- (*end debugging *)
-
-(*s specific manipulations on constr *)
-let lift1_leqs leq=
- List.map 
-  (function (r,(typofg,g,d)) 
-      -> lift 1 r, (lift 1 typofg, lift 1 g , lift 1 d)) leq
-
-let lift1_relleqs leq= List.map (function (r,x) -> lift 1 r,x) leq
-
-(* WARNING: In the types, we don't lift the rels in the type. This is
-   intentional. Use with care. *)
-let lift1_lvars lvars= List.map 
- (function x,(nme,c) -> lift 1 x, (nme, (*lift 1*) c)) lvars
-
-let pop1_levar levars = List.map (function ev,tev -> ev, popn 1 tev) levars
-
-
-let rec add_n_dummy_prod t n = 
- if n<=0 then t
- else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkthesort t) (n-1)
-
-(* [add_lambdas t gl [csr1;csr2...]] returns [[x1:type of csr1]
-   [x2:type of csr2] t [csr <- x1 ...]], names of abstracted variables
-   are not specified *)
-let rec add_lambdas t gl lcsr =
- match lcsr with
-  | [] -> t
-  | csr::lcsr' -> 
-     let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
-     lambda_id hyp_csr hyptyp (add_lambdas t gl lcsr')
-
-(* [add_pis t gl [csr1;csr2...]] returns ([x1] :type of [csr1]
-   [x2]:type of csr2) [t]*)
-let rec add_pis t gl lcsr =
- match lcsr with
-  | [] -> t
-  | csr::lcsr' -> 
-     let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
-     prod_id hyp_csr hyptyp (add_pis t gl lcsr')
-
-let mkProdEg teq eql eqr concl =
- mkProd (name_of_string "eg", mkEq teq eql eqr, lift 1 concl)
-
-let eqs_of_beqs x = 
- List.map (function (_,(a,b,c)) -> (Anonymous, mkEq a b c)) x
-
-
-let rec eqs_of_beqs_named_aux s i l =
- match l with 
-  | [] -> []
-  | (r,(a,b,c))::l' -> 
-     (Name(id_of_string (s^ string_of_int i)), mkEq a b c)
-     ::eqs_of_beqs_named_aux s (i-1) l'
-
-
-let eqs_of_beqs_named s l = eqs_of_beqs_named_aux s (List.length l) l
-
-let rec patternify ltypes c nme =
- match ltypes with
-  | [] -> c
-  | (mv,t)::ltypes' -> 
-     let c'= substitterm 0 mv (mkRel 1) c in
-     let tlift = lift (List.length ltypes') t in
-     let res = 
-      patternify ltypes' (mkLambda (newname_append nme "rec", tlift, c')) nme in
-     res
-
-let rec npatternify ltypes c =
- match ltypes with
-  | [] -> c
-  | (mv,nme,t)::ltypes' -> 
-     let c'= substitterm 0 mv (mkRel 1) c in
-     let tlift = lift (List.length ltypes') t in
-     let res = 
-      npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in
-     res
-
-(* fait une application (c m1 m2...mn, où mi est une evar, on rend également
-   la liste des evar munies de leur type) *)
-let rec apply_levars c lmetav =
- match lmetav with
-  | [] -> [],c
-  | (i,typ) :: lmetav' -> 
-     let levars,trm = apply_levars c lmetav' in
-     let exkey = mknewexist() in
-     ((exkey,typ)::levars),  applistc trm [mkEvar exkey]
-      (* EXPERIMENT le refine est plus long si on met un cast:
-         ((exkey,typ)::levars), mkCast ((applistc trm [mkEvar exkey]),typ) *)
-
-
-let prod_change_concl c newconcl = 
- let lv,_ = decompose_prod c in prod_it  newconcl lv
-
-let lam_change_concl c newconcl = 
- let lv,_ = decompose_prod c in lam_it newconcl lv
-
-
-let rec mkAppRel c largs n =
- match largs with
-  | [] -> c
-  | arg::largs' -> 
-     let newc = mkApp (c,[|(mkRel n)|]) in mkAppRel newc largs' (n-1)
-
-let applFull c typofc =
- let lv,t = decompose_prod typofc in 
- let ltyp = List.map fst lv in 
- let res = mkAppRel c ltyp (List.length ltyp) in
- res
-
-(* Take two terms with same structure and return a map of deBruijn from the
-   first to the second. Only DeBruijn should be different between the two
-   terms. *)
-let rec build_rel_map typ type_of_b = 
- match (kind_of_term typ), (kind_of_term type_of_b) with
-    Evar _ , Evar _  -> Smap.empty
-  | Const c1, Const c2  when c1=c2 -> Smap.empty
-  | Ind c1, Ind c2 when c1=c2 -> Smap.empty
-  | Rel i, Rel j when i=j -> Smap.empty
-  | Rel i, Rel j -> Smap.add typ type_of_b Smap.empty
-  | Prod (name,c1,c2), Prod (nameb,c1b,c2b) -> 
-     let map1 = build_rel_map c1 c1b in
-     let map2 = build_rel_map (pop c2) (pop c2b) in
-     merge_smap map1 map2
-  | App (f,args), App (fb,argsb) when Array.length args = Array.length argsb ->
-     build_rel_map_list (Array.to_list args) (Array.to_list argsb)
-  | _,_ -> failwith ("Could not generate case annotation. "^
-    "Incompatibility between annotation and actual type")
-
-and build_rel_map_list ltyp ltype_of_b =
- List.fold_left2 (fun a b c -> merge_smap a (build_rel_map b c))
-  Smap.empty ltyp ltype_of_b
-
-
-(*s Use (and proof) of the principle *)
-
-(* This is the type of the argument of [proofPrinc] *)
-
-type mimickinfo =
-    {
-     concl: constr; (* conclusion voulue, cad (xi:ti)gl, ou gl est le but a
-                       prouver, et xi:ti correspondent aux arguments donnés à
-                       la tactique.  On enlèvera un produit à chaque fois
-                       qu'on rencontrera un binder, sans lift ou pop.
-                       Initialement: une seule conclusion, puis specifique à
-                       chaque branche. *)
-     absconcl: constr array; (* conclusions patternisées pour pouvoir être
-                                appliquées = un predicat pour chaque fixpt
-                                mutuel. *)
-     mimick: constr; (* le terme qu'on imite. On plongera  dedans au fur et
-                        à mesure, sans lift ni pop. *)
-     env: env; (* The global typing environment, we will add thing in it when
-                  going inside the term (push_rel, push_rec_types) *)
-     sigma: Evd.evar_map; 
-     nmefonc: constr array; (* la constante correspondant à la fonction
-                               appelée, permet de remplacer les appels
-                               recursifs par des appels à la constante
-                               correspondante (non pertinent (et inutile) si
-                               on permet l'appel de la tactique sur une terme
-                               donné directement (au lieu d'une constante
-                               comme pour l'instant)). *)
-     fonc: int * int; (* bornes des indices des variable correspondant aux
-                         appels récursifs (plusieurs car fixp.  mutuels),
-                         utile pour reconnaître les appels récursifs
-                         (ATTENTION: initialement vide, reste vide tant qu'on
-                         n'est pas dans un fix).  *)
-     doeqs: bool; (* this reference is to toggle building of equalities during
-                    the building of the principle (default is true) *)
-     fix: bool; (* did I already went through a fix or case constr? lambdas
-                  found before a case or a fix are treated as parameters of
-                  the induction principle *)
-     lst_vars: (constr*(name*constr)) list ; (* Variables rencontrées jusque là *)
-     lst_eqs: (Term.constr * (Term.constr * Term.constr * Term.constr)) list ; 
-                                   (* liste d'équations engendrées au cours du
-                                      parcours, cette liste grandit à chaque
-                                      case, et il faut lifter le tout à chaque
-                                      binder *)
-     lst_recs: constr list ; (* appels récursifs rencontrés jusque là *)
-    }
-
-(* This is the return type of [proofPrinc] *)
-type 'a funind = (* 'A = CONTR  OU  CONSTR ARRAY *)
-    {
-
-     princ:'a; (* le (ou les) principe(s) demandé(s), il contient des meta
-                  variables représentant soit des trous à prouver plus tard,
-                  soit les conclusions à compléter avant de rendre le terme
-                  (suivant qu'on utilise le principe pour faire refine ou
-                  functional scheme). Il y plusieurs conclusions si plusieurs
-                  fonction mutuellement récursives) voir la suite. *)
-     evarlist: (constr*Term.types) list; (* [(ev1,tev1);(ev2,tev2)...]]
-                                            l'ensemble des meta variables
-                                            correspondant à des trous. [evi]
-                                            est la meta variable, [tevi] est
-                                            son type. *)
-     hypnum: (int*int*int) list; (* [[(in,jn,kn)...]] sont les nombres
-                                    respectivement de variables, d'équations,
-                                    et d'hypothèses de récurrence pour le but
-                                    n. Permet de faire le bon nombre d'intros
-                                    et des rewrite au bons endroits dans la
-                                    suite. *)
-     mutfixmetas: constr array ; (* un tableau de meta variables correspondant
-                                    à chacun des prédicats mutuellement
-                                    récursifs construits. *)
-     conclarray: types array; (* un tableau contenant les conclusions
-                                 respectives de chacun des prédicats
-                                 mutuellement récursifs. Permet de finir la
-                                 construction du principe. *)
-     params:(constr*name*constr) list; (* [[(metavar,param,tparam)..]] la
-                                          liste des paramètres (les lambdas
-                                          au-dessus du fix) du fixpoint si
-                                          fixpoint il y a, le paramètre est
-                                          une meta var, dont on stocke le nom
-                                          et le type. TODO: utiliser la
-                                          structure adequat? *)
-    }
-
-
-
-let empty_funind_constr =
-    {
-     princ = mkProp;
-     evarlist = [];
-     hypnum = [];
-     mutfixmetas = [||];
-     conclarray = [||];
-     params = []
-    }
-
-let empty_funind_array =
-    { empty_funind_constr with
-     princ = [||];
-    }
-
-(* Replace the calls to the function (recursive calls) by calls to the
-   corresponding constant  *)
-let replace_reccalls mi b =
- let d,f = mi.fonc in 
- let res = ref b in
- let _ = for i = d to f do 
-   res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in
- !res
- 
-
-
-(* collects all information of match branches stored in [l] *)
-let rec collect_cases l =
- match l with
-  | [||] -> empty_funind_array
-  | arr -> 
-     let x = arr.(0) in
-     let resrec = collect_cases (Array.sub arr 1 (Array.length arr - 1)) in
-     { x with
-      princ= Array.append [|x.princ|] resrec.princ;
-      evarlist = x.evarlist@resrec.evarlist;
-      hypnum = x.hypnum@resrec.hypnum;
-     }
-
-let collect_pred l = 
- let l1,l2,l3 = split3 l in
- Array.of_list l1 , Array.of_list l2 , Array.of_list l3
-
-
-(* [build_pred n tarr] builds the right predicates for each element of [tarr]
-   (of type: [type array] of size [n]). Return the list of triples: 
-   (?i , 
-   fun (x1:t1) ... (xn:tn) => (?i x1...xn) ,
-   forall (x1:t1) ... (xn:tn), (?i x1...xn)),
-   where ti's are deduced from elements of tarr, which are of the form:
-   t1 -> t2 -> ... -> tn -> <nevermind>. *)
-let rec build_pred n tarr =
- if n >= Array.length tarr (* iarr *) then []
- else
-   let ftyp = Array.get tarr n in
-   let gl = mknewmeta() in
-   let gl_app = applFull gl ftyp in
-   let pis = prod_change_concl ftyp gl_app in
-   let gl_abstr = lam_change_concl ftyp gl_app in
-   (gl,gl_abstr,pis):: build_pred (n+1) tarr
-
-
-let heq_prefix = "H_eq_"
-
-type kind_of_hyp = Var | Eq  (*| Rec*)
-
-(* the main function, build the principle by exploring the term and reproduce
-   the same structure. *)
-let rec proofPrinc mi: constr funind =
- match kind_of_term mi.mimick with
-    (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to point on
-       the name of recursive calls *) 
-  | Fix((iarr,i),(narr,tarr,carr)) -> 
-     (* We construct the right predicates for each mutual fixpt *)
-     let evararr,newabsconcl,pisarr = collect_pred (build_pred 0 tarr) in
-     let newenv = push_rec_types (narr,tarr,carr) mi.env in
-     let anme',aappel_rec,llevar,llposeq = 
-      collect_fix mi 0 iarr narr carr pisarr newabsconcl newenv in
-     let anme = Array.map (fun nme -> newname_append nme "_ind") anme' in
-     { 
-      princ = mkFix((iarr,i),(anme, pisarr,aappel_rec));
-      evarlist= pop1_levar llevar; (* llevar are put outside the fix, so we pop 1 *)
-      hypnum = llposeq;
-      mutfixmetas = evararr;
-      conclarray = pisarr;
-      params = []
-     }
-  (* <pcase> Cases b of arrPt end.*)
-  | Case (cinfo, pcase, b, arrPt) -> 
-     let prod_pcase,_ = decompose_lam pcase in
-     let _nmeb,_ = List.hd prod_pcase in
-     let newb'= apply_leqtrpl_t b mi.lst_eqs in
-     let type_of_b = Typing.type_of mi.env mi.sigma b in
-     (* Replace the recursive calls to the function by calls to the constant *)
-     let newb = replace_reccalls mi newb' in     
-     let cases = collect_cases (Array.mapi (fold_proof mi b type_of_b newb) arrPt) in
-     (* the match (case) annotation must be transformed, see [build_pcase] below *)
-     let newpcase = build_pcase mi pcase b type_of_b newb in
-     let trm' = mkCase (cinfo,newpcase,newb, cases.princ) in
-    { cases with
-     princ = if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) else trm';
-     params = [] (* FIX: fix parms here (fixpt inside a match)*)
-    }
-
-
-  | Lambda(nme, typ, cstr) ->
-     let _, _, cconcl = destProd mi.concl in
-     let d,f=mi.fonc in
-     let newenv = push_rel (nme,None,typ) mi.env in
-     let newlst_var = (* if this lambda is a param, then don't add it here *)
-      if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars mi.lst_vars
-      else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars mi.lst_vars in
-     let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv;
-      fonc = (if d > 0 then d+1 else 0) , (if f > 0 then f+1 else 0);
-      lst_vars = newlst_var ; lst_eqs = lift1_leqs mi.lst_eqs;
-      lst_recs = lift1L mi.lst_recs} in
-     let resrec = proofPrinc newmi in
-     (* are we inside a fixpoint or a case? then this is a normal lambda *)
-     if mi.fix 
-     then { resrec with princ = mkLambda (nme,typ,resrec.princ) ; params = [] }
-     else (* otherwise this is a parameter *)
-       let metav = mknewmeta() in
-       let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
-       { resrec with
-        princ = substmeta resrec.princ;
-        evarlist = List.map (fun (ev,tev) -> ev, substmeta tev) resrec.evarlist;
-        conclarray = Array.map substmeta resrec.conclarray;
-        params = (metav,nme,typ) :: resrec.params
-       }
-
-
-  | LetIn(nme,cstr1, typ, cstr) ->
-     failwith ("I don't deal with let ins yet. "^
-				 "Please expand them before applying this function.")
-
-  | u -> 
-     let varrels = List.rev (List.map fst mi.lst_vars) in
-     let varnames = List.map snd mi.lst_vars in
-     let nb_vars = List.length varnames in
-     let nb_eqs = List.length mi.lst_eqs in
-     let _eqrels = List.map fst mi.lst_eqs in
-     (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
-        trouvés dans les let in et les Cases avec ceux trouves dans u (ie
-        mi.mimick). *)
-     (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
-     let terms_recs = mi.lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
-     (*c construction du terme: application successive des variables, des
-       egalites et des appels rec, a la variable existentielle correspondant a
-       l'hypothese de recurrence en cours. *)
-     (* d'abord, on fabrique les types des appels recursifs en replacant le nom
-        de des fonctions par les predicats dans [terms_recs]: [(f_i t u v)]
-        devient [(P_i t u v)] *)
-     (* TODO optimiser ici: *)
-     let appsrecpred = exchange_reli_arrayi_L mi.absconcl mi.fonc terms_recs in
-     let typeofhole''  = prod_it_anonym_lift mi.concl appsrecpred in
-     let typeofhole    = prodn nb_vars varnames typeofhole'' in
-     (* Un bug de refine m'oblige à mettre ici un H (meta variable à ce point,
-        mais remplacé par H avant le refine) au lieu d'un '?', je mettrai les
-        '?'  à la fin comme ça [(([H1,H2,H3...] ...) ? ? ?)] *)
-     let newmeta = mknewmeta() in
-     let concl_with_var = applistc newmeta varrels in
-     let conclrecs = applistc concl_with_var terms_recs in
-     { empty_funind_constr with
-      princ = conclrecs;
-      evarlist = [ newmeta , typeofhole ];
-      hypnum = [ nb_vars , List.length terms_recs , nb_eqs ];
-      conclarray = mi.absconcl;
-     }
-
-     
-(* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant
-   l'annotation de type du case [pcase] contient des lambdas supplémentaires
-   en tête. Je les récupère dans la variable [suppllam_pcase]. Le problème est
-   que la conclusion de l'annotation du nouveauacse doit faire référence à ces
-   variables plutôt qu'à celle de l'exterieur. Ce qui suit permet de changer
-   les reference de newpcase' pour pointer vers les lambda du piquant. On
-   procède comme suit: on repère les rels qui pointent à l'interieur de
-   l'annotation dans la fonction initiale et on les relie à celle du type
-   voulu pour le case, pour ça ([build_rel_map]) on parcourt en même temps le
-   dernier lambda du piquant ([typ]) (qui contient le type de l'argument du
-   case) et le type attendu pour le case ([type_of_b]) et on construit un
-   map. Ensuite on remplace les rels correspondant dans la preuve construite
-   en suivant le map. *)
-     
-and build_pcase mi pcase b type_of_b newb =
-     let prod_pcase,_ = decompose_lam pcase in
-     let nme,typ = List.hd prod_pcase in
-     (* je remplace b par rel1 (apres avoir lifte un coup) dans la future
-        annotation du futur case: ensuite je mettrai un lambda devant *)
-     let typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 mi.concl) in
-     let suppllam_pcase = List.tl prod_pcase in
-     let suppllam_pcasel = List.length suppllam_pcase  in
-     let rel_smap = 
-      if suppllam_pcasel=0 then Smap.empty else (* FIX: is this test necessary ? *)
-        build_rel_map (lift suppllam_pcasel type_of_b) typ in
-     let newpcase''' =  
-      Smap.fold (fun e e' acc -> substitterm 0 e (lift 1 e') acc)
-       rel_smap typeof_case'' in
-     let neweq = mkEq (lift (suppllam_pcasel + 1) type_of_b) 
-      (lift (suppllam_pcasel + 1) newb) (mkRel 1) in
-     let newpcase'' = 
-      if mi.doeqs 
-      then mkProd (name_of_string "eg", neweq, lift 1 newpcase''') 
-      else newpcase''' in
-     (* construction du dernier lambda du piquant. *)
-     let newpcase' = mkLambda (newname_append nme "_ind" ,typ, newpcase'') in
-     (* ajout des lambdas supplémentaires (type dépendant) du piquant. *)
-     lamn suppllam_pcasel suppllam_pcase newpcase'
-
-
-(* [fold_proof mi b typeofb newb l n] rend le resultat de l'appel recursif sur
-   cstr (correpsondant au ième elt de [arrPt] ci-dessus et donc au ième
-   constructeur de [typeofb]), appele avec les bons arguments: [mi.concl]
-   devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments
-   du constructeur considéré, et [concl'] est [mi.concl] ou l'on a réécrit [b]
-   en ($c_n$ [rel1]...). *)
-and fold_proof mi b type_of_b newb i cstr = 
- let new_lst_recs = mi.lst_recs @ hdMatchSub_cpl b mi.fonc in
- (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3
-    x2 x1... ], sans quoi les annotations ne sont plus coherentes *)
- let cstr_appl,nargs = nth_dep_constructor type_of_b i in
- let concl'' = 
-  substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in
- let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in
- let concl_dummy = add_n_dummy_prod concl'' nargs in
- let lsteqs_rew = apply_eq_leqtrpl mi.lst_eqs neweq in
- let new_lsteqs = (mkRel (-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in
- let a',a'' = decompose_lam_n nargs cstr in
- let newa'' = 
-  if mi.doeqs 
-  then mkLambda (name_of_string heq_prefix,lift nargs neweq,lift 1 a'') 
-  else a'' in
- let newmimick = lamn nargs a' newa'' in
- let b',b'' = decompose_prod_n nargs concl_dummy in
- let newb'' = 
-  if mi.doeqs 
-  then mkProd (name_of_string heq_prefix,lift nargs neweq,lift 1 b'')
-  else b'' in
- let newconcl = prodn nargs b' newb'' in
- let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true; 
-  lst_eqs= new_lsteqs; lst_recs = new_lst_recs} in
- proofPrinc newmi 
-
-
-and collect_fix mi n iarr narr carr pisarr newabsconcl newenv =
- if n >= Array.length iarr then [||],[||],[],[]
- else
-   let nme = Array.get narr n in
-   let c = Array.get carr n in
-   (* rappelle sur le sous-terme, on ajoute un niveau de
-      profondeur (lift) parce que Fix est un binder. *)
-   let newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl;
-    mimick=c; fonc=(1,((Array.length iarr)));env=newenv;fix=true;
-    lst_vars=lift1_lvars mi.lst_vars; lst_eqs=lift1_leqs mi.lst_eqs; 
-    lst_recs= lift1L mi.lst_recs;} in
-   let resrec = proofPrinc newmi  in
-   let lnme,lappel_rec,llevar,llposeq = 
-    collect_fix mi (n+1) iarr narr carr pisarr newabsconcl newenv in
-   Array.append [|nme|] lnme , Array.append [|resrec.princ|] lappel_rec
-    , (resrec.evarlist@llevar) , (resrec.hypnum@llposeq)
-
-let mkevarmap_aux ex = let x,y = ex in	(mkevarmap_from_listex x),y
-
-
-(* TODO: deal with any term, not only a constant. *)
-let interp_fonc_tacarg fonctac gl =
- (* [fonc] is the constr corresponding to fontact not unfolded,
-    if [fonctac] is a (qualified) name then this is a [const] ?. *)
-(*  let fonc = constr_of_Constr fonctac in *)
- (* TODO: replace the [with _ -> ] by something more precise in
-    the following. *)
- (* [def_fonc] is the definition of fonc. TODO: We should do this only
-    if [fonc] is a const, and take [fonc] otherwise.*)
- try fonctac, pf_const_value gl (destConst fonctac)
- with _ -> failwith ("don't know how to deal with this function "
- ^"(DEBUG:is it a constante?)")
-
-
-
-
-(* [invfun_proof fonc  def_fonc  gl_abstr pis]  builds  the principle,
-   following  the shape  of   [def_fonc],    [fonc]  is the      constant
-   corresponding to [def_func] (or a reduced form of  it ?), gl_abstr and
-   pis are the goal to be proved, of the form [x,y...]g and (x.y...)g.
-
-   This function calls the big function proofPrinc. *)
-
-let invfun_proof fonc def_fonc gl_abstr pis env sigma =
- let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env;
- sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false ; 
- lst_vars = []; lst_eqs = []; lst_recs = []} in
- proofPrinc mi
-
-(* Do intros [i] times, then do rewrite on all introduced hyps which are called
-   like [heq_prefix], FIX: have another filter than the name. *)
-let rec iterintro i = 
- if i<=0 then tclIDTAC else 
-   tclTHEN
-    (tclTHEN 
-     intro
-     (iterintro (i-1)))
-    (fun gl -> 
-     (tclREPEAT 
-      (tclNTH_HYP i
-       (fun hyp -> 
-        let hypname = (string_of_id (destVar hyp)) in
-        let sub = 
-         try String.sub hypname 0 (String.length heq_prefix)
-         with _ -> "" (* different than [heq_prefix] *) in
-        if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite"))
-      )) gl)
-
-
-(* 
-       (fun hyp gl -> 
-        let _ = prstr ("nthhyp= "^ string_of_int i) in
-        if isConst hyp && ((name_of_const hyp)==heq_prefix) then
-          let _ = prstr "YES\n" in
-          rewriteLR hyp gl 
-        else 
-          let _ = prstr "NO\n" in
-          tclIDTAC gl)
- *)
-    
-(* [invfun_basic C listargs_ids gl dorew lposeq] builds the tactic
-   which:
-   \begin{itemize}
-   \item Do refine on C (the induction principle),
-   \item try to Clear listargs_ids
-   \item if boolean dorew is true, then intro all new hypothesis, and
-   try rewrite on those hypothesis that are equalities.
-   \end{itemize}
-*)
-
-let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq =
- (tclTHEN_i
-  (tclTHEN
-   (tclTHEN
-    (* Refine on the right term (following the sheme of the
-       given function) *)
-    (fun gl -> refine open_princ_proof_applied gl)
-    (* Clear the hypothesis given as arguments of the tactic
-       (because they are generalized) *)
-    (tclTHEN simpl_in_concl (tclTRY (clear listargs_ids))))
-   (* Now we introduce the created hypothesis, and try rewrite on
-      equalities due to case analysis *)
-   (fun gl ->  (tclIDTAC gl)))
-		(fun i gl -> 
-   if not dorew then tclIDTAC gl
-   else
-     (* d,m,f correspond respectively to vars, induction hyps and
-        equalities*)
-     let d,m,f = List.nth lposeq (i-1) in
-     tclTHEN (iterintro (d)) (tclDO m (tclTRY intro)) gl)
- )
- gl
-
-
-
-
-(* This function trys to reduce instanciated arguments, provided they
-   are of the form [(C t u v...)] where [C] is a constructor, and
-   provided that the argument is not the argument of a fixpoint (i.e. the
-   argument corresponds to a simple lambda) . *)
-let rec applistc_iota cstr lcstr env sigma = 
- match lcstr with
-  | [] -> cstr,[]
-  | arg::lcstr' -> 
-     let arghd = 
-      if isApp arg then let x,_ = destApp arg in x else arg in
-     if isConstruct arghd (* of the form [(C ...)]*)
-     then 
-        applistc_iota (Tacred.nf env sigma (nf_beta (applistc cstr [arg])))
-         lcstr' env sigma
-     else 
-       try 
-        let nme,typ,suite = destLambda cstr in
-        let c, l = applistc_iota suite lcstr' env sigma in
-        mkLambda (nme,typ,c), arg::l
-       with _ -> cstr,arg::lcstr' (* the arg does not correspond to a lambda*)
-
-
-
-(* TODO: ne plus mettre les sous-but à l'exterieur, mais à l'intérieur (le bug
-   de refine est normalement resolu). Ca permettra 2 choses: d'une part que
-   les preuves soient plus simple, et d'autre part de fabriquer un terme de
-   refine qui pourra s'aapliquer SANS FAIRE LES INTROS AVANT, ce qui est bcp
-   mieux car fonctionne comme induction et plus comme inversion (pas de perte
-   de connexion entre les hypothèse et les variables). *)
-
-(*s Tactic that makes induction and case analysis following the shape
-  of a function (idf) given with arguments (listargs) *)
-let invfun c l dorew gl = 
-(* \begin{itemize}
-    \item [fonc] = the constant corresponding to the function
-    (necessary for equalities of the form [(f x1 x2 ...)=...] where
-    [f] is the recursive function).
-    \item [def_fonc] = body of the function, where let ins have
-    been expanded. *)
- let fonc, def_fonc' = interp_fonc_tacarg c gl in
- let def_fonc'',listargs' = 
-  applistc_iota def_fonc' l (pf_env gl) (project gl)  in
- let def_fonc = expand_letins def_fonc'' in
- (* quantifies on previously generalized arguments. 
-    [(x1:T1)...g[arg1 <- x1 ...]] *)
- let pis = add_pis (pf_concl gl) gl listargs' in
- (* princ_proof builds the principle *)
- let _ = resetmeta() in
- let pr = invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
- (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
- let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
- (* apply parameters immediately *)
- let gl_abstr = 
-  applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev pr.params)) in
- (* we apply args of the fix now, the parameters will be applied later *)
- let princ_proof_applied_args = 
-  applistc pr.princ (listsuf (List.length pr.params) listargs') in
- (* parameters are still there so patternify must not take them -> lift *)
- let princ_proof_applied_lift = 
-  lift (List.length pr.evarlist) princ_proof_applied_args in
- let princ_applied_hyps'' = patternify (List.rev pr.evarlist)
-  princ_proof_applied_lift (Name (id_of_string "Hyp"))  in
- (* if there was a fix, we will not add "Q" as in funscheme, so we make a pop,
-    TODO: find were we made the lift in proofPrinc instead and supress it here,
-    and add lift in funscheme. *)
- let princ_applied_hyps' = 
-  if Array.length pr.mutfixmetas > 0 then popn 1 princ_applied_hyps''
-  else princ_applied_hyps'' in 
- (* if there is was fix, we have to replace the meta representing the
-    predicate of the goal by the abstracted goal itself. *)
- let princ_applied_hyps = 
-  if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) 
-    (substit_red 0 (pr.mutfixmetas.(0)) gl_abstr princ_applied_hyps')
-  else princ_applied_hyps' (* No Fixpoint *) in
- let _ = prNamedConstr "princ_applied_hyps" princ_applied_hyps in
- (* Same thing inside levar *)
- let newlevar' = 
-  if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) 
-    List.map (fun (x,y) -> x,substit_red 0 (pr.mutfixmetas.(0)) gl_abstr y) pr.evarlist 
-  else pr.evarlist
- in
- (* replace params metavar by real args *)
- let rec replace_parms lparms largs t = 
-  match lparms, largs with
-     [], _ -> t
-   | ((p,_,_)::lp), (a::la) -> let t'= substitterm 0 p a t in replace_parms lp la t'
-   | _, _ -> error "problem with number of args." in
- let princ_proof_applied = replace_parms pr.params listargs' princ_applied_hyps in
- let _ = prNamedLConstr "levar:" (List.map fst newlevar') in
- let _ = prNamedLConstr "levar types:" (List.map snd newlevar') in
- let _ = prNamedConstr "princ_proof_applied" princ_proof_applied in
- (* replace also in levar *)
- let newlevar = 
-  List.rev (List.map (fun (x,y) -> x, replace_parms pr.params listargs' y) newlevar') in
-(*
- (* replace params metavar by abstracted variables *)
-  let princ_proof_params = npatternify (List.rev pr.params) princ_applied_hyps in
- (* we apply now the real parameters *)
- let princ_proof_applied = 
-  applistc princ_proof_params (listpref (List.length pr.params) listargs') in
-*)
- let princ_applied_evars = apply_levars princ_proof_applied newlevar in
- let open_princ_proof_applied = princ_applied_evars in
- let _ = prNamedConstr "princ_applied_evars" (snd princ_applied_evars) in
- let _ = prNamedLConstr "evars" (List.map snd (fst princ_applied_evars)) in
- let listargs_ids = List.map destVar (List.filter isVar listargs') in
- (* debug: impression du but*)
- let lgl = Evd.to_list (sig_sig gl) in
- let _ = prNamedLConstr "\ngl= " (List.map (fun x -> (snd x).evar_concl) lgl) in
- let _ = prstr "fin gl \n\n" in
- invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids 
-  gl dorew pr.hypnum
-
-(* function must be a constant, all arguments must be given. *)
-let invfun_verif c l dorew gl =
- if not (isConst c) then error "given function is not a constant"
- else 
-   let x,_ = decompose_prod (pf_type_of gl c) in
-   if List.length x = List.length l then 
-     try invfun c l dorew gl
-     with UserError (x,y) -> raise (UserError (x,y))
-   else error "wrong number of arguments for the function"
-
-
-
-
-(* Construction of the functional scheme. *)
-let buildFunscheme fonc mutflist =
- let def_fonc = expand_letins (def_of_const fonc) in
- let ftyp = type_of (Global.env ()) Evd.empty fonc in
- let _ = resetmeta() in
- let gl = mknewmeta() in
- let gl_app = applFull gl ftyp in
- let pis = prod_change_concl ftyp gl_app in
- (* Here we call the function invfun_proof, that effectively 
-    builds the scheme *)
-(*  let princ_proof,levar,_,evararr,absc,parms =  *)
- let _ = prstr "Recherche du principe... lancement de invfun_proof\n" in
- let pr = invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in
- (* parameters are still there (unboud rel), and patternify must not take them
-  -> lift*)
- let princ_proof_lift = lift (List.length pr.evarlist) pr.princ in
- let princ_proof_hyps = 
-  patternify (List.rev pr.evarlist) princ_proof_lift (Name (id_of_string "Hyp"))  in
- let rec princ_replace_metas ev abs i t = 
-  if i>= Array.length ev then t
-  else (* fix? *)
-    princ_replace_metas ev abs (i+1)
-     (mkLambda (
-      (Name (id_of_string ("Q"^(string_of_int i)))),
-      prod_change_concl (lift 0 abs.(i)) mkthesort,
-      (substitterm 0 ev.(i) (mkRel 1) (lift 0 t))))
- in
- let rec princ_replace_params params t = 
-  List.fold_left (
-   fun acc (ev,nam,typ) -> 
-    mkLambda (Name (id_of_name nam) , typ, 
-    substitterm 0 ev (mkRel 1) (lift 0 acc)))
-   t (List.rev params) in
- if Array.length pr.mutfixmetas = 0 (* Is there a Fixpoint? *)
-	then (* No Fixpoint *)
-   princ_replace_params pr.params (mkLambda ((Name (id_of_string "Q")), 
-		 prod_change_concl ftyp mkthesort,
-   (substitterm 0 gl (mkRel 1) princ_proof_hyps)))
-	else (* there is a fix -> add parameters + replace metas *)
-   let princ_rpl = 
-    princ_replace_metas pr.mutfixmetas pr.conclarray 0 princ_proof_hyps in
-   princ_replace_params pr.params princ_rpl
-
-
-    
-(* Declaration of the functional scheme. *)
-let declareFunScheme f fname mutflist =
- let _ = prstr "Recherche du perincipe...\n" in
- let id_to_cstr id = 
-  try global_reference id
-  with
-     Not_found -> error (string_of_id id ^ " not found in the environment") in
- let flist = if mutflist=[] then [f] else mutflist in
- let fcstrlist = Array.of_list (List.map id_to_cstr flist) in
- let idf = id_to_cstr f in
- let scheme = buildFunscheme idf fcstrlist in
-  let _ = prstr "Principe:" in
-  let _ = prconstr scheme in
- let ce = { 
-  const_entry_body = scheme;
-  const_entry_type = None;
-  const_entry_opaque = false;
-  const_entry_boxed = true } in
- let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in
- ()
-
-
-
-TACTIC EXTEND functional_induction
-  [ "old" "functional" "induction" constr(c)  ne_constr_list(l) ] 
-     -> [ invfun_verif c l true ]
-END
-
-VERNAC COMMAND EXTEND FunctionalScheme
- [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
-    ident(c) "with" ne_ident_list(l) ] 
-  -> [ declareFunScheme c na l ]
-| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
-  -> [ declareFunScheme c na [] ]
-END
-
-
-
-
-
-(* 
-*** Local Variables: ***
-*** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" ***
-*** tuareg-default-indent:1 ***
-*** tuareg-begin-indent:1 ***
-*** tuareg-let-indent:1 ***
-*** tuareg-match-indent:-1 ***
-*** tuareg-try-indent:1 ***
-*** tuareg-with-indent:1 ***
-*** tuareg-if-then-else-inden:1 ***
-*** fill-column: 78 ***
-*** indent-tabs-mode: nil ***
-***  test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v" ***
-*** End: ***
-*)
-          
-
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
deleted file mode 100644
index ce775e0be..000000000
--- a/contrib/funind/tacinvutils.ml
+++ /dev/null
@@ -1,284 +0,0 @@
-(* tacinvutils.ml *)
-(*s utilities *)
-
-(*i*)
-open Names
-open Util
-open Term
-open Termops
-open Coqlib
-open Pp
-open Printer
-open Inductiveops
-open Environ
-open Declarations
-open Nameops
-open Evd
-open Sign
-open Reductionops
-(*i*)
-
-(*s printing of constr -- 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"  " ++ pr_lconstr c ++ str"\n")
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
-
-let prchr () = msg (str" (ret) \n")
-let prNamedConstr s c = 
-  begin
-    msg(str "");
-    msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n");
-    msg(str "");
-  end
-
-let prNamedLConstr_aux lc = 
-  List.iter (prNamedConstr "#>") lc
-
-let prNamedLConstr s lc = 
-  begin
-    prstr s;
-    prNamedLConstr_aux lc
-  end
-
-
-(* FIXME: ref 1, pas bon, si? *)
-let evarcpt = ref 0
-let metacpt = ref 0
-let mknewexist ()= 
-  begin
-    evarcpt := !evarcpt+1;
-    !evarcpt,[||]
-  end
-
-let resetexist ()= evarcpt := 0
-
-let mknewmeta ()= 
-  begin
-    metacpt := !metacpt+1;
-    mkMeta (!metacpt)
-  end
-
-let resetmeta () = metacpt := 0
-
-let  rec mkevarmap_from_listex lex =
-  match lex with
-	 | [] -> Evd.empty
-	 | ((ex,_),typ)::lex' -> 
-(*		  let _ = prstr "mkevarmap" in
-		  let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in
-		  let _ = prstr "OF TYPE: " in
-		  let _ = prconstr typ in*)
-		  let info = {
-			 evar_concl = typ;
-			 evar_hyps = empty_named_context_val;
-			 evar_body = Evar_empty;
-		         evar_extra = None} in
-		  Evd.add (mkevarmap_from_listex lex') ex info
-
-let mkEq typ c1 c2 = 
-  mkApp (build_coq_eq(),[| typ; c1; c2|])
-
-let mkRefl typ c1 = 
-  mkApp ((build_coq_eq_data()).refl, [| typ; c1|])
-
-let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
-
-
-(* Operations on names *)
-let id_of_name = function
-    Anonymous -> id_of_string "H"
-  | Name id   -> id;;
-let string_of_name nme = string_of_id (id_of_name nme)
-let name_of_string str = Name (id_of_string str)
-let newname_append nme str = 
-  Name(id_of_string ((string_of_id (id_of_name nme))^str))
-
-(* 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 apply_eqtrpl eq t =
-  let r,(tb,b,by_t) = eq in
-  substitterm 0 b by_t t
-
-let apply_eqtrpl_lt lt eq =  List.map (apply_eqtrpl eq) lt
-
-let apply_leqtrpl_t t leq =
-  List.fold_left (fun x y -> apply_eqtrpl y x) t leq
-
-
-let apply_refl_term eq t =
-  let _,arr = destApp eq in
-  let reli= (Array.get arr 1) in
-  let by_t= (Array.get arr 2) in
-  substitterm 0 reli by_t t
-
-let apply_eq_leqtrpl leq eq =
-  List.map 
-    (function (r,(tb,b,t)) ->
-		r,(tb, 
-		(if isRel b then b else (apply_refl_term eq b)), apply_refl_term eq t))
-	 leq
-
-
-
-(* [(a b c) a] -> true *)
-let constr_head_match u t=
-  if isApp u 
-  then 
-	 let uhd,args= destApp u in
-    uhd=t
-  else false
-
-(* My operations on constr *)
-let lift1L l = (List.map (lift 1) l)
-let mkArrow_lift t1 t2 = mkArrow t1 (lift 1 t2)
-let mkProd_liftc nme c1 c2 = mkProd (nme,c1,(lift 1 c2))
-(* prod_it_lift x [a1 a2 ...] *)
-let prod_it_lift ini lcpl =
-  List.fold_right (function a,b -> (fun c -> mkProd_liftc a b c)) ini lcpl;;
-
-let prod_it_anonym_lift trm lst = List.fold_right mkArrow_lift lst trm
-
-let lam_it_anonymous trm lst =
-  List.fold_right 
-	 (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm
-
-let lambda_id id typeofid cstr =
-  let cstr' = mkNamedLambda (id_of_string "FUNX") typeofid cstr in
-  substitterm 0 id (mkRel 0) cstr'
-
-let prod_id id typeofid cstr =
-  let cstr' = mkNamedProd (id_of_string "FUNX") typeofid cstr in
-  substitterm 0 id (mkRel 0) cstr'
-
-
-
-
-
-let nth_dep_constructor indtype n =
-  let sigma = Evd.empty and env = Global.env() in
-  let indtypedef = find_rectype env sigma indtype in
-  let indfam,_ = dest_ind_type indtypedef in
-  let arr_cstr_summary = get_constructors env indfam in
-  let cstr_sum = Array.get arr_cstr_summary n in
-  build_dependent_constructor cstr_sum,  cstr_sum.cs_nargs
-
-
-let rec buildrefl_from_eqs eqs = 
-  match eqs with 
-    | []  ->  []
-    | cstr::eqs' -> 
-        let eq,args = destApp cstr in
-        (mkRefl (Array.get args 0) (Array.get args 2))
-	:: (buildrefl_from_eqs eqs')
-
-
-
-
-(* list of occurrences of a term inside another *)
-(* Cofix will be wrong, not sure Fix is correct too *)
-let rec hdMatchSub u t=
-  let subres = 
-    match kind_of_term u with
-      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t
-      | Fix (_,(lna,tl,bl))  -> 
-	  Array.fold_left 
-	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) 
-	    [] bl
-      | LetIn _  -> assert false
-	  (* Correct? *)
-      | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u
-  in 
-  if constr_head_match u t then u :: subres else subres
-
-
-(* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
-let hdMatchSub_cpl u (d,f) = 
-  let res = ref [] in
-  begin
-    for i = d to f do res := hdMatchSub u (mkRel i) @ !res done;
-    !res
-  end
-
-
-(* destApplication raises an exception if [t] is not an application *)      
-let exchange_hd_prod subst_hd t =
-  let hd,args= destApplication t in mkApp (subst_hd,args)
-
-(* substitute t by by_t in head of products inside in_u, reduces each
-	product found  *)
-let rec substit_red prof t by_t in_u =
-  if constr_head_match in_u (lift prof t) 
-  then
-    let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
-    x
-  else
-    map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u
-
-(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
-	reli by tarr.(f-i). *) 
-let exchange_reli_arrayi tarr (d,f) t =
-  let hd,args= destApp t in 
-  let i = destRel hd in
-  let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
-  res
-
-let exchange_reli_arrayi_L tarr (d,f) = 
-  List.map (exchange_reli_arrayi tarr (d,f))
-
-
-(* expand all letins in a term, before building the principle. *)
-let rec expand_letins mimick =
-  match kind_of_term mimick with
-    | LetIn(nme,cstr1, typ, cstr) ->
-        let cstr' = substitterm 0 (mkRel 1) (lift 1 cstr1) cstr in
-        expand_letins (pop cstr')
-    | x -> map_constr expand_letins mimick
-	  
-
-(* Valeur d'une constante, or identity *)
-let def_of_const t =
-  match kind_of_term t with
-    | Const sp -> 
-		  (try 
-			 match Global.lookup_constant sp with
-              {const_body=Some c} -> force c
- 				|_ -> assert false
-			 with _ -> assert false)
-    | _ -> t
-
-(* nom d'une constante. Must be a constante. x*)
-let name_of_const t =
-    match (kind_of_term t) with
-        Const cst -> Names.string_of_label (Names.con_label cst)
-		|_ -> assert false
- ;;
-
-
-(*i
-***  Local Variables:
-***  compile-command: "make -k tacinvutils.cmo"
-***  test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v"
-***  End:
-i*)
-
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
deleted file mode 100644
index 64b212130..000000000
--- a/contrib/funind/tacinvutils.mli
+++ /dev/null
@@ -1,80 +0,0 @@
-(* tacinvutils.ml *)
-(*s utilities *)
-
-(*i*)
-open Termops
-open Equality
-open Names
-open Pp
-open Tacmach
-open Proof_type
-open Tacinterp
-open Tactics
-open Tacticals
-open Term
-open Util
-open Printer
-open Reductionops
-open Inductiveops
-open Coqlib
-open Refine
-open Evd
-(*i*)
-
-(* printing debugging *)
-val prconstr: constr -> unit
-val prlistconstr: constr list  -> unit
-val prNamedConstr:string -> constr -> unit
-val prNamedLConstr:string -> constr list -> unit
-val prstr: string -> unit 
-
-
-val mknewmeta: unit -> constr
-val mknewexist: unit -> existential
-val resetmeta: unit -> unit (* safe *)
-val resetexist: unit -> unit (* be careful with this one *)
-val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map
-val mkEq: types -> constr -> constr -> constr
-(* let mkEq typ c1 c2 =   mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *)
-val mkRefl: types -> constr -> constr
-val buildrefl_from_eqs: constr list -> constr list
-(* typ c1 =  mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *)
-
-val nth_dep_constructor: constr -> int -> (constr*int)
-
-val prod_it_lift:  (name*constr) list -> constr -> constr
-val prod_it_anonym_lift: constr -> constr list -> constr
-val lam_it_anonymous: constr -> constr list -> constr
-val lift1L: (constr list) -> constr list
-val popn: int -> constr -> constr
-val lambda_id: constr -> constr -> constr -> constr
-val prod_id: constr -> constr -> constr -> constr
-
-
-val name_of_string : string -> name
-val newname_append: name -> string -> name
-
-val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr
-val substitterm: int -> constr -> constr -> constr -> constr
-val apply_leqtrpl_t: 
-  constr -> (constr*(constr*constr*constr)) list -> constr
-val apply_eq_leqtrpl: 
-  (constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list
-(* val apply_leq_lt: constr list -> constr list -> constr list *)
-
-val hdMatchSub: constr -> constr -> constr list
-val hdMatchSub_cpl: constr -> int*int -> constr list
-val exchange_hd_prod: constr -> constr -> constr
-val exchange_reli_arrayi_L: constr array  -> int*int -> constr list -> constr list
-val substit_red: int -> constr -> constr -> constr -> constr
-val expand_letins: constr -> constr
-
-val def_of_const: constr -> constr
-val name_of_const: constr -> string
-
-(*i
- *** Local Variables: ***
- *** compile-command: "make -C ../.. contrib/funind/tacinvutils.cmi" ***
- *** End: ***
-i*)
-