[funind] Move principle generation to its own file.

1 files changed, 0 insertions, 1626 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 73e9c94d34..eeb2f246c2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -13,43 +13,13 @@ open Sorts
 open Util
 open Names
 open Constr
-open Context
 open EConstr
 open Pp
 open Indfun_common
-open Libnames
-open Glob_term
-open Declarations
 open Tactypes
-open Decl_kinds
 
 module RelDecl = Context.Rel.Declaration
 
-(* Move to common *)
-let observe strm =
-  if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
-
-let do_observe_tac s tac g =
-  let goal =
-    try Printer.pr_goal g
-    with e when CErrors.noncritical e -> assert false
-  in
-  try
-    let v = tac g in
-    msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    observe (hov 0 (str "observation "++ s++str " raised exception " ++
-             CErrors.iprint reraise ++ str " on goal" ++ fnl() ++ goal ));
-    iraise reraise;;
-
-let observe_tac s tac g =
-  if do_observe ()
-  then do_observe_tac (str s) tac g
-  else tac g
-
 let is_rec_info sigma scheme_info =
   let test_branche min acc decl =
     acc || (
@@ -175,1599 +145,3 @@ let functional_induction with_clean c princl pat =
       subst_and_reduce
       g'
   in res
-
-let rec abstract_glob_constr c = function
-  | [] -> c
-  | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl)
-  | Constrexpr.CLocalAssum (idl,k,t)::bl ->
-      List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
-        (abstract_glob_constr c bl)
-  | Constrexpr.CLocalPattern _::bl -> assert false
-
-let interp_casted_constr_with_implicits env sigma impls c  =
-  Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls c
-
-(*
-   Construct a fixpoint as a Glob_term
-   and not as a constr
-*)
-
-let build_newrecursive lnameargsardef =
-  let env0 = Global.env() in
-  let sigma = Evd.from_env env0 in
-  let (rec_sign,rec_impls) =
-    List.fold_left
-      (fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } ->
-        let arityc = Constrexpr_ops.mkCProdN binders rtype in
-        let arity,ctx = Constrintern.interp_type env0 sigma arityc in
-        let evd = Evd.from_env env0 in
-        let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in
-        let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
-        let open Context.Named.Declaration in
-        let r = Sorts.Relevant in (* TODO relevance *)
-        (EConstr.push_named (LocalAssum (make_annot recname r,arity)) env, Id.Map.add recname impl impls))
-      (env0,Constrintern.empty_internalization_env) lnameargsardef in
-  let recdef =
-    (* Declare local notations *)
-    let f { Vernacexpr.binders; body_def } =
-      match body_def with
-      | Some body_def ->
-        let def = abstract_glob_constr body_def binders in
-        interp_casted_constr_with_implicits
-          rec_sign sigma rec_impls def
-      | None -> user_err ~hdr:"Function" (str "Body of Function must be given")
-    in
-    States.with_state_protection (List.map f) lnameargsardef
-  in
-  recdef,rec_impls
-
-let error msg = user_err Pp.(str msg)
-
-(* Checks whether or not the mutual bloc is recursive *)
-let is_rec names =
-  let names = List.fold_right Id.Set.add names Id.Set.empty in
-  let check_id id names =  Id.Set.mem id names in
-  let rec lookup names gt = match DAst.get gt with
-    | GVar(id) -> check_id id names
-    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GInt _ -> false
-    | GCast(b,_) -> lookup names b
-    | GRec _ -> error "GRec not handled"
-    | GIf(b,_,lhs,rhs) ->
-        (lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | GProd(na,_,t,b) | GLambda(na,_,t,b) ->
-        lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b
-    | GLetIn(na,b,t,c) ->
-        lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c
-    | GLetTuple(nal,_,t,b) -> lookup names t ||
-        lookup
-          (List.fold_left
-             (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc)
-             names
-             nal
-          )
-          b
-    | GApp(f,args) -> List.exists (lookup names) (f::args)
-    | GCases(_,_,el,brl) ->
-        List.exists (fun (e,_) -> lookup names e) el ||
-          List.exists (lookup_br names) brl
-  and lookup_br names {CAst.v=(idl,_,rt)} =
-    let new_names = List.fold_right Id.Set.remove idl names in
-    lookup new_names rt
-  in
-  lookup names
-
-let rec local_binders_length = function
-  (* Assume that no `{ ... } contexts occur *)
-  | [] -> 0
-  | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl
-  | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-  | Constrexpr.CLocalPattern _::bl -> assert false
-
-let prepare_body { Vernacexpr.binders; rtype } rt =
-  let n = local_binders_length binders in
-(*   Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *)
-  let fun_args,rt' = chop_rlambda_n n rt in
-  (fun_args,rt')
-
-(* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ]
-   is the tactic used to prove correctness lemma.
-
-   [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions
-   (resp. graphs of the functions and principles and correctness lemma types) to prove correct.
-
-   [i] is the indice of the function to prove correct
-
-   The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is
-   it looks like~:
-   [\forall (x_1:t_1)\ldots(x_n:t_n), forall res,
-   res = f x_1\ldots x_n in, \rightarrow graph\ x_1\ldots x_n\ res]
-
-
-   The sketch of the proof is the following one~:
-   \begin{enumerate}
-   \item intros until $x_n$
-   \item $functional\ induction\ (f.(i)\ x_1\ldots x_n)$ using schemes.(i)
-   \item for each generated branch intro [res] and [hres :res = f x_1\ldots x_n], rewrite [hres] and the
-   apply the corresponding constructor of the corresponding graph inductive.
-   \end{enumerate}
-
-*)
-
-let rec generate_fresh_id x avoid i =
-  if i == 0
-  then []
-  else
-    let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in
-    id::(generate_fresh_id x (id::avoid) (pred i))
-
-let make_eq () =
-  try EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
-  with _ -> assert false
-
-let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
-  let open Context.Rel.Declaration in
-  let open Tacmach in
-  let open Tactics in
-  let open Tacticals in
-  fun g ->
-    (* first of all we recreate the lemmas types to be used as predicates of the induction principle
-       that is~:
-       \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun  fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
-    *)
-    (* we the get the definition of the graphs block *)
-    let graph_ind,u = destInd evd graphs_constr.(i) in
-    let kn = fst graph_ind in
-    let mib,_ = Global.lookup_inductive graph_ind in
-    (* and the principle to use in this lemma in $\zeta$ normal form *)
-    let f_principle,princ_type = schemes.(i) in
-    let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in
-    let princ_infos = Tactics.compute_elim_sig evd princ_type in
-    (* The number of args of the function is then easily computable *)
-    let nb_fun_args = Termops.nb_prod (project g) (pf_concl g) - 2 in
-    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
-    let ids = args_names@(pf_ids_of_hyps g) in
-    (* Since we cannot ensure that the functional principle is defined in the
-       environment and due to the bug #1174, we will need to pose the principle
-       using a name
-    *)
-    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in
-    let ids = principle_id :: ids in
-    (* We get the branches of the principle *)
-    let branches = List.rev princ_infos.Tactics.branches in
-    (* and built the intro pattern for each of them *)
-    let intro_pats =
-      List.map
-        (fun decl ->
-           List.map
-             (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
-             (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
-        )
-        branches
-    in
-    (* before building the full intro pattern for the principle *)
-    let eq_ind = make_eq () in
-    let eq_construct = mkConstructUi (destInd evd eq_ind, 1) in
-    (* The next to referencies will be used to find out which constructor to apply in each branch *)
-    let ind_number = ref 0
-    and min_constr_number = ref 0 in
-    (* The tactic to prove the ith branch of the principle *)
-    let prove_branche i g =
-      (* We get the identifiers of this branch *)
-      let pre_args =
-        List.fold_right
-          (fun {CAst.v=pat} acc ->
-             match pat with
-               | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
-               | _ -> anomaly (Pp.str "Not an identifier.")
-          )
-          (List.nth intro_pats (pred i))
-          []
-      in
-      (* and get the real args of the branch by unfolding the defined constant *)
-      (*
-         We can then recompute the arguments of the constructor.
-         For each [hid] introduced by this branch, if [hid] has type
-         $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are
-         [ fv (hid fv (refl_equal fv)) ].
-         If [hid] has another type the corresponding argument of the constructor is [hid]
-      *)
-      let constructor_args g =
-        List.fold_right
-          (fun hid acc ->
-             let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
-             let sigma = project g in
-             match EConstr.kind sigma type_of_hid with
-               | Prod(_,_,t') ->
-                   begin
-                     match EConstr.kind sigma t' with
-                       | Prod(_,t'',t''') ->
-                           begin
-                             match EConstr.kind sigma t'',EConstr.kind sigma t''' with
-                               | App(eq,args), App(graph',_)
-                                   when
-                                     (EConstr.eq_constr sigma eq eq_ind) &&
-                                       Array.exists  (EConstr.eq_constr_nounivs sigma graph') graphs_constr ->
-                                   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
-                                    ::acc)
-                               | _ -> mkVar hid ::  acc
-                           end
-                       | _ -> mkVar hid :: acc
-                   end
-               | _ -> mkVar hid :: acc
-          ) pre_args []
-      in
-      (* in fact we must also add the parameters to the constructor args *)
-      let constructor_args g =
-        let params_id = fst (List.chop princ_infos.Tactics.nparams args_names) in
-        (List.map mkVar params_id)@((constructor_args g))
-      in
-      (* We then get the constructor corresponding to this branch and
-         modifies the references has needed i.e.
-         if the constructor is the last one of the current inductive then
-         add one the number of the inductive to take and add the number of constructor of the previous
-         graph to the minimal constructor number
-      *)
-      let constructor =
-        let constructor_num = i - !min_constr_number in
-        let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in
-        if constructor_num <= length
-        then
-          begin
-            (kn,!ind_number),constructor_num
-          end
-        else
-          begin
-            incr ind_number;
-            min_constr_number := !min_constr_number + length ;
-            (kn,!ind_number),1
-          end
-      in
-      (* we can then build the final proof term *)
-      let app_constructor g = applist((mkConstructU(constructor,u)),constructor_args g) in
-      (* an apply the tactic *)
-      let res,hres =
-        match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
-          | [res;hres] -> res,hres
-          | _ -> assert false
-      in
-      (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *)
-      (
-        tclTHENLIST
-          [
-            observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in
-                                               match l with
-                                                 | [] -> tclIDTAC
-                                                 | _ -> Proofview.V82.of_tactic (intro_patterns false l));
-            (* unfolding of all the defined variables introduced by this branch *)
-            (* observe_tac "unfolding" pre_tac; *)
-            (* $zeta$ normalizing of the conclusion *)
-            Proofview.V82.of_tactic (reduce
-              (Genredexpr.Cbv
-                 { Redops.all_flags with
-                     Genredexpr.rDelta = false ;
-                     Genredexpr.rConst = []
-                 }
-              )
-              Locusops.onConcl);
-            observe_tac ("toto ") tclIDTAC;
-
-            (* introducing the result of the graph and the equality hypothesis *)
-            observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
-            (* replacing [res] with its value *)
-            observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
-            (* Conclusion *)
-            observe_tac "exact" (fun g ->
-                                 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)
-          ]
-      )
-        g
-    in
-    (* end of branche proof *)
-    let lemmas =
-      Array.map
-        (fun ((_,(ctxt,concl))) ->
-           match ctxt with
-           | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.")
-           | hres::res::decl::ctxt ->
-             let res = EConstr.it_mkLambda_or_LetIn
-                 (EConstr.it_mkProd_or_LetIn concl [hres;res])
-                 (LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl) :: ctxt)
-             in
-             res)
-        lemmas_types_infos
-    in
-    let param_names = fst (List.chop princ_infos.nparams args_names) in
-    let params = List.map mkVar param_names in
-    let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
-    (* The bindings of the principle
-       that is the params of the principle and the different lemma types
-    *)
-    let bindings =
-      let params_bindings,avoid =
-        List.fold_left2
-          (fun (bindings,avoid) decl p ->
-             let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
-             p::bindings,id::avoid
-          )
-          ([],pf_ids_of_hyps g)
-          princ_infos.params
-          (List.rev params)
-      in
-      let lemmas_bindings =
-        List.rev (fst  (List.fold_left2
-          (fun (bindings,avoid) decl p ->
-             let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
-             (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid)
-          ([],avoid)
-          princ_infos.predicates
-          (lemmas)))
-      in
-      (params_bindings@lemmas_bindings)
-    in
-    tclTHENLIST
-      [
-        observe_tac "principle" (Proofview.V82.of_tactic (assert_by
-          (Name principle_id)
-          princ_type
-          (exact_check f_principle)));
-        observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
-        (* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
-        observe_tac "idtac" tclIDTAC;
-        tclTHEN_i
-          (observe_tac
-             "functional_induction" (
-               (fun gl ->
-                let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-                let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
-                Proofview.V82.of_tactic (apply term) gl')
-           ))
-          (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
-      ]
-      g
-
-(**
-   [find_induction_principle f] searches and returns the [body] and the [type] of [f_rect]
-
-   WARNING: while convertible, [type_of body] and [type] can be non equal
-*)
-let find_induction_principle evd f =
-  let f_as_constant,u =  match EConstr.kind !evd f with
-    | Const c' -> c'
-    | _ -> user_err Pp.(str "Must be used with a function")
-  in
-  let infos = find_Function_infos f_as_constant in
-  match infos.rect_lemma with
-    | None -> raise Not_found
-    | Some rect_lemma ->
-       let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (GlobRef.ConstRef rect_lemma) in
-       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
-       evd:=evd';
-       rect_lemma,typ
-
-(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
-   (resp. g_to_f = false) where [graph]  is the graph of [f] and is the [i]th function in the block.
-
-   [generate_type true f i] returns
-   \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,
-   graph\ x_1\ldots x_n\ res \rightarrow res = fv \] decomposed as the context and the conclusion
-
-   [generate_type false f i] returns
-   \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,
-   res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion
- *)
-
-let generate_type evd g_to_f f graph i =
-  let open Context.Rel.Declaration in
-  let open EConstr.Vars in
-  (*i we deduce the number of arguments of the function and its returned type from the graph i*)
-  let evd',graph =
-    Evd.fresh_global  (Global.env ()) !evd  (GlobRef.IndRef (fst (destInd !evd graph)))
-  in
-  evd:=evd';
-  let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
-  evd := sigma;
-  let ctxt,_ = decompose_prod_assum !evd graph_arity in
-  let fun_ctxt,res_type =
-    match ctxt with
-      | [] | [_] -> anomaly (Pp.str "Not a valid context.")
-      | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
-  in
-  let rec args_from_decl i accu = function
-  | [] -> accu
-  | LocalDef _ :: l ->
-    args_from_decl (succ i) accu l
-  | _ :: l ->
-    let t = mkRel i in
-    args_from_decl (succ i) (t :: accu) l
-  in
-  (*i We need to name the vars [res] and [fv] i*)
-  let filter = fun decl -> match RelDecl.get_name decl with
-                           | Name id -> Some id
-                           | Anonymous -> None
-  in
-  let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in
-  let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
-  let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in
-  (*i we can then type the argument to be applied to the function [f] i*)
-  let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in
-  (*i
-    the hypothesis [res = fv] can then be computed
-    We will need to lift it by one in order to use it as a conclusion
-    i*)
-  let make_eq = make_eq ()
-  in
-  let res_eq_f_of_args =
-    mkApp(make_eq ,[|lift 2 res_type;mkRel 1;mkRel 2|])
-  in
-  (*i
-    The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed
-    We will need to lift it by one in order to use it as a conclusion
-    i*)
-  let args_and_res_as_rels = Array.of_list (args_from_decl 3 [] fun_ctxt) in
-  let args_and_res_as_rels = Array.append args_and_res_as_rels [|mkRel 1|] in
-  let graph_applied = mkApp(graph, args_and_res_as_rels) in
-  (*i The [pre_context]  is the defined to be the context corresponding to
-    \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,  \]
-    i*)
-  let pre_ctxt =
-    LocalAssum (make_annot (Name res_id) Sorts.Relevant, lift 1 res_type) ::
-    LocalDef (make_annot (Name fv_id) Sorts.Relevant, mkApp (f,args_as_rels), res_type) :: fun_ctxt
-  in
-  (*i and we can return the solution depending on which lemma type we are defining i*)
-  if g_to_f
-  then LocalAssum (make_annot Anonymous Sorts.Relevant,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
-  else LocalAssum (make_annot Anonymous Sorts.Relevant,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
-
-(* [prove_fun_complete funs graphs schemes lemmas_types_infos i]
-   is the tactic used to prove completeness lemma.
-
-   [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions
-   (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct.
-
-   [i] is the indice of the function to prove complete
-
-   The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is
-   it looks like~:
-   [\forall (x_1:t_1)\ldots(x_n:t_n), forall res,
-   graph\ x_1\ldots x_n\ res, \rightarrow  res = f x_1\ldots x_n in]
-
-
-   The sketch of the proof is the following one~:
-   \begin{enumerate}
-   \item intros until $H:graph\ x_1\ldots x_n\ res$
-   \item $elim\ H$ using schemes.(i)
-   \item for each generated branch, intro  the news hyptohesis, for each such hyptohesis [h], if [h] has
-   type [x=?] with [x] a variable, then subst [x],
-   if [h] has type [t=?] with [t] not a variable then rewrite [t] in the subterms, else
-   if [h] is a match then destruct it, else do just introduce it,
-   after all intros, the conclusion should be a reflexive equality.
-   \end{enumerate}
-
-*)
-
-let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
-
-(* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
-       (unfolding, substituting, destructing cases \ldots)
- *)
-let tauto =
-  let open Ltac_plugin in
-  let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
-  let mp = ModPath.MPfile (DirPath.make dp) in
-  let kn = KerName.make mp (Label.make "tauto") in
-  Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
-    let body = Tacenv.interp_ltac kn in
-    Tacinterp.eval_tactic body
-  end
-
-(* [generalize_dependent_of x hyp g]
-   generalize every hypothesis which depends of [x] but [hyp]
-*)
-let generalize_dependent_of x hyp g =
-  let open Context.Named.Declaration in
-  let open Tacmach in
-  let open Tacticals in
-  tclMAP
-    (function
-       | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) &&
-           (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
-       | _ -> tclIDTAC
-    )
-    (pf_hyps g)
-    g
-
-let rec intros_with_rewrite g =
-  observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
-and intros_with_rewrite_aux : Tacmach.tactic =
-  let open Tacmach in
-  let open Tactics in
-  let open Tacticals in
-  fun g ->
-    let eq_ind = make_eq () in
-    let sigma = project g in
-    match EConstr.kind sigma (pf_concl g) with
-          | Prod(_,t,t') ->
-              begin
-                match EConstr.kind sigma t with
-                  | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind)  ->
-                      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
-                      then
-                        let id = pf_get_new_id (Id.of_string "y") g  in
-                        tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
-                      else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g))
-                      then tclTHENLIST[
-                        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]);
-                        tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) )))
-                          (pf_ids_of_hyps g);
-                        intros_with_rewrite
-                      ] g
-                      else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g))
-                      then tclTHENLIST[
-                        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]);
-                        tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) )))
-                          (pf_ids_of_hyps g);
-                        intros_with_rewrite
-                      ] g
-                      else if isVar sigma args.(1)
-                      then
-                        let id = pf_get_new_id (Id.of_string "y") g  in
-                        tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
-                                     generalize_dependent_of (destVar sigma args.(1)) id;
-                                     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
-                                     intros_with_rewrite
-                                   ]
-                          g
-                      else if isVar sigma args.(2)
-                      then
-                        let id = pf_get_new_id (Id.of_string "y") g  in
-                        tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
-                                     generalize_dependent_of (destVar sigma args.(2)) id;
-                                     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
-                                     intros_with_rewrite
-                                   ]
-                          g
-                      else
-                        begin
-                          let id = pf_get_new_id (Id.of_string "y") g  in
-                          tclTHENLIST[
-                            Proofview.V82.of_tactic (Simple.intro id);
-                            tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
-                            intros_with_rewrite
-                          ] g
-                        end
-                  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) ->
-                      Proofview.V82.of_tactic tauto g
-                  | Case(_,_,v,_) ->
-                      tclTHENLIST[
-                        Proofview.V82.of_tactic (simplest_case v);
-                        intros_with_rewrite
-                      ] g
-                  | LetIn _ ->
-                      tclTHENLIST[
-                        Proofview.V82.of_tactic (reduce
-                          (Genredexpr.Cbv
-                             {Redops.all_flags
-                              with Genredexpr.rDelta = false;
-                             })
-                          Locusops.onConcl)
-                        ;
-                        intros_with_rewrite
-                      ] g
-                  | _ ->
-                      let id = pf_get_new_id (Id.of_string "y") g  in
-                      tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
-              end
-          | LetIn _ ->
-              tclTHENLIST[
-                Proofview.V82.of_tactic (reduce
-                  (Genredexpr.Cbv
-                     {Redops.all_flags
-                      with Genredexpr.rDelta = false;
-                     })
-                  Locusops.onConcl)
-                ;
-                intros_with_rewrite
-              ] g
-          | _ -> tclIDTAC g
-
-let rec reflexivity_with_destruct_cases g =
-  let open Tacmach in
-  let open Tactics in
-  let open Tacticals in
-  let destruct_case () =
-    try
-      match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with
-        | Case(_,_,v,_) ->
-            tclTHENLIST[
-              Proofview.V82.of_tactic (simplest_case v);
-              Proofview.V82.of_tactic intros;
-              observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
-            ]
-        | _ -> Proofview.V82.of_tactic reflexivity
-    with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
-  in
-  let eq_ind = make_eq () in
-  let my_inj_flags = Some {
-    Equality.keep_proof_equalities = false;
-    injection_in_context = false; (* for compatibility, necessary *)
-    injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *)
-  } in
-  let discr_inject =
-    Tacticals.onAllHypsAndConcl (
-       fun sc g ->
-         match sc with
-             None -> tclIDTAC g
-           | Some id ->
-               match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
-                 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
-                     if Equality.discriminable (pf_env g) (project g) t1 t2
-                     then Proofview.V82.of_tactic (Equality.discrHyp id) g
-                     else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
-                     then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite]  g
-                     else tclIDTAC g
-                 | _ -> tclIDTAC g
-    )
-  in
-  (tclFIRST
-    [ observe_tac "reflexivity_with_destruct_cases : reflexivity" (Proofview.V82.of_tactic reflexivity);
-      observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ()));
-      (*  We reach this point ONLY if
-          the same value is matched (at least) two times
-          along binding path.
-          In this case, either we have a discriminable hypothesis and we are done,
-          either at least an injectable one and we do the injection before continuing
-      *)
-      observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases)
-    ])
-    g
-
-let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tactic =
-  let open Tacmach in
-  let open Tactics in
-  let open Tacticals in
-  fun g ->
-    (* We compute the types of the different mutually recursive lemmas
-       in $\zeta$ normal form
-    *)
-    let lemmas =
-      Array.map
-        (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt))
-        lemmas_types_infos
-    in
-    (* We get the constant and the principle corresponding to this lemma *)
-    let f = funcs.(i) in
-    let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i))  in
-    let princ_type = pf_unsafe_type_of g graph_principle in
-    let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
-    (* Then we get the number of argument of the function
-       and compute a fresh name for each of them
-    *)
-    let nb_fun_args = Termops.nb_prod (project g) (pf_concl g) - 2 in
-    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
-    let ids = args_names@(pf_ids_of_hyps g) in
-    (* and fresh names for res H and the principle (cf bug bug #1174) *)
-    let res,hres,graph_principle_id =
-      match generate_fresh_id (Id.of_string "z") ids 3 with
-        | [res;hres;graph_principle_id] -> res,hres,graph_principle_id
-        | _ -> assert false
-    in
-    let ids = res::hres::graph_principle_id::ids in
-    (* we also compute fresh names for each hyptohesis of each branch
-       of the principle *)
-    let branches = List.rev princ_infos.branches in
-    let intro_pats =
-      List.map
-        (fun decl ->
-           List.map
-             (fun id -> id)
-             (generate_fresh_id (Id.of_string "y") ids (Termops.nb_prod (project g) (RelDecl.get_type decl)))
-        )
-        branches
-    in
-    (* We will need to change the function by its body
-       using [f_equation] if it is recursive (that is the graph is infinite
-       or unfold if the graph is finite
-    *)
-    let rewrite_tac j ids : Tacmach.tactic =
-      let graph_def = graphs.(j) in
-      let infos =
-        try find_Function_infos (fst (destConst (project g) funcs.(j)))
-        with Not_found ->  user_err Pp.(str "No graph found")
-      in
-      if infos.is_general
-        || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs
-      then
-        let eq_lemma =
-          try Option.get (infos).equation_lemma
-          with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.")
-        in
-        tclTHENLIST[
-          tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
-          Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
-          (* Don't forget to $\zeta$ normlize the term since the principles
-             have been $\zeta$-normalized *)
-          Proofview.V82.of_tactic (reduce
-            (Genredexpr.Cbv
-               {Redops.all_flags
-                with Genredexpr.rDelta = false;
-               })
-            Locusops.onConcl)
-          ;
-          Proofview.V82.of_tactic (generalize (List.map mkVar ids));
-          thin ids
-        ]
-      else
-        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst (project g) f)))])
-    in
-    (* The proof of each branche itself *)
-    let ind_number = ref 0 in
-    let min_constr_number = ref 0 in
-    let prove_branche i g =
-      (* we fist compute the inductive corresponding to the branch *)
-      let this_ind_number =
-        let constructor_num = i - !min_constr_number in
-        let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in
-        if constructor_num <= length
-        then !ind_number
-        else
-          begin
-            incr ind_number;
-            min_constr_number := !min_constr_number + length;
-            !ind_number
-          end
-      in
-      let this_branche_ids = List.nth intro_pats (pred i) in
-      tclTHENLIST[
-        (* we expand the definition of the function *)
-        observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
-        (* introduce hypothesis with some rewrite *)
-        observe_tac "intros_with_rewrite (all)" intros_with_rewrite;
-        (* The proof is (almost) complete *)
-        observe_tac "reflexivity" (reflexivity_with_destruct_cases)
-      ]
-        g
-    in
-    let params_names = fst (List.chop princ_infos.nparams args_names) in
-    let open EConstr in
-    let params = List.map mkVar params_names in
-    tclTHENLIST
-      [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
-        observe_tac "h_generalize"
-        (Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
-        Proofview.V82.of_tactic (Simple.intro graph_principle_id);
-        observe_tac "" (tclTHEN_i
-          (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
-          (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
-      ]
-      g
-
-(* [derive_correctness make_scheme funs graphs] create correctness and completeness
-   lemmas for each function in [funs] w.r.t. [graphs]
-
-   [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and
-*)
-
-let derive_correctness (funs: pconstant list) (graphs:inductive list) =
-  assert (funs <> []);
-  assert (graphs <> []);
-  let funs = Array.of_list funs and graphs = Array.of_list graphs in
-  let map (c, u) = mkConstU (c, EInstance.make u) in
-  let funs_constr = Array.map map funs  in
-  (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
-  funind_purify
-    (fun () ->
-     let env = Global.env () in
-     let evd = ref (Evd.from_env env) in
-     let graphs_constr = Array.map mkInd graphs in
-     let lemmas_types_infos =
-       Util.Array.map2_i
-         (fun i f_constr graph ->
-         (* let const_of_f,u = destConst f_constr in *)
-         let (type_of_lemma_ctxt,type_of_lemma_concl,graph) =
-           generate_type evd false f_constr graph i
-         in
-         let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
-         graphs_constr.(i) <- graph;
-         let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-         let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
-         evd := sigma;
-           let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in
-           observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
-           type_of_lemma,type_info
-        )
-        funs_constr
-        graphs_constr
-    in
-    let schemes =
-      (* The functional induction schemes are computed and not saved if there is more that one function
-         if the block contains only one function we can safely reuse [f_rect]
-       *)
-      try
-        if not (Int.equal (Array.length funs_constr) 1) then raise Not_found;
-        [| find_induction_principle evd funs_constr.(0) |]
-      with Not_found ->
-        (
-
-          Array.of_list
-            (List.map
-               (fun entry ->
-                  (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
-               )
-               (Functional_principles_types.make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
-            )
-        )
-    in
-    let proving_tac =
-      prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos
-    in
-    Array.iteri
-      (fun i f_as_constant ->
-         let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
-         (*i The next call to mk_correct_id is valid since we are constructing the lemma
-             Ensures by: obvious
-         i*)
-         let lem_id = mk_correct_id f_id in
-         let (typ,_) = lemmas_types_infos.(i) in
-         let info = Lemmas.Info.make
-             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:(Decls.(IsProof Theorem)) () in
-         let lemma = Lemmas.start_lemma
-             ~name:lem_id
-             ~poly:false
-             ~info
-             !evd
-             typ in
-         let lemma = fst @@ Lemmas.by
-                   (Proofview.V82.tactic (proving_tac i)) lemma in
-         let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-         let finfo = find_Function_infos (fst f_as_constant) in
-         (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
-         let _,lem_cst_constr = Evd.fresh_global
-                                  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-         let (lem_cst,_) = destConst !evd lem_cst_constr in
-         update_Function {finfo with correctness_lemma = Some lem_cst};
-
-      )
-      funs;
-    let lemmas_types_infos =
-      Util.Array.map2_i
-        (fun i f_constr graph ->
-         let (type_of_lemma_ctxt,type_of_lemma_concl,graph)   =
-           generate_type evd true f_constr graph i
-         in
-         let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
-         graphs_constr.(i) <- graph;
-         let type_of_lemma =
-           EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
-         in
-         let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in
-         observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
-         type_of_lemma,type_info
-        )
-        funs_constr
-        graphs_constr
-    in
-
-    let (kn,_) as graph_ind,u  = (destInd !evd graphs_constr.(0)) in
-    let mib,mip = Global.lookup_inductive graph_ind in
-    let sigma, scheme =
-        (Indrec.build_mutual_induction_scheme (Global.env ()) !evd
-           (Array.to_list
-              (Array.mapi
-                 (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType)
-                 mib.Declarations.mind_packets
-              )
-           )
-        )
-    in
-    let schemes =
-      Array.of_list scheme
-    in
-    let proving_tac =
-      prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos
-    in
-    Array.iteri
-      (fun i f_as_constant ->
-         let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
-         (*i The next call to mk_complete_id is valid since we are constructing the lemma
-             Ensures by: obvious
-           i*)
-         let lem_id = mk_complete_id f_id in
-         let info = Lemmas.Info.make
-             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:Decls.(IsProof Theorem) () in
-         let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
-             sigma (fst lemmas_types_infos.(i)) in
-         let lemma = fst (Lemmas.by
-                            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-                                                     (proving_tac i))) lemma) in
-         let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-         let finfo = find_Function_infos (fst f_as_constant) in
-         let _,lem_cst_constr = Evd.fresh_global
-                                  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-         let (lem_cst,_) = destConst !evd lem_cst_constr in
-         update_Function {finfo with completeness_lemma = Some lem_cst}
-      )
-      funs)
-    ()
-
-let warn_funind_cannot_build_inversion =
-  CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
-    (fun e' -> strbrk "Cannot build inversion information" ++
-                 if do_observe () then (fnl() ++ CErrors.print e') else mt ())
-
-let derive_inversion fix_names =
-  try
-    let evd' = Evd.from_env (Global.env ()) in
-    (* we first transform the fix_names identifier into their corresponding constant *)
-    let evd',fix_names_as_constant =
-      List.fold_right
-        (fun id (evd,l) ->
-         let evd,c =
-           Evd.fresh_global
-             (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in
-        let (cst, u) = destConst evd c in
-         evd, (cst, EInstance.kind evd u) :: l
-        )
-        fix_names
-        (evd',[])
-    in
-    (*
-       Then we check that the graphs have been defined
-       If one of the graphs haven't been defined
-       we do nothing
-    *)
-    List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ;
-    try
-      let evd', lind =
-        List.fold_right
-          (fun id (evd,l) ->
-           let evd,id =
-             Evd.fresh_global
-               (Global.env ()) evd
-               (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id)))
-           in
-           evd,(fst (destInd evd id))::l
-          )
-          fix_names
-          (evd',[])
-      in
-      derive_correctness
-        fix_names_as_constant
-        lind;
-      with e when CErrors.noncritical e ->
-        warn_funind_cannot_build_inversion e
-  with e when CErrors.noncritical e ->
-    warn_funind_cannot_build_inversion e
-
-let warn_cannot_define_graph =
-  CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
-    (fun (names,error) -> strbrk "Cannot define graph(s) for " ++
-      h 1 names ++ error)
-
-let warn_cannot_define_principle =
-  CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind"
-  (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++
-      h 1 names ++ error)
-
-let warning_error names e =
-  let e_explain e =
-    match e with
-      | ToShow e ->
-        spc () ++ CErrors.print e
-      | _ ->
-        if do_observe ()
-        then (spc () ++ CErrors.print e)
-        else mt ()
-  in
-  match e with
-    | Building_graph e ->
-       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
-       warn_cannot_define_graph (names,e_explain e)
-    | Defining_principle e ->
-       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
-       warn_cannot_define_principle (names,e_explain e)
-    | _ -> raise e
-
-let error_error names e =
-  let e_explain e =
-    match e with
-      | ToShow e -> spc () ++ CErrors.print e
-      | _ -> if do_observe () then (spc () ++ CErrors.print e) else mt ()
-  in
-  match e with
-    | Building_graph e ->
-        user_err
-          (str "Cannot define graph(s) for " ++
-             h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
-             e_explain e)
-    | _ -> raise e
-
-let generate_principle (evd:Evd.evar_map ref) pconstants on_error
-    is_general do_built (fix_rec_l : Vernacexpr.fixpoint_expr list) recdefs interactive_proof
-    (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
-      Tacmach.tactic) : unit =
-  let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in
-  let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
-  let funs_args = List.map fst fun_bodies in
-  let funs_types =  List.map (function { Vernacexpr.rtype } -> rtype) fix_rec_l in
-  try
-    (* We then register the Inductive graphs of the functions  *)
-    Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs;
-    if do_built
-    then
-      begin
-        (*i The next call to mk_rel_id is valid since we have just construct the graph
-           Ensures by : do_built
-        i*)
-        let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in
-        let ind_kn =
-          fst (locate_with_msg
-                 (pr_qualid f_R_mut++str ": Not an inductive type!")
-                 locate_ind
-                 f_R_mut)
-        in
-        let fname_kn { Vernacexpr.fname } =
-   let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in
-          locate_with_msg
-            (pr_qualid f_ref++str ": Not an inductive type!")
-            locate_constant
-            f_ref
-        in
-        let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
-        let _ =
-          List.map_i
-            (fun i x ->
-              let env = Global.env () in
-              let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in
-             let evd = ref (Evd.from_env env) in
-             let evd',uprinc = Evd.fresh_global env !evd princ in
-             let _ = evd := evd' in
-             let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in
-             evd := sigma;
-             let princ_type = EConstr.Unsafe.to_constr princ_type in
-             Functional_principles_types.generate_functional_principle
-               evd
-                 interactive_proof
-                 princ_type
-                 None
-                 None
-                 (Array.of_list pconstants)
-                 (* funs_kn *)
-                 i
-                 (continue_proof  0 [|funs_kn.(i)|])
-            )
-            0
-            fix_rec_l
-        in
-        Array.iter (add_Function is_general) funs_kn;
-        ()
-      end
-  with e when CErrors.noncritical e ->
-    on_error names e
-
-let register_struct is_rec (fixpoint_exprl:  Vernacexpr.fixpoint_expr list) =
-  match fixpoint_exprl with
-    | [ { Vernacexpr.fname; univs; binders; rtype; body_def } ] when not is_rec ->
-      let body = match body_def with
-        | Some body -> body
-        | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
-      ComDefinition.do_definition
-        ~program_mode:false
-        ~name:fname.CAst.v
-        ~poly:false
-        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-        ~kind:Decls.Definition univs
-        binders None body (Some rtype);
-       let evd,rev_pconstants =
-         List.fold_left
-           (fun (evd,l) { Vernacexpr.fname } ->
-            let evd,c =
-              Evd.fresh_global
-                (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in
-            let (cst, u) = destConst evd c in
-            let u = EInstance.kind evd u in
-            evd,((cst, u) :: l)
-           )
-           (Evd.from_env (Global.env ()),[])
-           fixpoint_exprl
-       in
-       None, evd,List.rev rev_pconstants
-    | _ ->
-       ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl;
-       let evd,rev_pconstants =
-         List.fold_left
-           (fun (evd,l) { Vernacexpr.fname } ->
-            let evd,c =
-              Evd.fresh_global
-                (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in
-            let (cst, u) = destConst evd c in
-            let u = EInstance.kind evd u in
-            evd,((cst, u) :: l)
-           )
-           (Evd.from_env (Global.env ()),[])
-           fixpoint_exprl
-       in
-       None,evd,List.rev rev_pconstants
-
-
-let generate_correction_proof_wf f_ref tcc_lemma_ref
-    is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-    (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
-  Functional_principles_proofs.prove_principle_for_gen
-    (f_ref,functional_ref,eq_ref)
-    tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
-
-
-let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
-    pre_hook
-    =
-  let type_of_f = Constrexpr_ops.mkCProdN args ret_type in
-  let rec_arg_num =
-    let names =
-      List.map
-        CAst.(with_val (fun x -> x))
-        (Constrexpr_ops.names_of_local_assums args)
-    in
-          List.index Name.equal (Name wf_arg) names
-  in
-  let unbounded_eq =
-    let f_app_args =
-      CAst.make @@ Constrexpr.CAppExpl(
-         (None,qualid_of_ident fname.CAst.v,None) ,
-         (List.map
-            (function
-               | {CAst.v=Anonymous} -> assert false
-               | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e)
-            )
-            (Constrexpr_ops.names_of_local_assums args)
-         )
-        )
-    in
-    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")),
-                    [(f_app_args,None);(body,None)])
-  in
-  let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
-  let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
-      nb_args relation =
-    try
-      pre_hook [fconst]
-        (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
-           functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-        );
-      derive_inversion [fname.CAst.v]
-    with e when CErrors.noncritical e ->
-      (* No proof done *)
-      ()
-  in
-  Recdef.recursive_definition ~interactive_proof
-    ~is_mes fname.CAst.v rec_impls
-    type_of_f
-    wf_rel_expr
-    rec_arg_num
-    eq
-    hook
-    using_lemmas
-
-
-let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body =
-  let wf_arg_type,wf_arg =
-    match wf_arg with
-      | None ->
-          begin
-            match args with
-              | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
-              | _ -> error "Recursive argument must be specified"
-          end
-      | Some wf_args ->
-          try
-            match
-              List.find
-                (function
-                   | Constrexpr.CLocalAssum(l,k,t) ->
-                       List.exists
-                         (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
-                         l
-                   | _ -> false
-                )
-                args
-            with
-              | Constrexpr.CLocalAssum(_,k,t)  ->           t,wf_args
-              | _ -> assert false
-          with Not_found -> assert false
-  in
-  let wf_rel_from_mes,is_mes =
-    match wf_rel_expr_opt with
-      | None ->
-          let ltof =
-            let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
-            Libnames.qualid_of_path
-              (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))
-          in
-          let fun_from_mes =
-            let applied_mes =
-              Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg])    in
-            Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
-          in
-          let wf_rel_from_mes =
-            Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC  ltof,[wf_arg_type;fun_from_mes])
-          in
-          wf_rel_from_mes,true
-      | Some wf_rel_expr ->
-          let wf_rel_with_mes =
-            let a = Names.Id.of_string "___a" in
-            let b = Names.Id.of_string "___b" in
-            Constrexpr_ops.mkLambdaC(
-              [CAst.make @@ Name a; CAst.make @@ Name b],
-              Constrexpr.Default Explicit,
-              wf_arg_type,
-              Constrexpr_ops.mkAppC(wf_rel_expr,
-                               [
-                                Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC a]);
-                                Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC b])
-                               ])
-                              )
-          in
-          wf_rel_with_mes,false
-  in
-  register_wf interactive_proof ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg
-    using_lemmas args ret_type body
-
-let map_option f = function
-  | None -> None
-  | Some v -> Some (f v)
-
-open Constrexpr
-
-let rec rebuild_bl aux bl typ =
-        match bl,typ with
-          | [], _ -> List.rev aux,typ
-          | (CLocalAssum(nal,bk,_))::bl',typ ->
-             rebuild_nal aux bk bl' nal  typ
-          | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } ->
-            rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux)
-              bl' typ'
-          | _ -> assert false
-and rebuild_nal aux bk bl' nal typ =
-        match nal,typ with
-          | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
-          | [], _ -> rebuild_bl aux bl' typ
-          | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } ->
-             if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v)
-             then
-               let assum = CLocalAssum([na],bk,nal't) in
-               let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
-               rebuild_nal
-                 (assum::aux)
-                 bk
-                 bl'
-                 nal
-                 (CAst.make @@ CProdN(new_rest,typ'))
-             else
-               let assum = CLocalAssum([na'],bk,nal't) in
-               let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
-               rebuild_nal
-                 (assum::aux)
-                 bk
-                 bl'
-                 (na::nal)
-                 (CAst.make @@ CProdN(new_rest,typ'))
-          | _ ->
-             assert false
-
-let rebuild_bl aux bl typ = rebuild_bl aux bl typ
-
-let recompute_binder_list fixpoint_exprl =
-  let fixl =
-    List.map (fun fix -> Vernacexpr.{
-        fix
-        with rec_order = ComFixpoint.adjust_rec_order ~structonly:false fix.binders fix.rec_order }) fixpoint_exprl in
-  let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl in
-  let constr_expr_typel =
-    with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
-  let fixpoint_exprl_with_new_bl =
-    List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ ->
-      let binders, rtype = rebuild_bl [] binders fix_typ in
-      { fp with Vernacexpr.binders; rtype }
-    ) fixpoint_exprl constr_expr_typel
-  in
-  fixpoint_exprl_with_new_bl
-
-
-let do_generate_principle_aux pconstants on_error register_built interactive_proof
-    (fixpoint_exprl : Vernacexpr.fixpoint_expr list) : Lemmas.t option =
-  List.iter (fun { Vernacexpr.notations } ->
-      if not (List.is_empty notations)
-      then error "Function does not support notations for now") fixpoint_exprl;
-  let lemma, _is_struct =
-    match fixpoint_exprl with
-      | [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] ->
-        let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr =
-          match recompute_binder_list [fixpoint_expr] with
-          | [e] -> e
-          | _ -> assert false
-        in
-        let fixpoint_exprl = [fixpoint_expr] in
-        let body = match body_def with
-          | Some body -> body
-          | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
-        let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
-        let using_lemmas = [] in
-        let pre_hook pconstants =
-          generate_principle
-            (ref (Evd.from_env (Global.env ())))
-            pconstants
-            on_error
-            true
-            register_built
-            fixpoint_exprl
-            recdefs
-            true
-        in
-        if register_built
-        then register_wf interactive_proof fname rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false
-        else None, false
-      |[{ Vernacexpr.rec_order=Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] ->
-        let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr =
-          match recompute_binder_list [fixpoint_expr] with
-          | [e] -> e
-          | _ -> assert false
-        in
-        let fixpoint_exprl = [fixpoint_expr] in
-        let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
-        let using_lemmas = [] in
-        let body = match body_def with
-          | Some body -> body
-          | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
-        let pre_hook pconstants =
-          generate_principle
-            (ref (Evd.from_env (Global.env ())))
-            pconstants
-            on_error
-            true
-            register_built
-            fixpoint_exprl
-            recdefs
-            true
-        in
-        if register_built
-        then register_mes interactive_proof fname rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas binders rtype body pre_hook, true
-        else None, true
-      | _ ->
-        List.iter (function { Vernacexpr.rec_order } ->
-          match rec_order with
-          | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } ->
-            error
-              ("Cannot use mutual definition with well-founded recursion or measure")
-          | _ -> ()
-                    )
-            fixpoint_exprl;
-        let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
-        let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in
-        (* ok all the expressions are structural *)
-        let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
-        let is_rec = List.exists (is_rec fix_names) recdefs in
-        let lemma,evd,pconstants =
-          if register_built
-          then register_struct is_rec fixpoint_exprl
-          else None, Evd.from_env (Global.env ()), pconstants
-        in
-        let evd = ref evd in
-        generate_principle
-          (ref !evd)
-          pconstants
-          on_error
-          false
-          register_built
-          fixpoint_exprl
-          recdefs
-          interactive_proof
-          (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof);
-          if register_built then
-            begin derive_inversion fix_names; end;
-          lemma, true
-  in
-  lemma
-
-let rec add_args id new_args = CAst.map (function
-  | CRef (qid,_) as b ->
-    if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
-      CAppExpl((None,qid,None),new_args)
-    else b
-  | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
-  | CProdN(nal,b1) ->
-        CProdN(List.map (function  CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
-                                 | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
-                                 | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
-             add_args id new_args  b1)
-  | CLambdaN(nal,b1) ->
-      CLambdaN(List.map (function  CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
-                                 | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
-                                 | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
-               add_args id new_args  b1)
-  | CLetIn(na,b1,t,b2) ->
-      CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
-  | CAppExpl((pf,qid,us),exprl) ->
-    if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
-      CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl))
-    else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl)
-  | CApp((pf,b),bl) ->
-      CApp((pf,add_args id new_args b),
-           List.map (fun (e,o) -> add_args id new_args e,o) bl)
-  | CCases(sty,b_option,cel,cal) ->
-      CCases(sty,Option.map (add_args id new_args) b_option,
-             List.map (fun (b,na,b_option) ->
-                         add_args id new_args b,
-                         na, b_option) cel,
-             List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal
-            )
-  | CLetTuple(nal,(na,b_option),b1,b2) ->
-      CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
-                add_args id new_args b1,
-                add_args id new_args b2
-               )
-
-  | CIf(b1,(na,b_option),b2,b3) ->
-      CIf(add_args id new_args b1,
-          (na,Option.map (add_args id new_args) b_option),
-          add_args id new_args b2,
-          add_args id new_args b3
-         )
-  | CHole _
-  | CPatVar _
-  | CEvar _
-  | CPrim _
-  | CSort _ as b -> b
-  | CCast(b1,b2)  ->
-      CCast(add_args id new_args b1,
-            Glob_ops.map_cast_type (add_args id new_args) b2)
-  | CRecord pars ->
-      CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
-  | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
-  | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
-  | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
-  )
-exception Stop of  Constrexpr.constr_expr
-
-
-(* [chop_n_arrow n t] chops the [n] first arrows in [t]
-   Acts on Constrexpr.constr_expr
-*)
-let rec chop_n_arrow n t =
-  if n <= 0
-  then t (* If we have already removed all the arrows then return the type *)
-  else (* If not we check the form of [t] *)
-    match t.CAst.v with
-      | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible :
-                                             either we need to discard more than the number of arrows contained
-                                             in this product declaration then we just recall [chop_n_arrow] on
-                                             the remaining number of arrow to chop and [t'] we discard it and
-                                             recall [chop_n_arrow], either this product contains more arrows
-                                             than the number we need to chop and then we return the new type
-                                          *)
-          begin
-            try
-              let new_n =
-                let rec aux (n:int) = function
-                    [] -> n
-                | CLocalAssum(nal,k,t'')::nal_ta' ->
-                    let nal_l = List.length nal in
-                    if n >= nal_l
-                    then
-                      aux (n - nal_l) nal_ta'
-                    else
-                      let new_t' = CAst.make @@
-                        Constrexpr.CProdN(
-                                        CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t')
-                      in
-                      raise (Stop new_t')
-                | _ -> anomaly (Pp.str "Not enough products.")
-                in
-                aux n nal_ta'
-            in
-              chop_n_arrow new_n t'
-            with Stop t -> t
-          end
-      | _ -> anomaly (Pp.str "Not enough products.")
-
-
-let rec get_args b t : Constrexpr.local_binder_expr list *
-    Constrexpr.constr_expr * Constrexpr.constr_expr =
-  match b.CAst.v with
-    | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') ->
-        begin
-          let n = List.length nal in
-          let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in
-          d :: nal_tas, b'',t''
-        end
-    | Constrexpr.CLambdaN ([], b) -> [],b,t
-    | _ -> [],b,t
-
-
-let make_graph (f_ref : GlobRef.t) =
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-  let c,c_body =
-    match f_ref with
-    | GlobRef.ConstRef c ->
-      begin try c,Global.lookup_constant c
-        with Not_found ->
-          raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
-      end
-    | _ -> raise (UserError (None, str "Not a function reference") )
-  in
-  (match Global.body_of_constant_body Library.indirect_accessor c_body with
-     | None -> error "Cannot build a graph over an axiom!"
-     | Some (body, _, _) ->
-       let env = Global.env () in
-       let extern_body,extern_type =
-         with_full_print (fun () ->
-             (Constrextern.extern_constr false env sigma (EConstr.of_constr body),
-              Constrextern.extern_type false env sigma
-                (EConstr.of_constr (*FIXME*) c_body.const_type)
-             )
-           ) ()
-       in
-       let (nal_tas,b,t)  = get_args extern_body extern_type in
-       let expr_list =
-         match b.CAst.v with
-         | Constrexpr.CFix(l_id,fixexprl) ->
-           let l =
-             List.map
-               (fun (id,recexp,bl,t,b) ->
-                  let { CAst.loc; v=rec_id } = match Option.get recexp with
-                    | { CAst.v = CStructRec id } -> id
-                    | { CAst.v = CWfRec (id,_) } -> id
-                    | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid
-                  in
-                  let new_args =
-                    List.flatten
-                      (List.map
-                         (function
-                           | Constrexpr.CLocalDef (na,_,_)-> []
-                           | Constrexpr.CLocalAssum (nal,_,_) ->
-                             List.map
-                               (fun {CAst.loc;v=n} -> CAst.make ?loc @@
-                                 CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
-                               nal
-                           | Constrexpr.CLocalPattern _ -> assert false
-                         )
-                         nal_tas
-                      )
-                  in
-                  let b' = add_args id.CAst.v new_args b in
-                  { Vernacexpr.fname=id; univs=None
-                  ; rec_order = Some (CAst.make (CStructRec (CAst.make rec_id)))
-                  ; binders = nal_tas@bl; rtype=t; body_def=Some b'; notations = []}
-               ) fixexprl in
-           l
-         | _ ->
-           let fname = CAst.make (Label.to_id (Constant.label c)) in
-           [{ Vernacexpr.fname; univs=None; rec_order = None; binders=nal_tas; rtype=t; body_def=Some b; notations=[]}]
-       in
-       let mp = Constant.modpath c in
-       let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error  false false expr_list in
-       assert (Option.is_empty pstate);
-       (* We register the infos *)
-       List.iter
-         (fun { Vernacexpr.fname= {CAst.v=id} } ->
-            add_Function false (Constant.make2 mp (Label.of_id id)))
-         expr_list)
-
-(* *************** statically typed entrypoints ************************* *)
-
-let do_generate_principle_interactive fixl : Lemmas.t =
-  match
-    do_generate_principle_aux [] warning_error true true fixl
-  with
-  | Some lemma -> lemma
-  | None ->
-    CErrors.anomaly
-      (Pp.str"indfun: leaving no open proof in interactive mode")
-
-let do_generate_principle fixl : unit =
-  match do_generate_principle_aux [] warning_error true false fixl  with
-  | Some _lemma ->
-    CErrors.anomaly
-      (Pp.str"indfun: leaving a goal open in non-interactive mode")
-  | None -> ()