Merge PR #10525: [funind] Miscellaneous code reorganizations and cleanup

Reviewed-by: ppedrot

16 files changed, 2425 insertions, 2490 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 08298bf02c..5a939b4adf 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -18,77 +18,6 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
-(* let msgnl = Pp.msgnl *)
-
-(*
-let observe strm =
-  if do_observe ()
-  then Pp.msg_debug strm
-  else ()
-
-let do_observe_tac s tac g =
- try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
- with e ->
-   let e = ExplainErr.process_vernac_interp_error e in
-   let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
-   msg_debug (str "observation "++ s++str " raised exception " ++
-            Errors.print e ++ str " on goal " ++ goal );
-   raise e;;
-
-let observe_tac_stream s tac g =
-  if do_observe ()
-  then do_observe_tac  s tac g
-  else tac g
-
-let observe_tac s tac g = observe_tac_stream (str s) tac g
-  *)
-
-
-let debug_queue = Stack.create ()
-
-let rec print_debug_queue e =
-  if  not (Stack.is_empty debug_queue)
-  then
-    begin
-      let lmsg,goal = Stack.pop debug_queue in
-      let _ =
-        match e with
-        | Some e ->
-           Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
-        | None ->
-           begin
-             Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
-           end in
-      print_debug_queue None ;
-    end
-
-let observe strm =
-  if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
-
-let do_observe_tac s tac g =
-  let goal = Printer.pr_goal g in
-  let lmsg = (str "observation : ") ++ s in
-  Stack.push (lmsg,goal) debug_queue;
-  try
-    let v = tac g in
-    ignore(Stack.pop debug_queue);
-    v
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    if not (Stack.is_empty debug_queue)
-    then print_debug_queue (Some (fst reraise));
-    iraise reraise
-
-let observe_tac_stream s tac g =
-  if do_observe ()
-  then do_observe_tac s tac g
-  else tac g
-
-let observe_tac s = observe_tac_stream (str s)
-
-
 let list_chop ?(msg="") n l =
   try
     List.chop n l
@@ -120,6 +49,7 @@ type 'a dynamic_info =
 
 type body_info = constr dynamic_info
 
+let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
 
 let finish_proof dynamic_infos g =
   observe_tac "finish"
@@ -171,7 +101,7 @@ let is_incompatible_eq env sigma t =
         | _ -> false
     with e when CErrors.noncritical e -> false
   in
-  if res then   observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t);
+  if res then observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t);
   res
 
 let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -843,7 +773,8 @@ let build_proof
           | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-    observe_tac_stream (str "build_proof with " ++ pr_leconstr_env (pf_env g) (project g) dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+    Indfun_common.observe_tac (fun env sigma ->
+        str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args env sigma do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in
@@ -1232,7 +1163,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
               if this_fix_info.idx + 1 = 0
               then tclIDTAC (* Someone  tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
               else
-                observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1)))
+                Indfun_common.observe_tac (fun _ _ -> str "h_fix " ++ int (this_fix_info.idx +1))
+                  (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1)))
             else
               Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
                 other_fix_infos 0)
@@ -1476,13 +1408,14 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
                          (observe_tac "finishing using"
                            (
                             tclCOMPLETE(
-                                    Eauto.eauto_with_bases
-                                      (true,5)
-                                      [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
-                                      [Hints.Hint_db.empty TransparentState.empty false]
-                                  )
-                           )
-                        )
+                              Proofview.V82.of_tactic @@
+                              Eauto.eauto_with_bases
+                                (true,5)
+                                [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
+                                [Hints.Hint_db.empty TransparentState.empty false]
+                            )
+                          )
+                         )
                        ]
                     )
                 ]
@@ -1538,7 +1471,9 @@ let prove_principle_for_gen
   let wf_tac =
     if is_mes
     then
-      (fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None)
+      (fun b ->
+         Proofview.V82.of_tactic @@
+         Recdef.tclUSER_if_not_mes Tacticals.New.tclIDTAC b None)
     else fun _ -> prove_with_tcc tcc_lemma_ref []
   in
   let real_rec_arg_num = rec_arg_num - princ_info.nparams in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d34faa22fa..797d421c56 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -11,18 +11,15 @@
 open Printer
 open CErrors
 open Term
-open Sorts
 open Util
 open Constr
 open Context
 open Vars
-open Namegen
 open Names
 open Pp
 open Tactics
 open Context.Rel.Declaration
 open Indfun_common
-open Functional_principles_proofs
 
 module RelDecl = Context.Rel.Declaration
 
@@ -258,449 +255,3 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
                       new_predicates)
     )
     (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params)
-
-
-
-let change_property_sort evd toSort princ princName =
-  let open Context.Rel.Declaration in
-  let princ = EConstr.of_constr princ in
-  let princ_info = compute_elim_sig evd princ in
-  let change_sort_in_predicate decl =
-    LocalAssum
-    (get_annot decl,
-     let args,ty = decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in
-     let s = destSort ty in
-       Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
-       Term.compose_prod args (mkSort toSort)
-    )
-  in
-  let evd,princName_as_constr =
-    Evd.fresh_global
-      (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in
-  let init =
-    let nargs =  (princ_info.nparams + (List.length  princ_info.predicates)) in
-    mkApp(EConstr.Unsafe.to_constr princName_as_constr,
-          Array.init nargs
-            (fun i -> mkRel (nargs - i )))
-  in
-  evd,  it_mkLambda_or_LetIn
-    (it_mkLambda_or_LetIn init
-       (List.map change_sort_in_predicate princ_info.predicates)
-    )
-    (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.params)
-
-let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
-  (* First we get the type of the old graph principle *)
-  let mutr_nparams = (compute_elim_sig !evd (EConstr.of_constr old_princ_type)).nparams in
-  (*   let time1 = System.get_time ()  in *)
-  let new_principle_type =
-    compute_new_princ_type_from_rel
-      (Array.map mkConstU funs)
-      sorts
-      old_princ_type
-  in
-  (*    let time2 = System.get_time ()  in *)
-  (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
-  let new_princ_name =
-    next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
-  in
-  let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
-  evd := sigma;
-  let hook = DeclareDef.Hook.make (hook new_principle_type) in
-  let lemma =
-    Lemmas.start_lemma
-      ~name:new_princ_name
-      ~poly:false
-      !evd
-      (EConstr.of_constr new_principle_type)
-  in
-  (*       let _tim1 = System.get_time ()  in *)
-  let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
-  let lemma,_ = Lemmas.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) lemma in
-  (*       let _tim2 =  System.get_time ()  in *)
-  (*    begin *)
-  (*      let dur1 = System.time_difference tim1 tim2 in *)
-  (*      Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
-  (*    end; *)
-
-  let open Proof_global in
-  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
-  match entries with
-  | [entry] ->
-    name, entry, hook
-  | _ ->
-    CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
-
-let generate_functional_principle (evd: Evd.evar_map ref)
-    interactive_proof
-    old_princ_type sorts new_princ_name funs i proof_tac
-    =
-  try
-
-  let f = funs.(i) in
-  let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in
-  evd := sigma;
-  let new_sorts =
-    match sorts with
-      | None -> Array.make (Array.length funs) (type_sort)
-      | Some a -> a
-  in
-  let base_new_princ_name,new_princ_name =
-    match new_princ_name with
-      | Some (id) -> id,id
-      | None ->
-          let id_of_f = Label.to_id (Constant.label (fst f)) in
-          id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort)
-  in
-  let names = ref [new_princ_name] in
-  let hook =
-    fun new_principle_type _  ->
-    if Option.is_empty sorts
-    then
-      (*     let id_of_f = Label.to_id (con_label f) in *)
-      let register_with_sort fam_sort =
-        let evd' = Evd.from_env (Global.env ()) in
-        let evd',s = Evd.fresh_sort_in_family evd' fam_sort in
-        let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
-        let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
-        let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
-        (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-        let univs = Evd.univ_entry ~poly:false evd' in
-        let ce = Declare.definition_entry ~univs value in
-        ignore(
-          Declare.declare_constant
-            ~name
-            ~kind:Decls.(IsDefinition Scheme)
-            (Declare.DefinitionEntry ce)
-        );
-        Declare.definition_message name;
-        names := name :: !names
-      in
-      register_with_sort InProp;
-      register_with_sort InSet
-  in
-  let id,entry,hook =
-    build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
-    proof_tac hook
-  in
-  (* Pr  1278 :
-     Don't forget to close the goal if an error is raised !!!!
-  *)
-  let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(IsProof Theorem)
-  with e when CErrors.noncritical e ->
-    raise (Defining_principle e)
-
-exception Not_Rec
-
-let get_funs_constant mp =
-  let get_funs_constant const e : (Names.Constant.t*int) array =
-    match Constr.kind ((strip_lam e)) with
-      | Fix((_,(na,_,_))) ->
-          Array.mapi
-            (fun i na ->
-               match na.binder_name with
-                 | Name id ->
-                     let const = Constant.make2 mp (Label.of_id id) in
-                     const,i
-                 | Anonymous ->
-                     anomaly (Pp.str "Anonymous fix.")
-            )
-            na
-      | _ -> [|const,0|]
-  in
-  function const ->
-    let find_constant_body const =
-      match Global.body_of_constant Library.indirect_accessor const with
-        | Some (body, _, _) ->
-            let body = Tacred.cbv_norm_flags
-              (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-              (Global.env ())
-              (Evd.from_env (Global.env ()))
-              (EConstr.of_constr body)
-            in
-            let body = EConstr.Unsafe.to_constr body in
-            body
-        | None -> user_err Pp.(str ( "Cannot define a principle over an axiom "))
-    in
-    let f = find_constant_body const in
-    let l_const = get_funs_constant const f in
-    (*
-       We need to check that all the functions found are in the same block
-       to prevent Reset strange thing
-    *)
-    let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
-    let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in
-    (* all the parameters must be equal*)
-    let _check_params =
-      let first_params = List.hd l_params  in
-      List.iter
-        (fun params ->
-   if not (List.equal (fun (n1, c1) (n2, c2) ->
-       eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
-           then user_err Pp.(str "Not a mutal recursive block")
-        )
-        l_params
-    in
-    (* The bodies has to be very similar *)
-    let _check_bodies =
-      try
-        let extract_info is_first body =
-          match Constr.kind body with
-            | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
-            | _ ->
-                if is_first && Int.equal (List.length l_bodies) 1
-                then raise Not_Rec
-                else user_err Pp.(str "Not a mutal recursive block")
-        in
-        let first_infos = extract_info true (List.hd l_bodies) in
-        let check body  = (* Hope this is correct *)
-          let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
-     Array.equal Int.equal ia1 ia2 && Array.equal (eq_annot Name.equal) na1 na2 &&
-     Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
-          in
-          if not (eq_infos first_infos (extract_info false body))
-          then  user_err Pp.(str "Not a mutal recursive block")
-        in
-        List.iter check l_bodies
-      with Not_Rec -> ()
-    in
-    l_const
-
-exception No_graph_found
-exception Found_type of int
-
-let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list =
-  let env = Global.env () in
-  let funs = List.map fst fas in
-  let first_fun = List.hd funs in
-  let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
-  let first_fun_kn =
-    try
-      fst (find_Function_infos  (fst first_fun)).graph_ind
-    with Not_found -> raise No_graph_found
-  in
-  let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
-  let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
-  let prop_sort = InProp in
-  let funs_indexes =
-    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.map
-      (function cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes)
-      funs
-  in
-  let ind_list =
-    List.map
-      (fun (idx) ->
-         let ind = first_fun_kn,idx in
-           (ind,snd first_fun),true,prop_sort
-      )
-      funs_indexes
-  in
-  let sigma, schemes =
-    Indrec.build_mutual_induction_scheme env !evd ind_list
-  in
-  let _ = evd := sigma in
-  let l_schemes =
-    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
-  in
-  let i = ref (-1) in
-  let sorts =
-    List.rev_map (fun (_,x) ->
-        let sigma, fs = Evd.fresh_sort_in_family !evd x in
-        evd := sigma; fs
-      )
-      fas
-  in
-  (* We create the first principle by tactic *)
-  let first_type,other_princ_types =
-    match l_schemes with
-        s::l_schemes -> s,l_schemes
-      | _ -> anomaly (Pp.str "")
-  in
-  let _,const,_ =
-    try
-      build_functional_principle evd false
-        first_type
-        (Array.of_list sorts)
-        this_block_funs
-        0
-        (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
-        (fun _ _ -> ())
-    with e when CErrors.noncritical e ->
-      raise (Defining_principle e)
-
-  in
-  incr i;
-  let opacity =
-    let finfos = find_Function_infos (fst first_fun) in
-    try
-      let equation =  Option.get finfos.equation_lemma in
-      Declareops.is_opaque (Global.lookup_constant equation)
-    with Option.IsNone -> (* non recursive definition *)
-      false
-  in
-  let const = {const with Proof_global.proof_entry_opaque = opacity } in
-  (* The others are just deduced *)
-  if List.is_empty other_princ_types
-  then
-    [const]
-  else
-    let other_fun_princ_types =
-      let funs = Array.map mkConstU this_block_funs in
-      let sorts = Array.of_list sorts in
-      List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
-    in
-    let open Proof_global in
-    let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in
-    let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
-    let (idxs,_),(_,ta,_ as decl) = destFix fix in
-    let other_result =
-      List.map (* we can now compute the other principles *)
-        (fun scheme_type ->
-           incr i;
-           observe (Printer.pr_lconstr_env env sigma scheme_type);
-           let type_concl = (strip_prod_assum scheme_type) in
-           let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in
-           let f = fst (decompose_app applied_f) in
-           try (* we search the number of the function in the fix block (name of the function) *)
-             Array.iteri
-             (fun j t ->
-                let t =  (strip_prod_assum t) in
-                let applied_g = List.hd (List.rev (snd (decompose_app t))) in
-                let g = fst (decompose_app applied_g) in
-                if Constr.equal f g
-                then raise (Found_type j);
-                observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++
-                         Printer.pr_lconstr_env env sigma g)
-
-             )
-             ta;
-             (* If we reach this point, the two principle are not mutually recursive
-                We fall back to the previous method
-                *)
-             let _,const,_ =
-               build_functional_principle
-                 evd
-                 false
-                 (List.nth other_princ_types (!i - 1))
-                 (Array.of_list sorts)
-                 this_block_funs
-                 !i
-                 (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
-                 (fun _ _ -> ())
-             in
-             const
-         with Found_type i ->
-           let princ_body =
-             Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
-           in
-           {const with
-              proof_entry_body =
-                (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
-              proof_entry_type = Some scheme_type
-           }
-      )
-      other_fun_princ_types
-    in
-    const::other_result
-
-let build_scheme fas =
-  let evd = (ref (Evd.from_env (Global.env ()))) in
-  let pconstants = (List.map
-         (fun (_,f,sort) ->
-            let f_as_constant =
-              try
-                Smartlocate.global_with_alias f
-              with Not_found ->
-                user_err ~hdr:"FunInd.build_scheme"
-                  (str "Cannot find " ++ Libnames.pr_qualid f)
-            in
-            let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
-            let _ = evd := evd' in
-            let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in
-            evd := sigma;
-            let c, u =
-              try EConstr.destConst !evd f
-              with DestKO ->
-                user_err Pp.(pr_econstr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function")
-            in
-            (c, EConstr.EInstance.kind !evd u), sort
-         )
-         fas
-                   ) in
-  let bodies_types =
-    make_scheme evd pconstants
-  in
-
-  List.iter2
-    (fun (princ_id,_,_) def_entry ->
-       ignore
-         (Declare.declare_constant
-            ~name:princ_id
-            ~kind:Decls.(IsProof Theorem)
-            (Declare.DefinitionEntry def_entry));
-       Declare.definition_message princ_id
-    )
-    fas
-    bodies_types
-
-let build_case_scheme fa =
-  let env = Global.env ()
-  and sigma = (Evd.from_env (Global.env ())) in
-(*   let id_to_constr id =  *)
-(*     Constrintern.global_reference  id *)
-(*   in  *)
-  let funs =
-    let (_,f,_) = fa in
-    try (let open GlobRef in
-         match Smartlocate.global_with_alias f with
-         | ConstRef c -> c
-         | IndRef _ | ConstructRef _ | VarRef _ -> assert false)
-    with Not_found ->
-      user_err ~hdr:"FunInd.build_case_scheme"
-        (str "Cannot find " ++ Libnames.pr_qualid f) in
-  let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
-  let first_fun = funs in
-  let funs_mp = Constant.modpath first_fun in
-  let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
-  let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
-  let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
-  let prop_sort = InProp in
-  let funs_indexes =
-    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc_f Constant.equal funs this_block_funs_indexes
-  in
-  let (ind, sf) =
-         let ind = first_fun_kn,funs_indexes in
-           (ind,Univ.Instance.empty)(*FIXME*),prop_sort
-  in
-  let (sigma, scheme) =
-      Indrec.build_case_analysis_scheme_default env sigma ind sf
-  in
-  let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
-  let sorts =
-    (fun (_,_,x) ->
-       fst @@ UnivGen.fresh_sort_in_family x
-    )
-      fa
-  in
-  let princ_name =  (fun (x,_,_) -> x) fa in
-  let _ =
-  (*  Pp.msgnl (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++
-               pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs
-            );
-  *)
-    generate_functional_principle
-      (ref (Evd.from_env (Global.env ())))
-      false
-      scheme_type
-      (Some ([|sorts|]))
-      (Some princ_name)
-      this_block_funs
-      0
-      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|])
-  in
-  ()
-
-
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 7cadd4396d..6f060b0146 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -8,35 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Names
-open Constr
-
-val generate_functional_principle :
-  Evd.evar_map ref -> 
-  (* do we accept interactive proving *)
-  bool ->
-  (* induction principle on rel *)
-  types ->
-  (* *)
-  Sorts.t array option ->
-  (* Name of the new principle *)
-  (Id.t) option ->
-  (* the compute functions to use   *)
-  pconstant array ->
-  (* We prove the nth- principle *)
-  int  ->
-  (* The tactic to use to make the proof w.r
-     the number of params
-  *)
-  (EConstr.constr array -> int -> Tacmach.tactic) ->
-  unit
-
-exception No_graph_found
-
-val make_scheme
-  :  Evd.evar_map ref
-  -> (pconstant*Sorts.family) list
-  -> Evd.side_effects Proof_global.proof_entry list
-
-val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list ->  unit
-val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family)  ->  unit
+val compute_new_princ_type_from_rel
+  : Constr.constr array
+  -> Sorts.t array
+  -> Constr.t
+  -> Constr.types
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 1b75d3d966..d220058120 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -64,7 +64,7 @@ END
 TACTIC EXTEND newfuninv
 | [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] ->
      {
-       Proofview.V82.tactic (Invfun.invfun hyp fname)
+       Invfun.invfun hyp fname
      }
 END
 
@@ -202,10 +202,10 @@ VERNAC COMMAND EXTEND Function STATE CUSTOM
     -> {
          if is_interactive recsl then
            Vernacextend.VtOpenProof (fun () ->
-             do_generate_principle_interactive (List.map snd recsl))
+             Gen_principle.do_generate_principle_interactive (List.map snd recsl))
          else
            Vernacextend.VtDefault (fun () ->
-             do_generate_principle (List.map snd recsl)) }
+             Gen_principle.do_generate_principle (List.map snd recsl)) }
 END
 
 {
@@ -226,15 +226,15 @@ END
 
 let warning_error names e =
   match e with
-    | Building_graph e ->
-       let names = pr_enum Libnames.pr_qualid names in
-       let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
-       warn_cannot_define_graph (names,error)
-    | Defining_principle e ->
-       let names = pr_enum Libnames.pr_qualid names in
-       let error = if do_observe () then CErrors.print e else mt () in
-       warn_cannot_define_principle (names,error)
-    | _ -> raise e
+  | Building_graph e ->
+    let names = pr_enum Libnames.pr_qualid names in
+    let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
+    Gen_principle.warn_cannot_define_graph (names,error)
+  | Defining_principle e ->
+    let names = pr_enum Libnames.pr_qualid names in
+    let error = if do_observe () then CErrors.print e else mt () in
+    Gen_principle.warn_cannot_define_principle (names,error)
+  | _ -> raise e
 
 }
 
@@ -244,17 +244,17 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
    ->
     { begin
         try
-          Functional_principles_types.build_scheme fas
+          Gen_principle.build_scheme fas
         with
-        | Functional_principles_types.No_graph_found ->
+        | Gen_principle.No_graph_found ->
           begin
             match fas with
             | (_,fun_name,_)::_ ->
               begin
-                make_graph (Smartlocate.global_with_alias fun_name);
-                try Functional_principles_types.build_scheme fas
+                Gen_principle.make_graph (Smartlocate.global_with_alias fun_name);
+                try Gen_principle.build_scheme fas
                 with
-                | Functional_principles_types.No_graph_found ->
+                | Gen_principle.No_graph_found ->
                   CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
                 | e when CErrors.noncritical e ->
                   let names = List.map (fun (_,na,_) -> na) fas in
@@ -273,11 +273,11 @@ END
 VERNAC COMMAND EXTEND NewFunctionalCase
 | ["Functional" "Case" fun_scheme_arg(fas) ]
   => { Vernacextend.(VtSideff([pi1 fas], VtLater)) }
-  -> { Functional_principles_types.build_case_scheme fas }
+  -> { Gen_principle.build_case_scheme fas }
 END
 
 (***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 | ["Generate" "graph" "for" reference(c)] ->
-  { make_graph (Smartlocate.global_with_alias c) }
+  { Gen_principle.make_graph (Smartlocate.global_with_alias c) }
 END
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
new file mode 100644
index 0000000000..730ae48393
--- /dev/null
+++ b/plugins/funind/gen_principle.ml
@@ -0,0 +1,2069 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Names
+
+open Indfun_common
+
+module RelDecl = Context.Rel.Declaration
+
+let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
+
+(*
+   Construct a fixpoint as a Glob_term
+   and not as a constr
+*)
+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
+
+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 (Context.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 -> CErrors.user_err ~hdr:"Function" (Pp.str "Body of Function must be given")
+    in
+    States.with_state_protection (List.map f) lnameargsardef
+  in
+  recdef,rec_impls
+
+(* Checks whether or not the mutual bloc is recursive *)
+let is_rec names =
+  let open Glob_term in
+  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 _ -> CErrors.user_err (Pp.str "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 rebuild_bl aux bl typ =
+  let open Constrexpr in
+  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 =
+  let open Constrexpr in
+  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 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 } 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')
+
+let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+  (* First we get the type of the old graph principle *)
+  let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in
+  (*   let time1 = System.get_time ()  in *)
+  let new_principle_type =
+    Functional_principles_types.compute_new_princ_type_from_rel
+      (Array.map Constr.mkConstU funs)
+      sorts
+      old_princ_type
+  in
+  (*    let time2 = System.get_time ()  in *)
+  (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
+  let new_princ_name =
+    Namegen.next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
+  in
+  let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
+  evd := sigma;
+  let hook = DeclareDef.Hook.make (hook new_principle_type) in
+  let lemma =
+    Lemmas.start_lemma
+      ~name:new_princ_name
+      ~poly:false
+      !evd
+      (EConstr.of_constr new_principle_type)
+  in
+  (*       let _tim1 = System.get_time ()  in *)
+  let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
+  let lemma,_ = Lemmas.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) lemma in
+  (*       let _tim2 =  System.get_time ()  in *)
+  (*    begin *)
+  (*      let dur1 = System.time_difference tim1 tim2 in *)
+  (*      Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
+  (*    end; *)
+
+  let open Proof_global in
+  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  match entries with
+  | [entry] ->
+    name, entry, hook
+  | _ ->
+    CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
+
+let change_property_sort evd toSort princ princName =
+  let open Context.Rel.Declaration in
+  let princ = EConstr.of_constr princ in
+  let princ_info = Tactics.compute_elim_sig evd princ in
+  let change_sort_in_predicate decl =
+    LocalAssum
+    (get_annot decl,
+     let args,ty = Term.decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in
+     let s = Constr.destSort ty in
+       Global.add_constraints (Univ.enforce_leq (Sorts.univ_of_sort toSort) (Sorts.univ_of_sort s) Univ.Constraint.empty);
+       Term.compose_prod args (Constr.mkSort toSort)
+    )
+  in
+  let evd,princName_as_constr =
+    Evd.fresh_global
+      (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in
+  let init =
+    let nargs =  (princ_info.Tactics.nparams + (List.length  princ_info.Tactics.predicates)) in
+    Constr.mkApp(EConstr.Unsafe.to_constr princName_as_constr,
+                 Array.init nargs
+                   (fun i -> Constr.mkRel (nargs - i )))
+  in
+  evd, Term.it_mkLambda_or_LetIn
+    (Term.it_mkLambda_or_LetIn init
+       (List.map change_sort_in_predicate princ_info.Tactics.predicates)
+    )
+    (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params)
+
+let generate_functional_principle (evd: Evd.evar_map ref)
+    interactive_proof
+    old_princ_type sorts new_princ_name funs i proof_tac
+    =
+  try
+
+  let f = funs.(i) in
+  let sigma, type_sort = Evd.fresh_sort_in_family !evd Sorts.InType in
+  evd := sigma;
+  let new_sorts =
+    match sorts with
+      | None -> Array.make (Array.length funs) (type_sort)
+      | Some a -> a
+  in
+  let base_new_princ_name,new_princ_name =
+    match new_princ_name with
+      | Some (id) -> id,id
+      | None ->
+          let id_of_f = Label.to_id (Constant.label (fst f)) in
+          id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort)
+  in
+  let names = ref [new_princ_name] in
+  let hook =
+    fun new_principle_type _  ->
+    if Option.is_empty sorts
+    then
+      (*     let id_of_f = Label.to_id (con_label f) in *)
+      let register_with_sort fam_sort =
+        let evd' = Evd.from_env (Global.env ()) in
+        let evd',s = Evd.fresh_sort_in_family evd' fam_sort in
+        let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
+        let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
+        let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
+        (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+        let univs = Evd.univ_entry ~poly:false evd' in
+        let ce = Declare.definition_entry ~univs value in
+        ignore(
+          Declare.declare_constant
+            ~name
+            ~kind:Decls.(IsDefinition Scheme)
+            (Declare.DefinitionEntry ce)
+        );
+        Declare.definition_message name;
+        names := name :: !names
+      in
+      register_with_sort Sorts.InProp;
+      register_with_sort Sorts.InSet
+  in
+  let id,entry,hook =
+    build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
+    proof_tac hook
+  in
+  (* Pr  1278 :
+     Don't forget to close the goal if an error is raised !!!!
+  *)
+  let uctx = Evd.evar_universe_context sigma in
+  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(IsProof Theorem)
+  with e when CErrors.noncritical e ->
+    raise (Defining_principle e)
+
+let generate_principle (evd:Evd.evar_map ref) pconstants on_error
+    is_general do_built fix_rec_l 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 = Libnames.qualid_of_ident @@ mk_rel_id (List.nth names 0) in
+        let ind_kn =
+          fst (locate_with_msg
+                 Pp.(Libnames.pr_qualid f_R_mut ++ str ": Not an inductive type!")
+                 locate_ind
+                 f_R_mut)
+        in
+        let fname_kn { Vernacexpr.fname } =
+          let f_ref = Libnames.qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in
+          locate_with_msg
+            Pp.(Libnames.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) (Sorts.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
+               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 =
+  let open EConstr in
+  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 ->
+        CErrors.user_err ~hdr:"Function" Pp.(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
+
+(* [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 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
+    | [] | [_] -> CErrors.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 (Context.make_annot (Name res_id) Sorts.Relevant, lift 1 res_type) ::
+    LocalDef (Context.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 (Context.make_annot Anonymous Sorts.Relevant,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+  else LocalAssum (Context.make_annot Anonymous Sorts.Relevant,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+
+(**
+   [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
+    | Constr.Const c' -> c'
+    | _ -> CErrors.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
+
+(* [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 prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
+  let open Constr in
+  let open EConstr in
+  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 @@ Tactypes.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
+             | Tactypes.IntroNaming (Namegen.IntroIdentifier id) -> id::acc
+             | _ -> CErrors.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
+           | [] | [_] | [_;_] -> CErrors.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
+
+(* [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 ({Context.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 [EConstr.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 Constr in
+  let open EConstr in
+  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 Constr in
+  let open EConstr in
+  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 EConstr in
+  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 -> CErrors.user_err Pp.(str "No graph found")
+      in
+      if infos.is_general
+      || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs
+      then
+        let eq_lemma =
+          try Option.get (infos).equation_lemma
+          with Option.IsNone -> CErrors.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, Tactypes.NoBindings)
+                                                                          (Some (mkVar graph_principle_id, Tactypes.NoBindings)))))
+                          (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
+      ]
+      g
+
+exception No_graph_found
+
+let get_funs_constant mp =
+  let open Constr in
+  let exception Not_Rec in
+  let get_funs_constant const e : (Names.Constant.t*int) array =
+    match Constr.kind (Term.strip_lam e) with
+    | Fix((_,(na,_,_))) ->
+      Array.mapi
+        (fun i na ->
+           match na.Context.binder_name with
+           | Name id ->
+             let const = Constant.make2 mp (Label.of_id id) in
+             const,i
+           | Anonymous ->
+             CErrors.anomaly (Pp.str "Anonymous fix.")
+        )
+        na
+    | _ -> [|const,0|]
+  in
+  function const ->
+    let find_constant_body const =
+      match Global.body_of_constant Library.indirect_accessor const with
+        | Some (body, _, _) ->
+            let body = Tacred.cbv_norm_flags
+              (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
+              (Global.env ())
+              (Evd.from_env (Global.env ()))
+              (EConstr.of_constr body)
+            in
+            let body = EConstr.Unsafe.to_constr body in
+            body
+        | None ->
+          CErrors.user_err Pp.(str ( "Cannot define a principle over an axiom "))
+    in
+    let f = find_constant_body const in
+    let l_const = get_funs_constant const f in
+    (*
+       We need to check that all the functions found are in the same block
+       to prevent Reset strange thing
+    *)
+    let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
+    let l_params,l_fixes = List.split (List.map Term.decompose_lam l_bodies) in
+    (* all the parameters must be equal*)
+    let _check_params =
+      let first_params = List.hd l_params  in
+      List.iter
+        (fun params ->
+   if not (List.equal (fun (n1, c1) (n2, c2) ->
+       Context.eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
+           then CErrors.user_err Pp.(str "Not a mutal recursive block")
+        )
+        l_params
+    in
+    (* The bodies has to be very similar *)
+    let _check_bodies =
+      try
+        let extract_info is_first body =
+          match Constr.kind body with
+            | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
+            | _ ->
+                if is_first && Int.equal (List.length l_bodies) 1
+                then raise Not_Rec
+                else CErrors.user_err Pp.(str "Not a mutal recursive block")
+        in
+        let first_infos = extract_info true (List.hd l_bodies) in
+        let check body  = (* Hope this is correct *)
+          let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
+     Array.equal Int.equal ia1 ia2 && Array.equal (Context.eq_annot Name.equal) na1 na2 &&
+     Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
+          in
+          if not (eq_infos first_infos (extract_info false body))
+          then CErrors.user_err Pp.(str "Not a mutal recursive block")
+        in
+        List.iter check l_bodies
+      with Not_Rec -> ()
+    in
+    l_const
+
+let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list =
+  let exception Found_type of int in
+  let env = Global.env () in
+  let funs = List.map fst fas in
+  let first_fun = List.hd funs in
+  let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
+  let first_fun_kn =
+    try
+      fst (find_Function_infos  (fst first_fun)).graph_ind
+    with Not_found -> raise No_graph_found
+  in
+  let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
+  let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
+  let prop_sort = Sorts.InProp in
+  let funs_indexes =
+    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+    List.map
+      (function cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes)
+      funs
+  in
+  let ind_list =
+    List.map
+      (fun (idx) ->
+         let ind = first_fun_kn,idx in
+           (ind,snd first_fun),true,prop_sort
+      )
+      funs_indexes
+  in
+  let sigma, schemes =
+    Indrec.build_mutual_induction_scheme env !evd ind_list
+  in
+  let _ = evd := sigma in
+  let l_schemes =
+    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
+  in
+  let i = ref (-1) in
+  let sorts =
+    List.rev_map (fun (_,x) ->
+        let sigma, fs = Evd.fresh_sort_in_family !evd x in
+        evd := sigma; fs
+      )
+      fas
+  in
+  (* We create the first principle by tactic *)
+  let first_type,other_princ_types =
+    match l_schemes with
+        s::l_schemes -> s,l_schemes
+      | _ -> CErrors.anomaly (Pp.str "")
+  in
+  let _,const,_ =
+    try
+      build_functional_principle evd false
+        first_type
+        (Array.of_list sorts)
+        this_block_funs
+        0
+        (Functional_principles_proofs.prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
+        (fun _ _ -> ())
+    with e when CErrors.noncritical e ->
+      raise (Defining_principle e)
+
+  in
+  incr i;
+  let opacity =
+    let finfos = find_Function_infos (fst first_fun) in
+    try
+      let equation =  Option.get finfos.equation_lemma in
+      Declareops.is_opaque (Global.lookup_constant equation)
+    with Option.IsNone -> (* non recursive definition *)
+      false
+  in
+  let const = {const with Proof_global.proof_entry_opaque = opacity } in
+  (* The others are just deduced *)
+  if List.is_empty other_princ_types
+  then
+    [const]
+  else
+    let other_fun_princ_types =
+      let funs = Array.map Constr.mkConstU this_block_funs in
+      let sorts = Array.of_list sorts in
+      List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
+    in
+    let open Proof_global in
+    let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in
+    let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
+    let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
+    let other_result =
+      List.map (* we can now compute the other principles *)
+        (fun scheme_type ->
+           incr i;
+           observe (Printer.pr_lconstr_env env sigma scheme_type);
+           let type_concl = (Term.strip_prod_assum scheme_type) in
+           let applied_f = List.hd (List.rev (snd (Constr.decompose_app type_concl))) in
+           let f = fst (Constr.decompose_app applied_f) in
+           try (* we search the number of the function in the fix block (name of the function) *)
+             Array.iteri
+             (fun j t ->
+                let t =  (Term.strip_prod_assum t) in
+                let applied_g = List.hd (List.rev (snd (Constr.decompose_app t))) in
+                let g = fst (Constr.decompose_app applied_g) in
+                if Constr.equal f g
+                then raise (Found_type j);
+                observe Pp.(Printer.pr_lconstr_env env sigma f ++ str " <> " ++
+                            Printer.pr_lconstr_env env sigma g)
+
+             )
+             ta;
+             (* If we reach this point, the two principle are not mutually recursive
+                We fall back to the previous method
+                *)
+             let _,const,_ =
+               build_functional_principle
+                 evd
+                 false
+                 (List.nth other_princ_types (!i - 1))
+                 (Array.of_list sorts)
+                 this_block_funs
+                 !i
+                 (Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
+                 (fun _ _ -> ())
+             in
+             const
+         with Found_type i ->
+           let princ_body =
+             Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt
+           in
+           {const with
+              proof_entry_body =
+                (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
+              proof_entry_type = Some scheme_type
+           }
+      )
+      other_fun_princ_types
+    in
+    const::other_result
+
+(* [derive_correctness funs graphs] create correctness and completeness
+   lemmas for each function in [funs] w.r.t. [graphs]
+*)
+
+let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
+  let open EConstr in
+  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 Pp.(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 ))
+                  )
+                  (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,_) = EConstr.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 Pp.(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, Sorts.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"
+    Pp.(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) = EConstr.destConst evd c in
+           evd, (cst, EConstr.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 (EConstr.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 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, Libnames.qualid_of_ident fname,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 (Libnames.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]
+    with e when CErrors.noncritical e ->
+      (* No proof done *)
+      ()
+  in
+  Recdef.recursive_definition ~interactive_proof
+    ~is_mes fname 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
+        | _ -> CErrors.user_err (Pp.str "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 Decl_kinds.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 do_generate_principle_aux pconstants on_error register_built interactive_proof fixpoint_exprl : Lemmas.t option =
+  List.iter (fun { Vernacexpr.notations } ->
+      if not (List.is_empty notations)
+      then CErrors.user_err (Pp.str "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 ->
+        CErrors.user_err ~hdr:"Function" (Pp.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.CAst.v 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 ->
+          CErrors.user_err ~hdr:"Function" Pp.(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.CAst.v rec_impls wf_mes wf_rel_opt
+          (Option.map (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 _) } ->
+          CErrors.user_err
+            (Pp.str "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 warn_cannot_define_graph =
+  CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
+    (fun (names,error) ->
+       Pp.(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) ->
+       Pp.(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 ->
+      Pp.(spc () ++ CErrors.print e)
+    | _ ->
+      if do_observe ()
+      then Pp.(spc () ++ CErrors.print e)
+      else Pp.mt ()
+  in
+  match e with
+  | Building_graph e ->
+    let names = Pp.(prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) in
+    warn_cannot_define_graph (names,e_explain e)
+  | Defining_principle e ->
+    let names = Pp.(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 -> Pp.(spc () ++ CErrors.print e)
+    | _ -> if do_observe () then Pp.(spc () ++ CErrors.print e) else Pp.mt ()
+  in
+  match e with
+  | Building_graph e ->
+    CErrors.user_err
+      Pp.(str "Cannot define graph(s) for " ++
+          h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+          e_explain e)
+  | _ -> raise e
+
+(* [chop_n_arrow n t] chops the [n] first arrows in [t]
+   Acts on Constrexpr.constr_expr
+*)
+let rec chop_n_arrow n t =
+  let exception Stop of Constrexpr.constr_expr in
+  let open Constrexpr in
+  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')
+              | _ -> CErrors.anomaly (Pp.str "Not enough products.")
+            in
+            aux n nal_ta'
+          in
+          chop_n_arrow new_n t'
+        with Stop t -> t
+      end
+    | _ -> CErrors.anomaly (Pp.str "Not enough products.")
+
+let rec add_args id new_args =
+  let open Libnames in
+  let open Constrexpr in
+  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 _ ->
+        CErrors.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 _ ->
+                                   CErrors.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 _ ->
+                                     CErrors.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 _ ->
+        CErrors.anomaly ~label:"add_args " (Pp.str "CNotation.")
+      | CGeneralization _ ->
+        CErrors.anomaly ~label:"add_args " (Pp.str "CGeneralization.")
+      | CDelimiters _ ->
+        CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+    )
+
+let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr =
+  let open Constrexpr in
+  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 open Constrexpr in
+  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 ->
+          CErrors.user_err Pp.(str "Cannot find " ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c))
+      end
+    | _ ->
+      CErrors.user_err Pp.(str "Not a function reference")
+  in
+  (match Global.body_of_constant_body Library.indirect_accessor c_body with
+   | None ->
+     CErrors.user_err (Pp.str "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.Declarations.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 -> ()
+
+
+let build_scheme fas =
+  let evd = (ref (Evd.from_env (Global.env ()))) in
+  let pconstants = (List.map
+         (fun (_,f,sort) ->
+            let f_as_constant =
+              try
+                Smartlocate.global_with_alias f
+              with Not_found ->
+                CErrors.user_err ~hdr:"FunInd.build_scheme"
+                  Pp.(str "Cannot find " ++ Libnames.pr_qualid f)
+            in
+            let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
+            let _ = evd := evd' in
+            let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in
+            evd := sigma;
+            let c, u =
+              try EConstr.destConst !evd f
+              with Constr.DestKO ->
+                CErrors.user_err Pp.(Printer.pr_econstr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function")
+            in
+            (c, EConstr.EInstance.kind !evd u), sort
+         )
+         fas
+                   ) in
+  let bodies_types = make_scheme evd pconstants in
+
+  List.iter2
+    (fun (princ_id,_,_) def_entry ->
+       ignore
+         (Declare.declare_constant
+            ~name:princ_id
+            ~kind:Decls.(IsProof Theorem)
+            (Declare.DefinitionEntry def_entry));
+       Declare.definition_message princ_id
+    )
+    fas
+    bodies_types
+
+let build_case_scheme fa =
+  let env = Global.env ()
+  and sigma = (Evd.from_env (Global.env ())) in
+(*   let id_to_constr id =  *)
+(*     Constrintern.global_reference  id *)
+(*   in  *)
+  let funs =
+    let (_,f,_) = fa in
+    try (let open GlobRef in
+         match Smartlocate.global_with_alias f with
+         | ConstRef c -> c
+         | IndRef _ | ConstructRef _ | VarRef _ -> assert false)
+    with Not_found ->
+      CErrors.user_err ~hdr:"FunInd.build_case_scheme"
+        Pp.(str "Cannot find " ++ Libnames.pr_qualid f) in
+  let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
+  let first_fun = funs in
+  let funs_mp = Constant.modpath first_fun in
+  let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
+  let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
+  let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
+  let prop_sort = Sorts.InProp in
+  let funs_indexes =
+    let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+    List.assoc_f Constant.equal funs this_block_funs_indexes
+  in
+  let (ind, sf) =
+         let ind = first_fun_kn,funs_indexes in
+           (ind,Univ.Instance.empty)(*FIXME*),prop_sort
+  in
+  let (sigma, scheme) =
+      Indrec.build_case_analysis_scheme_default env sigma ind sf
+  in
+  let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
+  let sorts =
+    (fun (_,_,x) ->
+       fst @@ UnivGen.fresh_sort_in_family x
+    )
+      fa
+  in
+  let princ_name =  (fun (x,_,_) -> x) fa in
+  let _ : unit =
+  (*  Pp.msgnl (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++
+               pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs
+            );
+  *)
+    generate_functional_principle
+      (ref (Evd.from_env (Global.env ())))
+      false
+      scheme_type
+      (Some ([|sorts|]))
+      (Some princ_name)
+      this_block_funs
+      0
+      (Functional_principles_proofs.prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|])
+  in
+  ()
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
new file mode 100644
index 0000000000..7eb8ca3af1
--- /dev/null
+++ b/plugins/funind/gen_principle.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
+val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
+
+val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t
+val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
+
+val make_graph : Names.GlobRef.t -> unit
+
+(* Can be thrown by build_{,case}_scheme *)
+exception No_graph_found
+
+val build_scheme : (Names.Id.t * Libnames.qualid * Sorts.family) list -> unit
+val build_case_scheme : (Names.Id.t * Libnames.qualid * Sorts.family) -> unit
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6dc01a9f8f..798c62d549 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1554,5 +1554,3 @@ let build_inductive evd funconstants funsargs returned_types rtl =
     Detyping.print_universes := pu;
     Constrextern.print_universes := cu;
     raise (Building_graph e)
-
-
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1987677d7d..eeb2f246c2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -13,15 +13,10 @@ 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
 
@@ -150,777 +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')
-
-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
-      Invfun.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 -> ()
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index bfc9686ae5..97a840e950 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,19 +1,16 @@
-open Names
-open Tactypes
-
-val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
-
-val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
-
-val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
-
-val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
 
 val functional_induction :
   bool ->
   EConstr.constr ->
-  (EConstr.constr * EConstr.constr bindings) option ->
+  (EConstr.constr * EConstr.constr Tactypes.bindings) option ->
   Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-
-val make_graph : GlobRef.t -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a119586f7b..52a29fb559 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -10,8 +10,7 @@ let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
 let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
 let mk_equation_id id = Nameops.add_suffix id "_equation"
 
-let msgnl m =
-  ()
+let msgnl m = ()
 
 let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid)
 
@@ -378,7 +377,73 @@ let () = declare_bool_option function_debug_sig
 
 let do_observe () = !function_debug
 
+let observe strm =
+  if do_observe ()
+  then Feedback.msg_debug strm
+  else ()
+
+let debug_queue = Stack.create ()
+
+let print_debug_queue b e =
+  if not (Stack.is_empty debug_queue)
+  then
+    let lmsg,goal = Stack.pop debug_queue in
+    (if b then
+       Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
+     else
+       Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal))
+       (* print_debug_queue false e; *)
+    )
 
+let do_observe_tac s tac g =
+  let goal = Printer.pr_goal g in
+  let s = s (pf_env g) (project g) in
+  let lmsg = (str "observation : ") ++ s in
+  Stack.push (lmsg,goal) debug_queue;
+  try
+    let v = tac g in
+    ignore(Stack.pop debug_queue);
+    v
+  with reraise ->
+    let reraise = CErrors.push reraise in
+    if not (Stack.is_empty debug_queue)
+    then print_debug_queue true (fst reraise);
+    Util.iraise reraise
+
+let observe_tac s tac g =
+  if do_observe ()
+  then do_observe_tac s tac g
+  else tac g
+
+module New = struct
+
+let do_observe_tac ~header s tac =
+  let open Proofview.Notations in
+  let open Proofview in
+  Goal.enter begin fun gl ->
+    let goal = Printer.pr_goal (Goal.print gl) in
+    let env, sigma = Goal.env gl, Goal.sigma gl in
+    let s = s env sigma in
+    let lmsg = seq [header; str " : " ++ s] in
+    tclLIFT (NonLogical.make (fun () ->
+        Feedback.msg_debug (s++fnl()))) >>= fun () ->
+    tclOR (
+      Stack.push (lmsg, goal) debug_queue;
+      tac >>= fun v ->
+      ignore(Stack.pop debug_queue);
+      Proofview.tclUNIT v)
+      (fun (exn, info) ->
+         if not (Stack.is_empty debug_queue)
+         then print_debug_queue true exn;
+         tclZERO ~info exn)
+  end
+
+let observe_tac ~header s tac =
+  if do_observe ()
+  then do_observe_tac ~header s tac
+  else tac
+
+end
 
 let strict_tcc = ref false
 let is_strict_tcc () = !strict_tcc
@@ -430,6 +495,10 @@ let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_gl
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
+let make_eq () =
+  try EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
+  with _ -> assert false
+
 let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
   match r with
       GlobRef.ConstRef sp -> EvalConstRef sp
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index a95b1242ac..fff4711044 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -41,6 +41,7 @@ val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
+val make_eq : unit -> EConstr.constr
 
 val save
   :  Id.t
@@ -84,7 +85,21 @@ val update_Function : function_info -> unit
 val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t
 val pr_table : Environ.env -> Evd.evar_map -> Pp.t
 
+val observe_tac
+  : (Environ.env -> Evd.evar_map -> Pp.t)
+  -> Tacmach.tactic -> Tacmach.tactic
+
+module New : sig
+
+  val observe_tac
+    : header:Pp.t
+    -> (Environ.env -> Evd.evar_map -> Pp.t)
+    -> unit Proofview.tactic -> unit Proofview.tactic
+
+end
+
 (* val function_debug : bool ref  *)
+val observe : Pp.t -> unit
 val do_observe : unit -> bool
 val do_rewrite_dependent : unit -> bool
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index f6b5a06cac..38fdd789a3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -8,880 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Ltac_plugin
-open Declarations
-open CErrors
 open Util
 open Names
-open Term
 open Constr
-open Context
 open EConstr
-open Vars
-open Pp
-open Tacticals
+open Tacmach.New
 open Tactics
-open Indfun_common
-open Tacmach
-open Tactypes
-open Termops
-open Context.Rel.Declaration
-
-module RelDecl = Context.Rel.Declaration
-
-(* The local debugging mechanism *)
-(* let msgnl = Pp.msgnl *)
-
-let observe strm =
-  if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
-
-(*let observennl strm =
-  if do_observe ()
-  then begin Pp.msg strm;Pp.pp_flush () end
-  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 thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
-
-(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
-(* let id_to_constr id = *)
-(*   try *)
-(*     Constrintern.global_reference id *)
-(*   with Not_found -> *)
-(*     raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) *)
-
-
-let make_eq () =
-  try
-    EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
-  with _ -> assert false
-
-(* [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 =
-  (*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
-
-
-(*
-   [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
-
-
-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))
-
-
-(* [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 prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
-  fun g ->
-    (* first of all we recreate the lemmas types to be used as predicates of the induction principle
-       that is~:
-       \[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 = 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.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.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
-
+open Tacticals.New
 
-
-
-(* [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
-  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
-
-
-(* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
-       (unfolding, substituting, destructing cases \ldots)
- *)
-let tauto =
-  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
-
-let  rec intros_with_rewrite g =
-  observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
-and intros_with_rewrite_aux : Tacmach.tactic =
-  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 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
-
-
-(* [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 prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tactic =
-  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 = 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 (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]
-*)
-
-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 (observe_tac ("prove correctness ("^(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 = 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)
-    ()
+open Indfun_common
 
 (***********************************************)
 
@@ -891,38 +26,35 @@ let derive_correctness (funs: pconstant list) (graphs:inductive list) =
 
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
-let revert_graph kn post_tac hid g =
-    let sigma = project g in
-    let typ = pf_unsafe_type_of g (mkVar hid) in
-    match EConstr.kind sigma typ with
-      | App(i,args) when isInd sigma i ->
-          let ((kn',num) as ind'),u = destInd sigma i in
-          if MutInd.equal kn kn'
-          then (* We have generated a graph hypothesis so that we must change it if we can *)
-            let info =
-              try find_Function_of_graph ind'
-              with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
-                anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
-            in
-            (* if we can find a completeness lemma for this function
-               then we can come back to the functional form. If not, we do nothing
-            *)
-            match info.completeness_lemma with
-              | None -> tclIDTAC g
-              | Some f_complete ->
-                  let f_args,res = Array.chop (Array.length args - 1) args in
-                  tclTHENLIST
-                    [
-                      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
-                      thin [hid];
-                      Proofview.V82.of_tactic (Simple.intro hid);
-                      post_tac hid
-                    ]
-                    g
-
-          else tclIDTAC g
-      | _ -> tclIDTAC g
-
+let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
+  let sigma = project gl in
+  let typ = pf_unsafe_type_of gl (mkVar hid) in
+  match EConstr.kind sigma typ with
+  | App(i,args) when isInd sigma i ->
+    let ((kn',num) as ind'),u = destInd sigma i in
+    if MutInd.equal kn kn'
+    then (* We have generated a graph hypothesis so that we must change it if we can *)
+      let info =
+        try find_Function_of_graph ind'
+        with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+          CErrors.anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
+      in
+      (* if we can find a completeness lemma for this function
+         then we can come back to the functional form. If not, we do nothing
+      *)
+      match info.completeness_lemma with
+      | None -> tclIDTAC
+      | Some f_complete ->
+        let f_args,res = Array.chop (Array.length args - 1) args in
+        tclTHENLIST
+          [ generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]
+          ; clear [hid]
+          ; Simple.intro hid
+          ; post_tac hid
+          ]
+    else tclIDTAC
+  | _ -> tclIDTAC
+  )
 
 (*
    [functional_inversion hid fconst f_correct ] is the functional version of [inversion]
@@ -941,101 +73,91 @@ let revert_graph kn post_tac hid g =
    \end{enumerate}
 *)
 
-let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
-  fun g ->
-    let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let sigma = project g in
-    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
-    match EConstr.kind sigma type_of_h with
-      | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
-          let pre_tac,f_args,res =
-            match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
-              | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
-                  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
-              |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
-                 ((fun hid -> tclIDTAC),f_args,args.(1))
-              | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
-          in
-          tclTHENLIST [
-            pre_tac hid;
-            Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
-            thin [hid];
-            Proofview.V82.of_tactic (Simple.intro hid);
-            Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid));
-            (fun g ->
-               let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
-               tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
-            );
-          ] g
-      | _ -> tclFAIL 1 (mt ()) g
-
-
-let error msg = user_err Pp.(str msg)
+let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl ->
+  let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps gl) Id.Set.empty in
+  let sigma = project gl in
+  let type_of_h = pf_unsafe_type_of gl (mkVar hid) in
+  match EConstr.kind sigma type_of_h with
+  | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
+    let pre_tac,f_args,res =
+      match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
+      | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
+        ((fun hid -> intros_symmetry (Locusops.onHyp hid))),f_args,args.(2)
+      |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
+        ((fun hid -> tclIDTAC),f_args,args.(1))
+      | _ -> (fun hid -> tclFAIL 1 Pp.(mt ())),[||],args.(2)
+    in
+    tclTHENLIST
+      [ pre_tac hid
+      ; generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]
+      ; clear [hid]
+      ; Simple.intro hid
+      ; Inv.inv Inv.FullInversion None (Tactypes.NamedHyp hid)
+      ; Proofview.Goal.enter (fun gl ->
+            let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps gl) in
+            tclMAP (revert_graph kn pre_tac)  (hid::new_ids)
+          )
+      ]
+  | _ -> tclFAIL 1 Pp.(mt ())
+  )
 
 let invfun qhyp f  =
   let f =
     match f with
-      | GlobRef.ConstRef f -> f
-      | _ -> raise (CErrors.UserError(None,str "Not a function"))
+    | GlobRef.ConstRef f -> f
+    | _ ->
+      CErrors.user_err Pp.(str "Not a function")
   in
   try
     let finfos = find_Function_infos f in
     let f_correct = mkConst(Option.get finfos.correctness_lemma)
-    and kn = fst finfos.graph_ind
-    in
-    Proofview.V82.of_tactic (
-      Tactics.try_intros_until (fun hid -> Proofview.V82.tactic (functional_inversion kn hid (mkConst f)  f_correct)) qhyp
-    )
+    and kn = fst finfos.graph_ind in
+    Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
   with
-    | Not_found ->  error "No graph found"
-    | Option.IsNone  -> error "Cannot use equivalence with graph!"
+  | Not_found -> CErrors.user_err (Pp.str "No graph found")
+  | Option.IsNone  -> CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
 
 exception NoFunction
-let invfun qhyp f g =
+
+let invfun qhyp f =
   match f with
-    | Some f -> invfun qhyp f g
-    | None ->
-       Proofview.V82.of_tactic begin
-        Tactics.try_intros_until
-          (fun hid -> Proofview.V82.tactic begin fun g ->
-            let sigma = project g in
-             let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
-             match EConstr.kind sigma hyp_typ with
-               | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
-                   begin
-                     let f1,_ = decompose_app sigma args.(1) in
-                     try
-                       if not (isConst sigma f1) then raise NoFunction;
-                       let finfos = find_Function_infos (fst (destConst sigma f1)) in
-                       let f_correct = mkConst(Option.get finfos.correctness_lemma)
-                       and kn = fst finfos.graph_ind
-                       in
-                       functional_inversion kn hid f1 f_correct g
-                     with | NoFunction | Option.IsNone | Not_found ->
-                       try
-                         let f2,_ = decompose_app sigma args.(2) in
-                         if not (isConst sigma f2) then raise NoFunction;
-                         let finfos = find_Function_infos (fst (destConst sigma f2)) in
-                         let f_correct = mkConst(Option.get finfos.correctness_lemma)
-                         and kn = fst finfos.graph_ind
-                         in
-                         functional_inversion kn hid  f2 f_correct g
-                       with
-                         | NoFunction ->
-                             user_err  (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
-                         | Option.IsNone  ->
-                             if do_observe ()
-                             then
-                               error "Cannot use equivalence with graph for any side of the equality"
-                             else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-                         | Not_found ->
-                             if do_observe ()
-                             then
-                               error "No graph found for any side of equality"
-                             else user_err  (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-                   end
-               | _ -> user_err  (Ppconstr.pr_id hid ++ str " must be an equality ")
-          end)
-          qhyp
-          end
-          g
+  | Some f -> invfun qhyp f
+  | None ->
+    let tac_action hid gl =
+      let sigma = project gl in
+      let hyp_typ = pf_unsafe_type_of gl (mkVar hid)  in
+      match EConstr.kind sigma hyp_typ with
+      | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
+        begin
+          let f1,_ = decompose_app sigma args.(1) in
+          try
+            if not (isConst sigma f1) then raise NoFunction;
+            let finfos = find_Function_infos (fst (destConst sigma f1)) in
+            let f_correct = mkConst(Option.get finfos.correctness_lemma)
+            and kn = fst finfos.graph_ind
+            in
+            functional_inversion kn hid f1 f_correct
+          with | NoFunction | Option.IsNone | Not_found ->
+          try
+            let f2,_ = decompose_app sigma args.(2) in
+            if not (isConst sigma f2) then raise NoFunction;
+            let finfos = find_Function_infos (fst (destConst sigma f2)) in
+            let f_correct = mkConst(Option.get finfos.correctness_lemma)
+            and kn = fst finfos.graph_ind
+            in
+            functional_inversion kn hid  f2 f_correct
+          with
+          | NoFunction ->
+            CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
+          | Option.IsNone  ->
+            if do_observe ()
+            then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
+            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+          | Not_found ->
+            if do_observe ()
+            then CErrors.user_err (Pp.str "No graph found for any side of equality")
+            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+        end
+      | _ -> CErrors.user_err Pp.(Ppconstr.pr_id hid ++ str " must be an equality ")
+    in
+    try_intros_until (tac_action %> Proofview.Goal.enter) qhyp
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index c7538fae9a..6b789e1bb2 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -8,12 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val invfun :
-  Tactypes.quantified_hypothesis ->
-  Names.GlobRef.t option ->
-  Evar.t Evd.sigma -> Evar.t list Evd.sigma
-
-val derive_correctness
-  :  Constr.pconstant list
-  -> Names.inductive list
-  -> unit
+val invfun
+  :  Tactypes.quantified_hypothesis
+  -> Names.GlobRef.t option
+  -> unit Proofview.tactic
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 937118bf57..c62aa0cf6b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -199,54 +199,24 @@ let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> Glo
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
-
-
-(* Debugging mechanism *)
-let debug_queue = Stack.create ()
-
-let print_debug_queue b e =
-  if  not (Stack.is_empty debug_queue)
-  then
-    begin
-      let lmsg,goal = Stack.pop debug_queue in
-      if b then
-        Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.iprint e) ++ str " on goal" ++ fnl() ++ goal))
-      else
-        begin
-          Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
-        end;
-      (* print_debug_queue false e; *)
-    end
-
-let observe strm =
+let observe_tclTHENLIST s tacl =
   if do_observe ()
-  then Feedback.msg_debug strm
-  else ()
+  then
+    let rec aux n = function
+      | [] -> tclIDTAC
+      | [tac] -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) tac
+      | tac::tacl -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl))
+    in
+    aux 0 tacl
+  else tclTHENLIST tacl
 
+module New = struct
 
-let do_observe_tac s tac g =
-  let goal = Printer.pr_goal g in
-  let s = s (pf_env g) (project g) in
-  let lmsg = (str "recdef : ") ++ s in
-  observe (s++fnl());
-  Stack.push (lmsg,goal) debug_queue;
-  try
-    let v = tac g in
-    ignore(Stack.pop debug_queue);
-    v
-  with reraise ->
-    let reraise = CErrors.push reraise in
-    if not (Stack.is_empty debug_queue)
-    then print_debug_queue true reraise;
-    iraise reraise
-
-let observe_tac s tac g =
-  if do_observe ()
-  then do_observe_tac s tac g
-  else tac g
+  open Tacticals.New
 
+  let observe_tac = New.observe_tac ~header:(Pp.mt())
 
-let observe_tclTHENLIST s tacl =
+  let observe_tclTHENLIST s tacl =
   if do_observe ()
   then
     let rec aux n = function
@@ -257,38 +227,36 @@ let observe_tclTHENLIST s tacl =
     aux 0 tacl
   else tclTHENLIST tacl
 
+end
+
 (* Conclusion tactics *)
 
 (* 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 tclUSER tac is_mes l =
+  let open Tacticals.New in
   let clear_tac =
     match l with
-      | None -> tclIDTAC
-      | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l)
+    | None -> tclIDTAC
+    | Some l -> tclMAP (fun id -> tclTRY (clear [id])) (List.rev l)
   in
-  observe_tclTHENLIST (fun _ _ -> str "tclUSER1")
-    [
-      clear_tac;
+  New.observe_tclTHENLIST (fun _ _ -> str "tclUSER1")
+    [ clear_tac;
       if is_mes
-      then observe_tclTHENLIST (fun _ _ -> str "tclUSER2")
-        [
-          Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
-            (delayed_force Indfun_common.ltof_ref))]);
-         tac
-         ]
+      then
+        New.observe_tclTHENLIST (fun _ _ -> str "tclUSER2")
+          [ unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
+                                (delayed_force Indfun_common.ltof_ref))]
+          ; tac
+          ]
       else tac
     ]
-    g
 
 let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
   if is_mes
-  then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (delayed_force well_founded_ltof)) gl)
-  else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress)
-
-
-
-
+  then Tacticals.New.tclCOMPLETE (Simple.apply (delayed_force well_founded_ltof))
+  else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *)
+    (tclUSER concl_tac is_mes names_to_suppress)
 
 (* Traveling term.
    Both definitions of [f_terminate] and [f_equation] use the same generic
@@ -330,7 +298,7 @@ let check_not_nested env sigma forbidden e =
 (* ['a info] contains the local information for traveling *)
 type 'a infos =
     { nb_arg : int; (* function number of arguments *)
-      concl_tac : tactic; (* final tactic to finish proofs *)
+      concl_tac : unit Proofview.tactic; (* final tactic to finish proofs *)
       rec_arg_id : Id.t; (*name of the declared recursive argument *)
       is_mes : bool; (* type of recursion *)
       ih : Id.t; (* induction hypothesis name *)
@@ -803,6 +771,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ g =
                                 expr_info.eqs
                              )
                     );
+                    Proofview.V82.of_tactic @@
                     tclUSER expr_info.concl_tac true
                       (Some (
                       expr_info.ih::expr_info.acc_id::
@@ -1153,7 +1122,7 @@ let rec instantiate_lambda sigma t l =
       let (_, _, body) = destLambda sigma t in
       instantiate_lambda sigma (subst1 a body) l
 
-let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num  : tactic =
+let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num  : tactic =
   begin
     fun g ->
       let sigma = project g in
@@ -1195,7 +1164,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
                is_final = true;      (* and on leaf (more or less) *)
                f_terminate = delayed_force coq_O;
                nb_arg = nb_args;
-               concl_tac = concl_tac;
+               concl_tac;
                rec_arg_id = rec_arg_id;
                is_mes = is_mes;
                ih = hrec;
@@ -1213,7 +1182,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
           )
              g
         )
-        (tclUSER_if_not_mes concl_tac)
+        (fun b ids -> Proofview.V82.of_tactic (tclUSER_if_not_mes concl_tac b ids))
         g
   end
 
@@ -1320,50 +1289,47 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     let lid = ref [] in
     let h_num = ref (-1) in
     let env = Global.env () in
-    let lemma = build_proof env (Evd.from_env env)
-      (  fun gls ->
-           let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
-           observe_tclTHENLIST (fun _ _ -> str "")
-             [
-               Proofview.V82.of_tactic (generalize [lemma]);
-               Proofview.V82.of_tactic (Simple.intro hid);
-               (fun g ->
-                  let ids = pf_ids_of_hyps g in
+    let start_tac =
+      let open Tacmach.New in
+      let open Tacticals.New in
+      Proofview.Goal.enter (fun gl ->
+          let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gl) in
+          New.observe_tclTHENLIST (fun _ _ -> mt ())
+            [ generalize [lemma]
+            ; Simple.intro hid
+            ; Proofview.Goal.enter (fun gl ->
+                  let ids = pf_ids_of_hyps gl in
                   tclTHEN
-                    (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
-                    (fun g ->
-                       let ids' = pf_ids_of_hyps g in
-                       lid := List.rev (List.subtract Id.equal ids' ids);
-                       if List.is_empty !lid then lid := [hid];
-                       tclIDTAC g
-                    )
-                    g
-               );
-             ] gls)
-      (fun g ->
-        let sigma = project g in
-         match EConstr.kind sigma (pf_concl g) with
-           | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) ->
-               Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
-           | _ ->
-               incr h_num;
-               (observe_tac (fun _ _ -> str "finishing using")
-                  (
-                    tclCOMPLETE(
-                      tclFIRST[
-                        tclTHEN
-                          (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
-                          (Proofview.V82.of_tactic e_assumption);
-                      Eauto.eauto_with_bases
-                        (true,5)
-                        [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
-                        [Hints.Hint_db.empty TransparentState.empty false]
+                    (Elim.h_decompose_and (mkVar hid))
+                    (Proofview.Goal.enter (fun gl ->
+                         let ids' = pf_ids_of_hyps gl in
+                         lid := List.rev (List.subtract Id.equal ids' ids);
+                         if List.is_empty !lid then lid := [hid];
+                         tclIDTAC)))
+            ]) in
+    let end_tac =
+      let open Tacmach.New in
+      let open Tacticals.New in
+      Proofview.Goal.enter (fun gl ->
+          let sigma = project gl in
+          match EConstr.kind sigma (pf_concl gl) with
+          | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) ->
+            Auto.h_auto None [] (Some [])
+          | _ ->
+            incr h_num;
+            tclCOMPLETE(
+              tclFIRST
+                [ tclTHEN
+                    (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+                    e_assumption
+                ; Eauto.eauto_with_bases
+                      (true,5)
+                      [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
+                      [Hints.Hint_db.empty TransparentState.empty false
                       ]
-                    )
-                  )
-               )
-                 g)
-    in
+                ]
+            )) in
+    let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
@@ -1409,18 +1375,18 @@ let com_terminate
     thm_name using_lemmas
     nb_args ctx
     hook =
-  let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
+  let start_proof env ctx tac_start tac_end =
     let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
         ~info
         ctx
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in
-    let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in
+    let lemma = fst @@ Lemmas.by (New.observe_tac (fun _ _ -> str "starting_tac") tac_start) lemma in
     fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
                                    input_type relation rec_arg_num ))) lemma
   in
-  let lemma = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in
+  let lemma = start_proof Global.(env ()) ctx Tacticals.New.tclIDTAC Tacticals.New.tclIDTAC in
   try
     let sigma, new_goal_type = build_new_goal_type lemma in
     let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in
@@ -1469,7 +1435,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemm
                {nb_arg=nb_arg;
                 f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref);
                 f_constr = EConstr.of_constr f_constr;
-                concl_tac = tclIDTAC;
+                concl_tac = Tacticals.New.tclIDTAC;
                 func=functional_ref;
                 info=(instantiate_lambda Evd.empty
                         (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref)))
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index e6aa452def..3225411c85 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,10 +1,10 @@
 open Constr
 
-val tclUSER_if_not_mes :
-  Tacmach.tactic ->
-  bool ->
-  Names.Id.t list option ->
-  Tacmach.tactic
+val tclUSER_if_not_mes
+  : unit Proofview.tactic
+  -> bool
+  -> Names.Id.t list option
+  -> unit Proofview.tactic
 
 val recursive_definition
   :  interactive_proof:bool
diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack
index 755fa4f879..2adcfddd0a 100644
--- a/plugins/funind/recdef_plugin.mlpack
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -6,4 +6,5 @@ Functional_principles_proofs
 Functional_principles_types
 Invfun
 Indfun
+Gen_principle
 G_indfun