Merge PR #13021: Almost fully moving funind to new proof engine

Reviewed-by: ppedrot

6 files changed, 2370 insertions, 2383 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 72e6006b7e..e50c6087bb 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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 Printer
 open CErrors
 open Util
@@ -8,9 +18,7 @@ open Vars
 open Namegen
 open Names
 open Pp
-open Tacmach
 open Termops
-open Tacticals
 open Tactics
 open Indfun_common
 open Libnames
@@ -27,7 +35,7 @@ let make_refl_eq constructor type_of_t t =
   mkApp (constructor, [|type_of_t; t|])
 
 type pte_info =
-  {proving_tac : Id.t list -> Tacmach.tactic; is_valid : constr -> bool}
+  {proving_tac : Id.t list -> unit Proofview.tactic; is_valid : constr -> bool}
 
 type ptes_info = pte_info Id.Map.t
 
@@ -36,16 +44,12 @@ 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" (Proofview.V82.of_tactic assumption) g
+let observe_tac s =
+  New.observe_tac ~header:(str "observation") (fun _ _ -> Pp.str s)
 
-let refine c =
-  Proofview.V82.of_tactic
-    (Logic.refiner ~check:true EConstr.Unsafe.(to_constr c))
-
-let thin l = Proofview.V82.of_tactic (Tactics.clear l)
+let finish_proof dynamic_infos = observe_tac "finish" assumption
+let refine c = Logic.refiner ~check:true EConstr.Unsafe.(to_constr c)
+let thin = clear
 let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
 
 let is_trivial_eq sigma t =
@@ -83,37 +87,42 @@ let is_incompatible_eq 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 =
- fun g ->
-  let prov_id = pf_get_new_id hyp_id g in
-  tclTHENS
-    ((* observe_tac msg *) Proofview.V82.of_tactic
-       (assert_by (Name prov_id) t (Proofview.V82.tactic (tclCOMPLETE tac))))
-    [ tclTHENLIST
-        [ (* observe_tac "change_hyp_with_using thin" *)
-          thin [hyp_id]
-        ; (* observe_tac "change_hyp_with_using rename " *)
-          Proofview.V82.of_tactic (rename_hyp [(prov_id, hyp_id)]) ] ]
-    g
+let pf_get_new_id id env =
+  next_ident_away id (Id.Set.of_list (Termops.ids_of_named_context env))
+
+let change_hyp_with_using msg hyp_id t tac =
+  Proofview.Goal.enter (fun gl ->
+      let prov_id = pf_get_new_id hyp_id (Proofview.Goal.hyps gl) in
+      Tacticals.New.tclTHENS
+        ((* observe_tac msg *)
+         assert_by (Name prov_id) t
+           (Tacticals.New.tclCOMPLETE tac))
+        [ Tacticals.New.tclTHENLIST
+            [ (* observe_tac "change_hyp_with_using thin" *)
+              Tactics.clear [hyp_id]
+            ; (* observe_tac "change_hyp_with_using rename " *)
+              rename_hyp [(prov_id, hyp_id)] ] ])
 
 exception TOREMOVE
 
 let prove_trivial_eq h_id context (constructor, type_of_term, term) =
   let nb_intros = List.length context in
-  tclTHENLIST
-    [ tclDO nb_intros (Proofview.V82.of_tactic intro)
+  Tacticals.New.tclTHENLIST
+    [ Tacticals.New.tclDO nb_intros intro
     ; (* introducing context *)
-      (fun g ->
-        let context_hyps =
-          fst
-            (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g))
-        in
-        let context_hyps' =
-          mkApp (constructor, [|type_of_term; term|])
-          :: List.map mkVar context_hyps
-        in
-        let to_refine = applist (mkVar h_id, List.rev context_hyps') in
-        refine to_refine g) ]
+      Proofview.Goal.enter (fun g ->
+          let hyps = Proofview.Goal.hyps g in
+          let context_hyps =
+            fst
+              (list_chop ~msg:"prove_trivial_eq : " nb_intros
+                 (ids_of_named_context hyps))
+          in
+          let context_hyps' =
+            mkApp (constructor, [|type_of_term; term|])
+            :: List.map mkVar context_hyps
+          in
+          let to_refine = applist (mkVar h_id, List.rev context_hyps') in
+          refine to_refine) ]
 
 let find_rectype env sigma c =
   let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in
@@ -255,13 +264,11 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type =
              Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g)
                to_refine
            in
-           tclTHEN
-             (Proofview.Unsafe.tclEVARS evm)
-             (Proofview.V82.tactic (refine to_refine))))
+           tclTHEN (Proofview.Unsafe.tclEVARS evm) (refine to_refine)))
   in
   let simpl_eq_tac =
     change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp
-      (Proofview.V82.of_tactic prove_new_hyp)
+      prove_new_hyp
   in
   (*     observe (str "In " ++ Ppconstr.pr_id hyp_id ++  *)
   (*             str "removing an equation " ++ fnl ()++  *)
@@ -294,30 +301,30 @@ let isLetIn sigma t =
   match EConstr.kind sigma t with LetIn _ -> true | _ -> false
 
 let h_reduce_with_zeta cl =
-  Proofview.V82.of_tactic
-    (reduce
-       (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false})
-       cl)
+  reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}) cl
 
-let rewrite_until_var arg_num eq_ids : tactic =
+let rewrite_until_var arg_num eq_ids : unit Proofview.tactic =
+  let open Tacticals.New in
   (* tests if the declares recursive argument is neither a Constructor nor
      an applied Constructor since such a form for the recursive argument
      will break the Guard when trying to save the Lemma.
   *)
   let test_var g =
-    let sigma = project g in
-    let _, args = destApp sigma (pf_concl g) in
+    let sigma = Proofview.Goal.sigma g in
+    let _, args = destApp sigma (Proofview.Goal.concl g) in
     not (isConstruct sigma args.(arg_num) || isAppConstruct sigma args.(arg_num))
   in
-  let rec do_rewrite eq_ids g =
-    if test_var g then tclIDTAC g
-    else
-      match eq_ids with
-      | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property.")
-      | eq_id :: eq_ids ->
-        tclTHEN
-          (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
-          (do_rewrite eq_ids) g
+  let rec do_rewrite eq_ids =
+    Proofview.Goal.enter (fun g ->
+        if test_var g then Proofview.tclUNIT ()
+        else
+          match eq_ids with
+          | [] ->
+            anomaly (Pp.str "Cannot find a way to prove recursive property.")
+          | eq_id :: eq_ids ->
+            tclTHEN
+              (tclTRY (Equality.rewriteRL (mkVar eq_id)))
+              (do_rewrite eq_ids))
   in
   do_rewrite eq_ids
 
@@ -336,7 +343,8 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
     EConstr.of_constr
       (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I")
   in
-  let rec scan_type context type_of_hyp : tactic =
+  let open Tacticals.New in
+  let rec scan_type context type_of_hyp : unit Proofview.tactic =
     if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
       let reduced_type_of_hyp =
@@ -362,28 +370,27 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
         let prove_new_type_of_hyp =
           let context_length = List.length context in
           tclTHENLIST
-            [ tclDO context_length (Proofview.V82.of_tactic intro)
-            ; (fun g ->
-                let context_hyps_ids =
-                  fst
-                    (list_chop ~msg:"rec hyp : context_hyps" context_length
-                       (pf_ids_of_hyps g))
-                in
-                let rec_pte_id = pf_get_new_id rec_pte_id g in
-                let to_refine =
-                  applist
-                    ( mkVar hyp_id
-                    , List.rev_map mkVar (rec_pte_id :: context_hyps_ids) )
-                in
-                (*                   observe_tac "rec hyp " *)
-                (tclTHENS
-                   (Proofview.V82.of_tactic
-                      (assert_before (Name rec_pte_id) t_x))
-                   [ (* observe_tac "prove rec hyp" *)
-                     prove_rec_hyp eq_hyps
-                   ; (*                      observe_tac "prove rec hyp" *)
-                     refine to_refine ])
-                  g) ]
+            [ tclDO context_length intro
+            ; Proofview.Goal.enter (fun g ->
+                  let hyps = Proofview.Goal.hyps g in
+                  let context_hyps_ids =
+                    fst
+                      (list_chop ~msg:"rec hyp : context_hyps" context_length
+                         (ids_of_named_context hyps))
+                  in
+                  let rec_pte_id = pf_get_new_id rec_pte_id hyps in
+                  let to_refine =
+                    applist
+                      ( mkVar hyp_id
+                      , List.rev_map mkVar (rec_pte_id :: context_hyps_ids) )
+                  in
+                  (*                   observe_tac "rec hyp " *)
+                  tclTHENS
+                    (assert_before (Name rec_pte_id) t_x)
+                    [ (* observe_tac "prove rec hyp" *)
+                      prove_rec_hyp eq_hyps
+                    ; (*                      observe_tac "prove rec hyp" *)
+                      refine to_refine ]) ]
         in
         tclTHENLIST
           [ (*              observe_tac "hyp rec"  *)
@@ -408,19 +415,20 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
         let prove_trivial =
           let nb_intro = List.length context in
           tclTHENLIST
-            [ tclDO nb_intro (Proofview.V82.of_tactic intro)
-            ; (fun g ->
-                let context_hyps =
-                  fst
-                    (list_chop ~msg:"removing True : context_hyps " nb_intro
-                       (pf_ids_of_hyps g))
-                in
-                let to_refine =
-                  applist
-                    ( mkVar hyp_id
-                    , List.rev (coq_I :: List.map mkVar context_hyps) )
-                in
-                refine to_refine g) ]
+            [ tclDO nb_intro intro
+            ; Proofview.Goal.enter (fun g ->
+                  let hyps = Proofview.Goal.hyps g in
+                  let context_hyps =
+                    fst
+                      (list_chop ~msg:"removing True : context_hyps " nb_intro
+                         (ids_of_named_context hyps))
+                  in
+                  let to_refine =
+                    applist
+                      ( mkVar hyp_id
+                      , List.rev (coq_I :: List.map mkVar context_hyps) )
+                  in
+                  refine to_refine) ]
         in
         tclTHENLIST
           [ change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp
@@ -455,103 +463,103 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
   try (scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id])
   with TOREMOVE -> (thin [hyp_id], [])
 
-let clean_goal_with_heq ptes_infos continue_tac (dyn_infos : body_info) g =
-  let env = pf_env g and sigma = project g in
-  let tac, new_hyps =
-    List.fold_left
-      (fun (hyps_tac, new_hyps) hyp_id ->
-        let hyp_tac, new_hyp =
-          clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma
-        in
-        (tclTHEN hyp_tac hyps_tac, new_hyp @ new_hyps))
-      (tclIDTAC, []) dyn_infos.rec_hyps
-  in
-  let new_infos =
-    {dyn_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps}
-  in
-  tclTHENLIST
-    [tac; (* observe_tac "clean_hyp_with_heq continue" *) continue_tac new_infos]
-    g
+let clean_goal_with_heq ptes_infos continue_tac (dyn_infos : body_info) =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let env = Proofview.Goal.env g in
+      let sigma = Proofview.Goal.sigma g in
+      let tac, new_hyps =
+        List.fold_left
+          (fun (hyps_tac, new_hyps) hyp_id ->
+            let hyp_tac, new_hyp =
+              clean_hyp_with_heq ptes_infos dyn_infos.eq_hyps hyp_id env sigma
+            in
+            (tclTHEN hyp_tac hyps_tac, new_hyp @ new_hyps))
+          (tclIDTAC, []) dyn_infos.rec_hyps
+      in
+      let new_infos =
+        {dyn_infos with rec_hyps = new_hyps; nb_rec_hyps = List.length new_hyps}
+      in
+      tclTHENLIST
+        [ tac
+        ; (* observe_tac "clean_hyp_with_heq continue" *)
+          continue_tac new_infos ])
 
 let heq_id = Id.of_string "Heq"
 
-let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos g =
-  let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
-  tclTHENLIST
-    [ (* We first introduce the variables *)
-      tclDO nb_first_intro
-        (Proofview.V82.of_tactic
-           (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps)))
-    ; (* Then the equation itself *)
-      Proofview.V82.of_tactic
-        (intro_using_then heq_id
-           (* we get the fresh name with onLastHypId *)
-           (fun _ -> Proofview.tclUNIT ()))
-    ; onLastHypId (fun heq_id ->
-          tclTHENLIST
-            [ (* Then the new hypothesis *)
-              tclMAP
-                (fun id -> Proofview.V82.of_tactic (introduction id))
-                dyn_infos.rec_hyps
-            ; observe_tac "after_introduction" (fun g' ->
-                  (* We get infos on the equations introduced*)
-                  let new_term_value_eq = pf_get_hyp_typ g' heq_id in
-                  (* compute the new value of the body *)
-                  let new_term_value =
-                    match EConstr.kind (project g') new_term_value_eq with
-                    | App (f, [|_; _; args2|]) -> args2
-                    | _ ->
-                      observe
-                        ( str "cannot compute new term value : "
-                        ++ pr_gls g' ++ fnl () ++ str "last hyp is"
-                        ++ pr_leconstr_env (pf_env g') (project g')
-                             new_term_value_eq );
-                      anomaly (Pp.str "cannot compute new term value.")
-                  in
-                  let g', termtyp = tac_type_of g' term in
-                  let fun_body =
-                    mkLambda
-                      ( make_annot Anonymous Sorts.Relevant
-                      , termtyp
-                      , Termops.replace_term (project g') term (mkRel 1)
-                          dyn_infos.info )
-                  in
-                  let new_body =
-                    pf_nf_betaiota g' (mkApp (fun_body, [|new_term_value|]))
-                  in
-                  let new_infos =
-                    { dyn_infos with
-                      info = new_body
-                    ; eq_hyps = heq_id :: dyn_infos.eq_hyps }
-                  in
-                  clean_goal_with_heq ptes_infos continue_tac new_infos g') ])
-    ]
-    g
-
-let my_orelse tac1 tac2 g =
-  try tac1 g
-  with e when CErrors.noncritical e ->
-    (*     observe (str "using snd tac since : " ++ CErrors.print e); *)
-    tac2 g
+let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in
+      tclTHENLIST
+        [ (* We first introduce the variables *)
+          tclDO nb_first_intro
+            (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))
+        ; (* Then the equation itself *)
+          intro_using_then heq_id
+            (* we get the fresh name with onLastHypId *)
+            (fun _ -> Proofview.tclUNIT ())
+        ; onLastHypId (fun heq_id ->
+              tclTHENLIST
+                [ (* Then the new hypothesis *)
+                  tclMAP introduction dyn_infos.rec_hyps
+                ; observe_tac "after_introduction"
+                    (Proofview.Goal.enter (fun g' ->
+                         let env = Proofview.Goal.env g' in
+                         let sigma = Proofview.Goal.sigma g' in
+                         (* We get infos on the equations introduced*)
+                         let new_term_value_eq =
+                           Tacmach.New.pf_get_hyp_typ heq_id g'
+                         in
+                         (* compute the new value of the body *)
+                         let new_term_value =
+                           match EConstr.kind sigma new_term_value_eq with
+                           | App (f, [|_; _; args2|]) -> args2
+                           | _ ->
+                             observe
+                               ( str "cannot compute new term value : "
+                               ++ Tacmach.New.pr_gls g' ++ fnl ()
+                               ++ str "last hyp is"
+                               ++ pr_leconstr_env env sigma new_term_value_eq );
+                             anomaly (Pp.str "cannot compute new term value.")
+                         in
+                         tclTYPEOFTHEN term (fun sigma termtyp ->
+                             let fun_body =
+                               mkLambda
+                                 ( make_annot Anonymous Sorts.Relevant
+                                 , termtyp
+                                 , Termops.replace_term sigma term (mkRel 1)
+                                     dyn_infos.info )
+                             in
+                             let new_body =
+                               Reductionops.nf_betaiota env sigma
+                                 (mkApp (fun_body, [|new_term_value|]))
+                             in
+                             let new_infos =
+                               { dyn_infos with
+                                 info = new_body
+                               ; eq_hyps = heq_id :: dyn_infos.eq_hyps }
+                             in
+                             clean_goal_with_heq ptes_infos continue_tac
+                               new_infos))) ]) ])
 
-let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id =
+let instantiate_hyps_with_args (do_prove : Id.t list -> unit Proofview.tactic)
+    hyps args_id =
   let args = Array.of_list (List.map mkVar args_id) in
+  let open Tacticals.New in
   let instantiate_one_hyp hid =
-    my_orelse
-      (fun (* we instantiate the hyp if possible  *)
-             g ->
-        let prov_hid = pf_get_new_id hid g in
-        let c = mkApp (mkVar hid, args) in
-        let evm, _ = pf_apply Typing.type_of g c in
-        let open Tacticals.New in
-        Proofview.V82.of_tactic
-          (tclTHENLIST
-             [ Proofview.Unsafe.tclEVARS evm
-             ; pose_proof (Name prov_hid) c
-             ; clear [hid]
-             ; rename_hyp [(prov_hid, hid)] ])
-          g)
-      (fun (*
+    tclORELSE0
+      (* we instantiate the hyp if possible  *)
+      (Proofview.Goal.enter (fun g ->
+           let prov_hid = Tacmach.New.pf_get_new_id hid g in
+           let c = mkApp (mkVar hid, args) in
+           (* Check typing *)
+           tclTYPEOFTHEN c (fun _ _ ->
+               tclTHENLIST
+                 [ pose_proof (Name prov_hid) c
+                 ; thin [hid]
+                 ; rename_hyp [(prov_hid, hid)] ])))
+      (*
           if not then we are in a mutual function block
           and this hyp is a recursive hyp on an other function.
 
@@ -559,9 +567,8 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id =
           principle so that we can trash it
 
         *)
-             g ->
-        (*         observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *)
-        thin [hid] g)
+      (*         observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *)
+      (thin [hid])
   in
   if List.is_empty args_id then
     tclTHENLIST
@@ -571,172 +578,178 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id =
     tclTHENLIST
       [ tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps
       ; tclMAP instantiate_one_hyp hyps
-      ; (fun g ->
-          let all_g_hyps_id =
-            List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty
-          in
-          let remaining_hyps =
-            List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps
-          in
-          do_prove remaining_hyps g) ]
+      ; Proofview.Goal.enter (fun g ->
+            let all_g_hyps_id =
+              List.fold_right Id.Set.add
+                (Tacmach.New.pf_ids_of_hyps g)
+                Id.Set.empty
+            in
+            let remaining_hyps =
+              List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps
+            in
+            do_prove remaining_hyps) ]
 
 let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
-    dyn_infos : tactic =
-  let rec build_proof_aux do_finalize dyn_infos : tactic =
-   fun g ->
-    let env = pf_env g in
-    let sigma = project g in
-    (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
-    match EConstr.kind sigma dyn_infos.info with
-    | Case (ci, ct, iv, t, cb) ->
-      let do_finalize_t dyn_info' g =
-        let t = dyn_info'.info in
-        let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in
-        let g_nb_prod = nb_prod (project g) (pf_concl g) in
-        let g, type_of_term = tac_type_of g t in
-        let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in
-        tclTHENLIST
-          [ Proofview.V82.of_tactic
-              (generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps))
-          ; thin dyn_infos.rec_hyps
-          ; Proofview.V82.of_tactic
-              (pattern_option [(Locus.AllOccurrencesBut [1], t)] None)
-          ; (fun g ->
-              observe_tac "toto"
-                (tclTHENLIST
-                   [ Proofview.V82.of_tactic (Simple.case t)
-                   ; (fun g' ->
-                       let g'_nb_prod = nb_prod (project g') (pf_concl g') in
-                       let nb_instantiate_partial = g'_nb_prod - g_nb_prod in
-                       observe_tac "treat_new_case"
-                         (treat_new_case ptes_infos nb_instantiate_partial
-                            (build_proof do_finalize) t dyn_infos)
-                         g') ])
-                g) ]
-          g
-      in
-      build_proof do_finalize_t {dyn_infos with info = t} g
-    | Lambda (n, t, b) -> (
-      match EConstr.kind sigma (pf_concl g) with
-      | Prod _ ->
-        tclTHEN
-          (Proofview.V82.of_tactic intro)
-          (fun g' ->
-            let open Context.Named.Declaration in
-            let id = pf_last_hyp g' |> get_id in
-            let new_term =
-              pf_nf_betaiota g' (mkApp (dyn_infos.info, [|mkVar id|]))
+    dyn_infos : unit Proofview.tactic =
+  let open Tacticals.New in
+  let rec build_proof_aux do_finalize dyn_infos : unit Proofview.tactic =
+    Proofview.Goal.enter (fun g ->
+        let env = Proofview.Goal.env g in
+        let sigma = Proofview.Goal.sigma g in
+        (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
+        match EConstr.kind sigma dyn_infos.info with
+        | Case (ci, ct, iv, t, cb) ->
+          let do_finalize_t dyn_info' =
+            Proofview.Goal.enter (fun g ->
+                let t = dyn_info'.info in
+                let dyn_infos =
+                  {dyn_info' with info = mkCase (ci, ct, iv, t, cb)}
+                in
+                let g_nb_prod =
+                  nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
+                in
+                tclTYPEOFTHEN t (fun _ type_of_term ->
+                    let term_eq =
+                      make_refl_eq (Lazy.force refl_equal) type_of_term t
+                    in
+                    tclTHENLIST
+                      [ generalize (term_eq :: List.map mkVar dyn_infos.rec_hyps)
+                      ; thin dyn_infos.rec_hyps
+                      ; pattern_option [(Locus.AllOccurrencesBut [1], t)] None
+                      ; observe_tac "toto"
+                          (tclTHENLIST
+                             [ Simple.case t
+                             ; Proofview.Goal.enter (fun g' ->
+                                   let g'_nb_prod =
+                                     nb_prod (Proofview.Goal.sigma g')
+                                       (Proofview.Goal.concl g')
+                                   in
+                                   let nb_instantiate_partial =
+                                     g'_nb_prod - g_nb_prod
+                                   in
+                                   observe_tac "treat_new_case"
+                                     (treat_new_case ptes_infos
+                                        nb_instantiate_partial
+                                        (build_proof do_finalize) t dyn_infos))
+                             ]) ]))
+          in
+          build_proof do_finalize_t {dyn_infos with info = t}
+        | Lambda (n, t, b) -> (
+          match EConstr.kind sigma (Proofview.Goal.concl g) with
+          | Prod _ ->
+            tclTHEN intro
+              (Proofview.Goal.enter (fun g' ->
+                   let open Context.Named.Declaration in
+                   let id = Tacmach.New.pf_last_hyp g' |> get_id in
+                   let new_term =
+                     Reductionops.nf_betaiota (Proofview.Goal.env g')
+                       (Proofview.Goal.sigma g')
+                       (mkApp (dyn_infos.info, [|mkVar id|]))
+                   in
+                   let new_infos = {dyn_infos with info = new_term} in
+                   let do_prove new_hyps =
+                     build_proof do_finalize
+                       { new_infos with
+                         rec_hyps = new_hyps
+                       ; nb_rec_hyps = List.length new_hyps }
+                   in
+                   (*                         observe_tac "Lambda" *)
+                   instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]
+                   (*                            build_proof do_finalize new_infos g' *)))
+          | _ -> do_finalize dyn_infos )
+        | Cast (t, _, _) -> build_proof do_finalize {dyn_infos with info = t}
+        | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _
+         |Int _ | Float _ ->
+          do_finalize dyn_infos
+        | App (_, _) -> (
+          let f, args = decompose_app sigma dyn_infos.info in
+          match EConstr.kind sigma f with
+          | Int _ -> user_err Pp.(str "integer cannot be applied")
+          | Float _ -> user_err Pp.(str "float cannot be applied")
+          | Array _ -> user_err Pp.(str "array cannot be applied")
+          | App _ ->
+            assert false (* we have collected all the app in decompose_app *)
+          | Proj _ -> assert false (*FIXME*)
+          | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
+           |Prod _ ->
+            let new_infos = {dyn_infos with info = (f, args)} in
+            build_proof_args env sigma do_finalize new_infos
+          | Const (c, _) when not (List.mem_f Constant.equal c fnames) ->
+            let new_infos = {dyn_infos with info = (f, args)} in
+            (*                    Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
+            build_proof_args env sigma do_finalize new_infos
+          | Const _ -> do_finalize dyn_infos
+          | Lambda _ ->
+            let new_term = Reductionops.nf_beta env sigma dyn_infos.info in
+            build_proof do_finalize {dyn_infos with info = new_term}
+          | LetIn _ ->
+            let new_infos =
+              { dyn_infos with
+                info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
             in
-            let new_infos = {dyn_infos with info = new_term} in
-            let do_prove new_hyps =
-              build_proof do_finalize
-                { new_infos with
-                  rec_hyps = new_hyps
-                ; nb_rec_hyps = List.length new_hyps }
+            tclTHENLIST
+              [ tclMAP
+                  (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
+                  dyn_infos.rec_hyps
+              ; h_reduce_with_zeta Locusops.onConcl
+              ; build_proof do_finalize new_infos ]
+          | Cast (b, _, _) -> build_proof do_finalize {dyn_infos with info = b}
+          | Case _ | Fix _ | CoFix _ ->
+            let new_finalize dyn_infos =
+              let new_infos = {dyn_infos with info = (dyn_infos.info, args)} in
+              build_proof_args env sigma do_finalize new_infos
             in
-            (*                         observe_tac "Lambda" *)
-            (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
-            (*                            build_proof do_finalize new_infos g' *))
-          g
-      | _ -> do_finalize dyn_infos g )
-    | Cast (t, _, _) -> build_proof do_finalize {dyn_infos with info = t} g
-    | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _
-     |Float _ ->
-      do_finalize dyn_infos g
-    | App (_, _) -> (
-      let f, args = decompose_app sigma dyn_infos.info in
-      match EConstr.kind sigma f with
-      | Int _ -> user_err Pp.(str "integer cannot be applied")
-      | Float _ -> user_err Pp.(str "float cannot be applied")
-      | Array _ -> user_err Pp.(str "array cannot be applied")
-      | App _ ->
-        assert false (* we have collected all the app in decompose_app *)
-      | Proj _ -> assert false (*FIXME*)
-      | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _
-        ->
-        let new_infos = {dyn_infos with info = (f, args)} in
-        build_proof_args env sigma do_finalize new_infos g
-      | Const (c, _) when not (List.mem_f Constant.equal c fnames) ->
-        let new_infos = {dyn_infos with info = (f, args)} in
-        (*                    Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
-        build_proof_args env sigma do_finalize new_infos g
-      | Const _ -> do_finalize dyn_infos g
-      | Lambda _ ->
-        let new_term = Reductionops.nf_beta env sigma dyn_infos.info in
-        build_proof do_finalize {dyn_infos with info = new_term} g
-      | LetIn _ ->
-        let new_infos =
-          { dyn_infos with
-            info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
-        in
-        tclTHENLIST
-          [ tclMAP
-              (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
-              dyn_infos.rec_hyps
-          ; h_reduce_with_zeta Locusops.onConcl
-          ; build_proof do_finalize new_infos ]
-          g
-      | Cast (b, _, _) -> build_proof do_finalize {dyn_infos with info = b} g
-      | Case _ | Fix _ | CoFix _ ->
-        let new_finalize dyn_infos =
-          let new_infos = {dyn_infos with info = (dyn_infos.info, args)} in
-          build_proof_args env sigma do_finalize new_infos
-        in
-        build_proof new_finalize {dyn_infos with info = f} g )
-    | Fix _ | CoFix _ ->
-      user_err Pp.(str "Anonymous local (co)fixpoints are not handled yet")
-    | Proj _ -> user_err Pp.(str "Prod")
-    | Prod _ -> do_finalize dyn_infos g
-    | LetIn _ ->
-      let new_infos =
-        { dyn_infos with
-          info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
-      in
-      tclTHENLIST
-        [ tclMAP
-            (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
-            dyn_infos.rec_hyps
-        ; h_reduce_with_zeta Locusops.onConcl
-        ; build_proof do_finalize new_infos ]
-        g
-    | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
-    | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet")
-  and build_proof do_finalize dyn_infos g =
+            build_proof new_finalize {dyn_infos with info = f} )
+        | Fix _ | CoFix _ ->
+          user_err Pp.(str "Anonymous local (co)fixpoints are not handled yet")
+        | Proj _ -> user_err Pp.(str "Prod")
+        | Prod _ -> do_finalize dyn_infos
+        | LetIn _ ->
+          let new_infos =
+            { dyn_infos with
+              info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
+          in
+          tclTHENLIST
+            [ tclMAP
+                (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
+                dyn_infos.rec_hyps
+            ; h_reduce_with_zeta Locusops.onConcl
+            ; build_proof do_finalize new_infos ]
+        | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
+        | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet"))
+  and build_proof do_finalize dyn_infos =
     (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-    Indfun_common.observe_tac
+    Indfun_common.New.observe_tac ~header:(str "observation")
       (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 : tactic =
-   (* f_args'  args *)
-   fun g ->
-    let f_args', args = dyn_infos.info in
-    let tac : tactic =
-     fun g ->
-      match args with
-      | [] -> do_finalize {dyn_infos with info = f_args'} g
-      | arg :: args ->
-        (*                observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
-        (*                        fnl () ++  *)
-        (*                        pr_goal (Tacmach.sig_it g) *)
-        (*                        ); *)
-        let do_finalize dyn_infos =
-          let new_arg = dyn_infos.info in
-          (*              tclTRYD *)
-          build_proof_args env sigma do_finalize
-            {dyn_infos with info = (mkApp (f_args', [|new_arg|]), args)}
+  and build_proof_args env sigma do_finalize dyn_infos : unit Proofview.tactic =
+    (* f_args'  args *)
+    Proofview.Goal.enter (fun g ->
+        let f_args', args = dyn_infos.info in
+        let tac =
+          match args with
+          | [] -> do_finalize {dyn_infos with info = f_args'}
+          | arg :: args ->
+            (*                observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
+            (*                        fnl () ++  *)
+            (*                        pr_goal (Tacmach.sig_it g) *)
+            (*                        ); *)
+            let do_finalize dyn_infos =
+              let new_arg = dyn_infos.info in
+              (*              tclTRYD *)
+              build_proof_args env sigma do_finalize
+                {dyn_infos with info = (mkApp (f_args', [|new_arg|]), args)}
+            in
+            build_proof do_finalize {dyn_infos with info = arg}
         in
-        build_proof do_finalize {dyn_infos with info = arg} g
-    in
-    (* observe_tac "build_proof_args" *) tac g
+        (* observe_tac "build_proof_args" *) tac)
   in
   let do_finish_proof dyn_infos =
     (* tclTRYD *) clean_goal_with_heq ptes_infos finish_proof dyn_infos
   in
   (* observe_tac "build_proof" *)
-  fun g ->
-    build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g
+  build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos
 
 (* Proof of principles from structural functions *)
 
@@ -750,52 +763,59 @@ type static_fix_info =
   ; num_in_block : int }
 
 let prove_rec_hyp_for_struct fix_info eq_hyps =
-  tclTHEN (rewrite_until_var fix_info.idx eq_hyps) (fun g ->
-      let _, pte_args = destApp (project g) (pf_concl g) in
-      let rec_hyp_proof =
-        mkApp (mkVar fix_info.name, array_get_start pte_args)
-      in
-      refine rec_hyp_proof g)
+  let open Tacticals.New in
+  tclTHEN
+    (rewrite_until_var fix_info.idx eq_hyps)
+    (Proofview.Goal.enter (fun g ->
+         let _, pte_args =
+           destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
+         in
+         let rec_hyp_proof =
+           mkApp (mkVar fix_info.name, array_get_start pte_args)
+         in
+         refine rec_hyp_proof))
 
 let prove_rec_hyp fix_info =
   {proving_tac = prove_rec_hyp_for_struct fix_info; is_valid = (fun _ -> true)}
 
-let generalize_non_dep hyp g =
-  (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
-  let hyps = [hyp] in
-  let env = Global.env () in
-  let hyp_typ = pf_get_hyp_typ g hyp in
-  let to_revert, _ =
-    let open Context.Named.Declaration in
-    Environ.fold_named_context_reverse
-      (fun (clear, keep) decl ->
-        let decl = map_named_decl EConstr.of_constr decl in
-        let hyp = get_id decl in
-        if
-          Id.List.mem hyp hyps
-          || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep
-          || Termops.occur_var env (project g) hyp hyp_typ
-          || Termops.is_section_variable hyp
-          (* should be dangerous *)
-        then (clear, decl :: keep)
-        else (hyp :: clear, keep))
-      ~init:([], []) (pf_env g)
-  in
-  (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
-  tclTHEN
-    ((* observe_tac "h_generalize" *) Proofview.V82.of_tactic
-       (generalize (List.map mkVar to_revert)))
-    ((* observe_tac "thin" *) thin to_revert)
-    g
+let generalize_non_dep hyp =
+  Proofview.Goal.enter (fun g ->
+      (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
+      let hyps = [hyp] in
+      let env = Global.env () in
+      let sigma = Proofview.Goal.sigma g in
+      let hyp_typ = Tacmach.New.pf_get_hyp_typ hyp g in
+      let to_revert, _ =
+        let open Context.Named.Declaration in
+        Environ.fold_named_context_reverse
+          (fun (clear, keep) decl ->
+            let decl = map_named_decl EConstr.of_constr decl in
+            let hyp = get_id decl in
+            if
+              Id.List.mem hyp hyps
+              || List.exists (Termops.occur_var_in_decl env sigma hyp) keep
+              || Termops.occur_var env sigma hyp hyp_typ
+              || Termops.is_section_variable hyp
+              (* should be dangerous *)
+            then (clear, decl :: keep)
+            else (hyp :: clear, keep))
+          ~init:([], []) (Proofview.Goal.env g)
+      in
+      (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
+      Tacticals.New.tclTHEN
+        ((* observe_tac "h_generalize" *)
+         generalize (List.map mkVar to_revert))
+        ((* observe_tac "thin" *) clear to_revert))
 
 let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
 let var_of_decl = id_of_decl %> mkVar
 
 let revert idl =
-  tclTHEN (Proofview.V82.of_tactic (generalize (List.map mkVar idl))) (thin idl)
+  Tacticals.New.tclTHEN (generalize (List.map mkVar idl)) (clear idl)
 
 let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
     =
+  let open Tacticals.New in
   (*   observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
   (*   observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
   (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
@@ -843,16 +863,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let f_id = Label.to_id (Constant.label (fst (destConst evd f))) in
   let prove_replacement =
     tclTHENLIST
-      [ tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro)
-      ; observe_tac "" (fun g ->
-            let rec_id = pf_nth_hyp_id g 1 in
-            tclTHENLIST
-              [ observe_tac "generalize_non_dep in generate_equation_lemma"
-                  (generalize_non_dep rec_id)
-              ; observe_tac "h_case"
-                  (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)))
-              ; Proofview.V82.of_tactic intros_reflexivity ]
-              g) ]
+      [ tclDO (nb_params + rec_args_num + 1) intro
+      ; observe_tac ""
+          (onNthHypId 1 (fun rec_id ->
+               tclTHENLIST
+                 [ observe_tac "generalize_non_dep in generate_equation_lemma"
+                     (generalize_non_dep rec_id)
+                 ; observe_tac "h_case" (simplest_case (mkVar rec_id))
+                 ; intros_reflexivity ])) ]
   in
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
 
@@ -863,9 +881,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
     Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ()
   in
   let lemma = Declare.Proof.start ~cinfo ~info evd in
-  let lemma, _ =
-    Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
-  in
+  let lemma, _ = Declare.Proof.by prove_replacement lemma in
   let (_ : _ list) =
     Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent
       ~idopt:None
@@ -873,377 +889,398 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   evd
 
 let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num
-    all_funs g =
-  let equation_lemma =
-    try
-      let finfos =
-        match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
-        | None -> raise Not_found
-        | Some finfos -> finfos
-      in
-      mkConst (Option.get finfos.equation_lemma)
-    with (Not_found | Option.IsNone) as e ->
-      let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
-      (*i The next call to mk_equation_id is valid since we will construct the lemma
-        Ensures by: obvious
-        i*)
-      let equation_lemma_id = mk_equation_id f_id in
-      evd :=
-        generate_equation_lemma !evd all_funs f fun_num (List.length params)
-          (List.length rev_args_id) rec_arg_num;
-      let _ =
-        match e with
-        | Option.IsNone ->
+    all_funs =
+  Proofview.Goal.enter (fun g ->
+      let equation_lemma =
+        try
           let finfos =
-            match find_Function_infos (fst (destConst !evd f)) with
+            match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
             | None -> raise Not_found
             | Some finfos -> finfos
           in
-          update_Function
-            { finfos with
-              equation_lemma =
-                Some
-                  ( match Nametab.locate (qualid_of_ident equation_lemma_id) with
-                  | GlobRef.ConstRef c -> c
-                  | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) }
-        | _ -> ()
+          mkConst (Option.get finfos.equation_lemma)
+        with (Not_found | Option.IsNone) as e ->
+          let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
+          (*i The next call to mk_equation_id is valid since we will construct the lemma
+            Ensures by: obvious
+            i*)
+          let equation_lemma_id = mk_equation_id f_id in
+          evd :=
+            generate_equation_lemma !evd all_funs f fun_num (List.length params)
+              (List.length rev_args_id) rec_arg_num;
+          let _ =
+            match e with
+            | Option.IsNone ->
+              let finfos =
+                match find_Function_infos (fst (destConst !evd f)) with
+                | None -> raise Not_found
+                | Some finfos -> finfos
+              in
+              update_Function
+                { finfos with
+                  equation_lemma =
+                    Some
+                      ( match
+                          Nametab.locate (qualid_of_ident equation_lemma_id)
+                        with
+                      | GlobRef.ConstRef c -> c
+                      | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) }
+            | _ -> ()
+          in
+          (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
+          let evd', res =
+            Evd.fresh_global (Global.env ()) !evd
+              (Constrintern.locate_reference
+                 (qualid_of_ident equation_lemma_id))
+          in
+          evd := evd';
+          let sigma, _ =
+            Typing.type_of ~refresh:true (Global.env ()) !evd res
+          in
+          evd := sigma;
+          res
       in
-      (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
-      let evd', res =
-        Evd.fresh_global (Global.env ()) !evd
-          (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
+      let nb_intro_to_do =
+        nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g)
       in
-      evd := evd';
-      let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in
-      evd := sigma;
-      res
-  in
-  let nb_intro_to_do = nb_prod (project g) (pf_concl g) in
-  tclTHEN
-    (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro))
-    (fun g' ->
-      let just_introduced = nLastDecls nb_intro_to_do g' in
-      let open Context.Named.Declaration in
-      let just_introduced_id = List.map get_id just_introduced in
+      let open Tacticals.New in
       tclTHEN
-        (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
-        (revert just_introduced_id)
-        g')
-    g
+        (tclDO nb_intro_to_do intro)
+        (Proofview.Goal.enter (fun g' ->
+             let just_introduced = Tacticals.New.nLastDecls g' nb_intro_to_do in
+             let open Context.Named.Declaration in
+             let just_introduced_id = List.map get_id just_introduced in
+             tclTHEN
+               (* Hack to synchronize the goal with the global env *)
+               (Proofview.V82.tactic
+                  (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)))
+               (revert just_introduced_id))))
 
 let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
-    fnames all_funs _nparams : tactic =
- fun g ->
-  let princ_type = pf_concl g in
-  (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
-  (* Pp.msgnl (str "all_funs "); *)
-  (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
-  let princ_info = compute_elim_sig (project g) princ_type in
-  let fresh_id =
-    let avoid = ref (pf_ids_of_hyps g) in
-    fun na ->
-      let new_id =
-        match na with
-        | Name id -> fresh_id !avoid (Id.to_string id)
-        | Anonymous -> fresh_id !avoid "H"
+    fnames all_funs _nparams : unit Proofview.tactic =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let princ_type = Proofview.Goal.concl g in
+      let env = Proofview.Goal.env g in
+      let sigma = Proofview.Goal.sigma g in
+      (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
+      (* Pp.msgnl (str "all_funs "); *)
+      (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
+      let princ_info = compute_elim_sig sigma princ_type in
+      let fresh_id =
+        let avoid = ref (Tacmach.New.pf_ids_of_hyps g) in
+        fun na ->
+          let new_id =
+            match na with
+            | Name id -> fresh_id !avoid (Id.to_string id)
+            | Anonymous -> fresh_id !avoid "H"
+          in
+          avoid := new_id :: !avoid;
+          Name new_id
       in
-      avoid := new_id :: !avoid;
-      Name new_id
-  in
-  let fresh_decl = RelDecl.map_name fresh_id in
-  let princ_info : elim_scheme =
-    { princ_info with
-      params = List.map fresh_decl princ_info.params
-    ; predicates = List.map fresh_decl princ_info.predicates
-    ; branches = List.map fresh_decl princ_info.branches
-    ; args = List.map fresh_decl princ_info.args }
-  in
-  let get_body const =
-    match Global.body_of_constant Library.indirect_accessor const with
-    | Some (body, _, _) ->
-      let env = Global.env () in
-      let sigma = Evd.from_env env in
-      Tacred.cbv_norm_flags
-        (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-        env sigma (EConstr.of_constr body)
-    | None -> user_err Pp.(str "Cannot define a principle over an axiom ")
-  in
-  let fbody = get_body fnames.(fun_num) in
-  let f_ctxt, f_body = decompose_lam (project g) fbody in
-  let f_ctxt_length = List.length f_ctxt in
-  let diff_params = princ_info.nparams - f_ctxt_length in
-  let full_params, princ_params, fbody_with_full_params =
-    if diff_params > 0 then
-      let princ_params, full_params = list_chop diff_params princ_info.params in
-      ( full_params
-      , (* real params *)
-        princ_params
-      , (* the params of the principle which are not params of the function *)
-        substl (* function instantiated with real params *)
-          (List.map var_of_decl full_params)
-          f_body )
-    else
-      let f_ctxt_other, f_ctxt_params = list_chop (-diff_params) f_ctxt in
-      let f_body = compose_lam f_ctxt_other f_body in
-      ( princ_info.params
-      , (* real params *)
-        []
-      , (* all params are full params *)
-        substl (* function instantiated with real params *)
-          (List.map var_of_decl princ_info.params)
-          f_body )
-  in
-  observe
-    ( str "full_params := "
-    ++ prlist_with_sep spc
-         (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
-         full_params );
-  observe
-    ( str "princ_params := "
-    ++ prlist_with_sep spc
-         (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
-         princ_params );
-  observe
-    ( str "fbody_with_full_params := "
-    ++ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params );
-  let all_funs_with_full_params =
-    Array.map
-      (fun f -> applist (f, List.rev_map var_of_decl full_params))
-      all_funs
-  in
-  let fix_offset = List.length princ_params in
-  let ptes_to_fix, infos =
-    match EConstr.kind (project g) fbody_with_full_params with
-    | Fix ((idxs, i), (names, typess, bodies)) ->
-      let bodies_with_all_params =
-        Array.map
-          (fun body ->
-            Reductionops.nf_betaiota (pf_env g) (project g)
-              (applist
-                 ( substl
-                     (List.rev (Array.to_list all_funs_with_full_params))
-                     body
-                 , List.rev_map var_of_decl princ_params )))
-          bodies
+      let fresh_decl = RelDecl.map_name fresh_id in
+      let princ_info : elim_scheme =
+        { princ_info with
+          params = List.map fresh_decl princ_info.params
+        ; predicates = List.map fresh_decl princ_info.predicates
+        ; branches = List.map fresh_decl princ_info.branches
+        ; args = List.map fresh_decl princ_info.args }
       in
-      let info_array =
-        Array.mapi
-          (fun i types ->
-            let types =
-              prod_applist (project g) types
-                (List.rev_map var_of_decl princ_params)
-            in
-            { idx = idxs.(i) - fix_offset
-            ; name = Nameops.Name.get_id (fresh_id names.(i).binder_name)
-            ; types
-            ; offset = fix_offset
-            ; nb_realargs =
-                List.length (fst (decompose_lam (project g) bodies.(i)))
-                - fix_offset
-            ; body_with_param = bodies_with_all_params.(i)
-            ; num_in_block = i })
-          typess
+      let get_body const =
+        match Global.body_of_constant Library.indirect_accessor const with
+        | Some (body, _, _) ->
+          let env = Global.env () in
+          let sigma = Evd.from_env env in
+          Tacred.cbv_norm_flags
+            (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
+            env sigma (EConstr.of_constr body)
+        | None -> user_err Pp.(str "Cannot define a principle over an axiom ")
       in
-      let pte_to_fix, rev_info =
-        List.fold_left_i
-          (fun i (acc_map, acc_info) decl ->
-            let pte = RelDecl.get_name decl in
-            let infos = info_array.(i) in
-            let type_args, _ = decompose_prod (project g) infos.types in
-            let nargs = List.length type_args in
-            let f =
-              applist
-                (mkConst fnames.(i), List.rev_map var_of_decl princ_info.params)
-            in
-            let first_args = Array.init nargs (fun i -> mkRel (nargs - i)) in
-            let app_f = mkApp (f, first_args) in
-            let pte_args = Array.to_list first_args @ [app_f] in
-            let app_pte = applist (mkVar (Nameops.Name.get_id pte), pte_args) in
-            let body_with_param, num =
-              let body = get_body fnames.(i) in
-              let body_with_full_params =
-                Reductionops.nf_betaiota (pf_env g) (project g)
-                  (applist (body, List.rev_map var_of_decl full_params))
-              in
-              match EConstr.kind (project g) body_with_full_params with
-              | Fix ((_, num), (_, _, bs)) ->
-                ( Reductionops.nf_betaiota (pf_env g) (project g)
-                    (applist
-                       ( substl
-                           (List.rev (Array.to_list all_funs_with_full_params))
-                           bs.(num)
-                       , List.rev_map var_of_decl princ_params ))
-                , num )
-              | _ -> user_err Pp.(str "Not a mutual block")
-            in
-            let info =
-              { infos with
-                types = compose_prod type_args app_pte
-              ; body_with_param
-              ; num_in_block = num }
-            in
-            (*                 observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++  *)
-            (*                            str " to " ++ Ppconstr.pr_id info.name); *)
-            (Id.Map.add (Nameops.Name.get_id pte) info acc_map, info :: acc_info))
-          0 (Id.Map.empty, [])
-          (List.rev princ_info.predicates)
+      let fbody = get_body fnames.(fun_num) in
+      let f_ctxt, f_body = decompose_lam sigma fbody in
+      let f_ctxt_length = List.length f_ctxt in
+      let diff_params = princ_info.nparams - f_ctxt_length in
+      let full_params, princ_params, fbody_with_full_params =
+        if diff_params > 0 then
+          let princ_params, full_params =
+            list_chop diff_params princ_info.params
+          in
+          ( full_params
+          , (* real params *)
+            princ_params
+          , (* the params of the principle which are not params of the function *)
+            substl (* function instantiated with real params *)
+              (List.map var_of_decl full_params)
+              f_body )
+        else
+          let f_ctxt_other, f_ctxt_params = list_chop (-diff_params) f_ctxt in
+          let f_body = compose_lam f_ctxt_other f_body in
+          ( princ_info.params
+          , (* real params *)
+            []
+          , (* all params are full params *)
+            substl (* function instantiated with real params *)
+              (List.map var_of_decl princ_info.params)
+              f_body )
       in
-      (pte_to_fix, List.rev rev_info)
-    | _ -> (Id.Map.empty, [])
-  in
-  let mk_fixes : tactic =
-    let pre_info, infos = list_chop fun_num infos in
-    match (pre_info, infos) with
-    | _, [] -> tclIDTAC
-    | _, this_fix_info :: others_infos ->
-      let other_fix_infos =
-        List.map
-          (fun fi -> (fi.name, fi.idx + 1, fi.types))
-          (pre_info @ others_infos)
+      observe
+        ( str "full_params := "
+        ++ prlist_with_sep spc
+             (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
+             full_params );
+      observe
+        ( str "princ_params := "
+        ++ prlist_with_sep spc
+             (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
+             princ_params );
+      observe
+        ( str "fbody_with_full_params := "
+        ++ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params );
+      let all_funs_with_full_params =
+        Array.map
+          (fun f -> applist (f, List.rev_map var_of_decl full_params))
+          all_funs
       in
-      if List.is_empty other_fix_infos then
-        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
-          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)
-  in
-  let first_tac : tactic =
-    (* every operations until fix creations *)
-    (* names are already refreshed *)
-    tclTHENLIST
-      [ observe_tac "introducing params"
-          (Proofview.V82.of_tactic
-             (intros_mustbe_force (List.rev_map id_of_decl princ_info.params)))
-      ; observe_tac "introducing predictes"
-          (Proofview.V82.of_tactic
-             (intros_mustbe_force
-                (List.rev_map id_of_decl princ_info.predicates)))
-      ; observe_tac "introducing branches"
-          (Proofview.V82.of_tactic
-             (intros_mustbe_force (List.rev_map id_of_decl princ_info.branches)))
-      ; observe_tac "building fixes" mk_fixes ]
-  in
-  let intros_after_fixes : tactic =
-   fun gl ->
-    let ctxt, pte_app = decompose_prod_assum (project gl) (pf_concl gl) in
-    let pte, pte_args = decompose_app (project gl) pte_app in
-    try
-      let pte =
-        try destVar (project gl) pte
-        with DestKO -> anomaly (Pp.str "Property is not a variable.")
+      let fix_offset = List.length princ_params in
+      let ptes_to_fix, infos =
+        match EConstr.kind sigma fbody_with_full_params with
+        | Fix ((idxs, i), (names, typess, bodies)) ->
+          let bodies_with_all_params =
+            Array.map
+              (fun body ->
+                Reductionops.nf_betaiota env sigma
+                  (applist
+                     ( substl
+                         (List.rev (Array.to_list all_funs_with_full_params))
+                         body
+                     , List.rev_map var_of_decl princ_params )))
+              bodies
+          in
+          let info_array =
+            Array.mapi
+              (fun i types ->
+                let types =
+                  prod_applist sigma types
+                    (List.rev_map var_of_decl princ_params)
+                in
+                { idx = idxs.(i) - fix_offset
+                ; name = Nameops.Name.get_id (fresh_id names.(i).binder_name)
+                ; types
+                ; offset = fix_offset
+                ; nb_realargs =
+                    List.length (fst (decompose_lam sigma bodies.(i)))
+                    - fix_offset
+                ; body_with_param = bodies_with_all_params.(i)
+                ; num_in_block = i })
+              typess
+          in
+          let pte_to_fix, rev_info =
+            List.fold_left_i
+              (fun i (acc_map, acc_info) decl ->
+                let pte = RelDecl.get_name decl in
+                let infos = info_array.(i) in
+                let type_args, _ = decompose_prod sigma infos.types in
+                let nargs = List.length type_args in
+                let f =
+                  applist
+                    ( mkConst fnames.(i)
+                    , List.rev_map var_of_decl princ_info.params )
+                in
+                let first_args =
+                  Array.init nargs (fun i -> mkRel (nargs - i))
+                in
+                let app_f = mkApp (f, first_args) in
+                let pte_args = Array.to_list first_args @ [app_f] in
+                let app_pte =
+                  applist (mkVar (Nameops.Name.get_id pte), pte_args)
+                in
+                let body_with_param, num =
+                  let body = get_body fnames.(i) in
+                  let body_with_full_params =
+                    Reductionops.nf_betaiota env sigma
+                      (applist (body, List.rev_map var_of_decl full_params))
+                  in
+                  match EConstr.kind sigma body_with_full_params with
+                  | Fix ((_, num), (_, _, bs)) ->
+                    ( Reductionops.nf_betaiota env sigma
+                        (applist
+                           ( substl
+                               (List.rev
+                                  (Array.to_list all_funs_with_full_params))
+                               bs.(num)
+                           , List.rev_map var_of_decl princ_params ))
+                    , num )
+                  | _ -> user_err Pp.(str "Not a mutual block")
+                in
+                let info =
+                  { infos with
+                    types = compose_prod type_args app_pte
+                  ; body_with_param
+                  ; num_in_block = num }
+                in
+                (*                 observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++  *)
+                (*                            str " to " ++ Ppconstr.pr_id info.name); *)
+                ( Id.Map.add (Nameops.Name.get_id pte) info acc_map
+                , info :: acc_info ))
+              0 (Id.Map.empty, [])
+              (List.rev princ_info.predicates)
+          in
+          (pte_to_fix, List.rev rev_info)
+        | _ -> (Id.Map.empty, [])
       in
-      let fix_info = Id.Map.find pte ptes_to_fix in
-      let nb_args = fix_info.nb_realargs in
-      tclTHENLIST
-        [ (* observe_tac ("introducing args") *)
-          tclDO nb_args (Proofview.V82.of_tactic intro)
-        ; (fun g ->
-            (* replacement of the function by its body *)
-            let args = nLastDecls nb_args g in
-            let fix_body = fix_info.body_with_param in
-            (*               observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
-            let open Context.Named.Declaration in
-            let args_id = List.map get_id args in
-            let dyn_infos =
-              { nb_rec_hyps = -100
-              ; rec_hyps = []
-              ; info =
-                  Reductionops.nf_betaiota (pf_env g) (project g)
-                    (applist (fix_body, List.rev_map mkVar args_id))
-              ; eq_hyps = [] }
-            in
-            tclTHENLIST
-              [ observe_tac "do_replace"
-                  (do_replace evd full_params
-                     (fix_info.idx + List.length princ_params)
-                     ( args_id
-                     @ List.map
-                         (RelDecl.get_name %> Nameops.Name.get_id)
-                         princ_params )
-                     all_funs.(fix_info.num_in_block)
-                     fix_info.num_in_block all_funs)
-              ; (let do_prove =
-                   build_proof interactive_proof (Array.to_list fnames)
-                     (Id.Map.map prove_rec_hyp ptes_to_fix)
-                 in
-                 let prove_tac branches =
-                   let dyn_infos =
-                     { dyn_infos with
-                       rec_hyps = branches
-                     ; nb_rec_hyps = List.length branches }
-                   in
-                   observe_tac "cleaning"
-                     (clean_goal_with_heq
-                        (Id.Map.map prove_rec_hyp ptes_to_fix)
-                        do_prove dyn_infos)
-                 in
-                 (*                   observe (str "branches := " ++ *)
-                 (*                              prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++  fnl () ++ *)
-                 (*                         str "args := " ++ prlist_with_sep spc Ppconstr.pr_id  args_id *)
+      let mk_fixes : unit Proofview.tactic =
+        let pre_info, infos = list_chop fun_num infos in
+        match (pre_info, infos) with
+        | _, [] -> Proofview.tclUNIT ()
+        | _, this_fix_info :: others_infos ->
+          let other_fix_infos =
+            List.map
+              (fun fi -> (fi.name, fi.idx + 1, fi.types))
+              (pre_info @ others_infos)
+          in
+          if List.is_empty other_fix_infos then
+            if this_fix_info.idx + 1 = 0 then Proofview.tclUNIT ()
+              (* Someone  tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
+            else
+              Indfun_common.New.observe_tac ~header:(str "observation")
+                (fun _ _ -> str "h_fix " ++ int (this_fix_info.idx + 1))
+                (fix this_fix_info.name (this_fix_info.idx + 1))
+          else
+            Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+              other_fix_infos 0
+      in
+      let first_tac : unit Proofview.tactic =
+        (* every operations until fix creations *)
+        (* names are already refreshed *)
+        tclTHENLIST
+          [ observe_tac "introducing params"
+              (intros_mustbe_force (List.rev_map id_of_decl princ_info.params))
+          ; observe_tac "introducing predicates"
+              (intros_mustbe_force
+                 (List.rev_map id_of_decl princ_info.predicates))
+          ; observe_tac "introducing branches"
+              (intros_mustbe_force
+                 (List.rev_map id_of_decl princ_info.branches))
+          ; observe_tac "building fixes" mk_fixes ]
+      in
+      let intros_after_fixes : unit Proofview.tactic =
+        Proofview.Goal.enter (fun gl ->
+            let sigma = Proofview.Goal.sigma gl in
+            let ccl = Proofview.Goal.concl gl in
+            let ctxt, pte_app = decompose_prod_assum sigma ccl in
+            let pte, pte_args = decompose_app sigma pte_app in
+            try
+              let pte =
+                try destVar sigma pte
+                with DestKO -> anomaly (Pp.str "Property is not a variable.")
+              in
+              let fix_info = Id.Map.find pte ptes_to_fix in
+              let nb_args = fix_info.nb_realargs in
+              tclTHENLIST
+                [ (* observe_tac ("introducing args") *)
+                  tclDO nb_args intro
+                ; Proofview.Goal.enter (fun g ->
+                      (* replacement of the function by its body *)
+                      let args = Tacticals.New.nLastDecls g nb_args in
+                      let fix_body = fix_info.body_with_param in
+                      (*               observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
+                      let open Context.Named.Declaration in
+                      let args_id = List.map get_id args in
+                      let dyn_infos =
+                        { nb_rec_hyps = -100
+                        ; rec_hyps = []
+                        ; info =
+                            Reductionops.nf_betaiota (Proofview.Goal.env g)
+                              (Proofview.Goal.sigma g)
+                              (applist (fix_body, List.rev_map mkVar args_id))
+                        ; eq_hyps = [] }
+                      in
+                      tclTHENLIST
+                        [ observe_tac "do_replace"
+                            (do_replace evd full_params
+                               (fix_info.idx + List.length princ_params)
+                               ( args_id
+                               @ List.map
+                                   (RelDecl.get_name %> Nameops.Name.get_id)
+                                   princ_params )
+                               all_funs.(fix_info.num_in_block)
+                               fix_info.num_in_block all_funs)
+                        ; (let do_prove =
+                             build_proof interactive_proof
+                               (Array.to_list fnames)
+                               (Id.Map.map prove_rec_hyp ptes_to_fix)
+                           in
+                           let prove_tac branches =
+                             let dyn_infos =
+                               { dyn_infos with
+                                 rec_hyps = branches
+                               ; nb_rec_hyps = List.length branches }
+                             in
+                             observe_tac "cleaning"
+                               (clean_goal_with_heq
+                                  (Id.Map.map prove_rec_hyp ptes_to_fix)
+                                  do_prove dyn_infos)
+                           in
+                           (*                   observe (str "branches := " ++ *)
+                           (*                              prlist_with_sep spc (fun decl -> Ppconstr.pr_id (id_of_decl decl)) princ_info.branches ++  fnl () ++ *)
+                           (*                         str "args := " ++ prlist_with_sep spc Ppconstr.pr_id  args_id *)
 
-                 (*                         ); *)
-                 (* observe_tac "instancing" *)
-                 instantiate_hyps_with_args prove_tac
-                   (List.rev_map id_of_decl princ_info.branches)
-                   (List.rev args_id)) ]
-              g) ]
-        gl
-    with Not_found ->
-      let nb_args = min princ_info.nargs (List.length ctxt) in
-      tclTHENLIST
-        [ tclDO nb_args (Proofview.V82.of_tactic intro)
-        ; (fun g ->
-            (* replacement of the function by its body *)
-            let args = nLastDecls nb_args g in
-            let open Context.Named.Declaration in
-            let args_id = List.map get_id args in
-            let dyn_infos =
-              { nb_rec_hyps = -100
-              ; rec_hyps = []
-              ; info =
-                  Reductionops.nf_betaiota (pf_env g) (project g)
-                    (applist
-                       ( fbody_with_full_params
-                       , List.rev_map var_of_decl princ_params
-                         @ List.rev_map mkVar args_id ))
-              ; eq_hyps = [] }
-            in
-            let fname =
-              destConst (project g)
-                (fst (decompose_app (project g) (List.hd (List.rev pte_args))))
-            in
-            tclTHENLIST
-              [ Proofview.V82.of_tactic
-                  (unfold_in_concl
-                     [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))])
-              ; (let do_prove =
-                   build_proof interactive_proof (Array.to_list fnames)
-                     (Id.Map.map prove_rec_hyp ptes_to_fix)
-                 in
-                 let prove_tac branches =
-                   let dyn_infos =
-                     { dyn_infos with
-                       rec_hyps = branches
-                     ; nb_rec_hyps = List.length branches }
-                   in
-                   clean_goal_with_heq
-                     (Id.Map.map prove_rec_hyp ptes_to_fix)
-                     do_prove dyn_infos
-                 in
-                 instantiate_hyps_with_args prove_tac
-                   (List.rev_map id_of_decl princ_info.branches)
-                   (List.rev args_id)) ]
-              g) ]
-        gl
-  in
-  tclTHEN first_tac intros_after_fixes g
+                           (*                         ); *)
+                           (* observe_tac "instancing" *)
+                           instantiate_hyps_with_args prove_tac
+                             (List.rev_map id_of_decl princ_info.branches)
+                             (List.rev args_id)) ]) ]
+            with Not_found ->
+              let nb_args = min princ_info.nargs (List.length ctxt) in
+              tclTHENLIST
+                [ tclDO nb_args intro
+                ; Proofview.Goal.enter (fun g ->
+                      let env = Proofview.Goal.env g in
+                      let sigma = Proofview.Goal.sigma g in
+                      (* replacement of the function by its body *)
+                      let args = Tacticals.New.nLastDecls g nb_args in
+                      let open Context.Named.Declaration in
+                      let args_id = List.map get_id args in
+                      let dyn_infos =
+                        { nb_rec_hyps = -100
+                        ; rec_hyps = []
+                        ; info =
+                            Reductionops.nf_betaiota env sigma
+                              (applist
+                                 ( fbody_with_full_params
+                                 , List.rev_map var_of_decl princ_params
+                                   @ List.rev_map mkVar args_id ))
+                        ; eq_hyps = [] }
+                      in
+                      let fname =
+                        destConst sigma
+                          (fst
+                             (decompose_app sigma (List.hd (List.rev pte_args))))
+                      in
+                      tclTHENLIST
+                        [ unfold_in_concl
+                            [ ( Locus.AllOccurrences
+                              , Names.EvalConstRef (fst fname) ) ]
+                        ; (let do_prove =
+                             build_proof interactive_proof
+                               (Array.to_list fnames)
+                               (Id.Map.map prove_rec_hyp ptes_to_fix)
+                           in
+                           let prove_tac branches =
+                             let dyn_infos =
+                               { dyn_infos with
+                                 rec_hyps = branches
+                               ; nb_rec_hyps = List.length branches }
+                             in
+                             clean_goal_with_heq
+                               (Id.Map.map prove_rec_hyp ptes_to_fix)
+                               do_prove dyn_infos
+                           in
+                           instantiate_hyps_with_args prove_tac
+                             (List.rev_map id_of_decl princ_info.branches)
+                             (List.rev args_id)) ]) ])
+      in
+      tclTHEN first_tac intros_after_fixes)
 
 (* Proof of principles of general functions *)
 (* let  hrec_id = Recdef.hrec_id *)
@@ -1254,97 +1291,95 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
 (* and list_rewrite = Recdef.list_rewrite *)
 (* and evaluable_of_global_reference = Recdef.evaluable_of_global_reference *)
 
-let prove_with_tcc tcc_lemma_constr eqs : tactic =
+let prove_with_tcc tcc_lemma_constr eqs : unit Proofview.tactic =
+  let open Tacticals.New in
   match !tcc_lemma_constr with
   | Undefined -> anomaly (Pp.str "No tcc proof !!")
   | Value lemma ->
-    fun gls ->
-      (*        let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
-      (*        let ids = hid::pf_ids_of_hyps gls in  *)
-      tclTHENLIST
-        [ (*            generalize [lemma]; *)
-          (*            h_intro hid; *)
-          (*            Elim.h_decompose_and (mkVar hid); *)
-          tclTRY (list_rewrite true eqs)
-        ; (*            (fun g ->  *)
-          (*               let ids' = pf_ids_of_hyps g in  *)
-          (*               let ids = List.filter (fun id -> not (List.mem id ids)) ids' in  *)
-          (*               rewrite *)
-          (*            ) *)
-          Proofview.V82.of_tactic (Eauto.gen_eauto (false, 5) [] (Some [])) ]
-        gls
-  | Not_needed -> tclIDTAC
+    (*        let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
+    (*        let ids = hid::pf_ids_of_hyps gls in  *)
+    tclTHENLIST
+      [ (*            generalize [lemma]; *)
+        (*            h_intro hid; *)
+        (*            Elim.h_decompose_and (mkVar hid); *)
+        tclTRY (list_rewrite true eqs)
+      ; (*            (fun g ->  *)
+        (*               let ids' = pf_ids_of_hyps g in  *)
+        (*               let ids = List.filter (fun id -> not (List.mem id ids)) ids' in  *)
+        (*               rewrite *)
+        (*            ) *)
+        Eauto.gen_eauto (false, 5) [] (Some []) ]
+  | Not_needed -> Proofview.tclUNIT ()
 
-let backtrack_eqs_until_hrec hrec eqs : tactic =
- fun gls ->
-  let eqs = List.map mkVar eqs in
-  let rewrite =
-    tclFIRST
-      (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs)
-  in
-  let _, hrec_concl = decompose_prod (project gls) (pf_get_hyp_typ gls hrec) in
-  let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in
-  let f = fst (destApp (project gls) f_app) in
-  let rec backtrack : tactic =
-   fun g ->
-    let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in
-    match EConstr.kind (project g) f_app with
-    | App (f', _) when eq_constr (project g) f' f -> tclIDTAC g
-    | _ -> tclTHEN rewrite backtrack g
-  in
-  backtrack gls
+let backtrack_eqs_until_hrec hrec eqs : unit Proofview.tactic =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun gls ->
+      let sigma = Proofview.Goal.sigma gls in
+      let eqs = List.map mkVar eqs in
+      let rewrite = tclFIRST (List.map Equality.rewriteRL eqs) in
+      let _, hrec_concl =
+        decompose_prod sigma (Tacmach.New.pf_get_hyp_typ hrec gls)
+      in
+      let f_app = Array.last (snd (destApp sigma hrec_concl)) in
+      let f = fst (destApp sigma f_app) in
+      let rec backtrack () : unit Proofview.tactic =
+        Proofview.Goal.enter (fun g ->
+            let sigma = Proofview.Goal.sigma gls in
+            let f_app =
+              Array.last (snd (destApp sigma (Proofview.Goal.concl g)))
+            in
+            match EConstr.kind sigma f_app with
+            | App (f', _) when eq_constr sigma f' f -> Proofview.tclUNIT ()
+            | _ -> tclTHEN rewrite (backtrack ()))
+      in
+      backtrack ())
 
 let rec rewrite_eqs_in_eqs eqs =
+  let open Tacticals.New in
   match eqs with
-  | [] -> tclIDTAC
+  | [] -> Proofview.tclUNIT ()
   | eq :: eqs ->
     tclTHEN
       (tclMAP
-         (fun id gl ->
+         (fun id ->
            observe_tac
              (Format.sprintf "rewrite %s in %s " (Id.to_string eq)
                 (Id.to_string id))
              (tclTRY
-                (Proofview.V82.of_tactic
-                   (Equality.general_rewrite_in true Locus.AllOccurrences true
-                      (* dep proofs also: *) true id (mkVar eq) false)))
-             gl)
+                (Equality.general_rewrite_in true Locus.AllOccurrences true
+                   (* dep proofs also: *) true id (mkVar eq) false)))
          eqs)
       (rewrite_eqs_in_eqs eqs)
 
-let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
- fun gls ->
-  (tclTHENLIST
-     [ backtrack_eqs_until_hrec hrec eqs
-     ; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
-       tclTHENS (* We must have exactly ONE subgoal !*)
-         (Proofview.V82.of_tactic (apply (mkVar hrec)))
-         [ tclTHENLIST
-             [ Proofview.V82.of_tactic (keep (tcc_hyps @ eqs))
-             ; Proofview.V82.of_tactic (apply (Lazy.force acc_inv))
-             ; (fun g ->
-                 if is_mes then
-                   Proofview.V82.of_tactic
-                     (unfold_in_concl
-                        [ ( Locus.AllOccurrences
-                          , evaluable_of_global_reference
-                              (delayed_force ltof_ref) ) ])
-                     g
-                 else tclIDTAC g)
-             ; observe_tac "rew_and_finish"
-                 (tclTHENLIST
-                    [ tclTRY
-                        (list_rewrite false
-                           (List.map (fun v -> (mkVar v, true)) eqs))
-                    ; observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs)
-                    ; observe_tac "finishing using"
-                        (tclCOMPLETE
-                           ( Proofview.V82.of_tactic
-                           @@ Eauto.eauto_with_bases (true, 5)
-                                [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
-                                [ Hints.Hint_db.empty TransparentState.empty
-                                    false ] )) ]) ] ] ])
-    gls
+let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : unit Proofview.tactic
+    =
+  let open Tacticals.New in
+  tclTHENLIST
+    [ backtrack_eqs_until_hrec hrec eqs
+    ; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
+      tclTHENS (* We must have exactly ONE subgoal !*)
+        (apply (mkVar hrec))
+        [ tclTHENLIST
+            [ keep (tcc_hyps @ eqs)
+            ; apply (Lazy.force acc_inv)
+            ; ( if is_mes then
+                unfold_in_concl
+                  [ ( Locus.AllOccurrences
+                    , evaluable_of_global_reference (delayed_force ltof_ref) )
+                  ]
+              else Proofview.tclUNIT () )
+            ; observe_tac "rew_and_finish"
+                (tclTHENLIST
+                   [ tclTRY
+                       (list_rewrite false
+                          (List.map (fun v -> (mkVar v, true)) eqs))
+                   ; observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs)
+                   ; 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]))
+                   ]) ] ] ]
 
 let is_valid_hypothesis sigma predicates_name =
   let predicates_name =
@@ -1367,199 +1402,204 @@ let is_valid_hypothesis sigma predicates_name =
   is_valid_hypothesis
 
 let prove_principle_for_gen (f_ref, functional_ref, eq_ref) tcc_lemma_ref is_mes
-    rec_arg_num rec_arg_type relation gl =
-  let princ_type = pf_concl gl in
-  let princ_info = compute_elim_sig (project gl) princ_type in
-  let fresh_id =
-    let avoid = ref (pf_ids_of_hyps gl) in
-    fun na ->
-      let new_id =
-        match na with
-        | Name id -> fresh_id !avoid (Id.to_string id)
-        | Anonymous -> fresh_id !avoid "H"
+    rec_arg_num rec_arg_type relation =
+  Proofview.Goal.enter (fun gl ->
+      let sigma = Proofview.Goal.sigma gl in
+      let princ_type = Proofview.Goal.concl gl in
+      let princ_info = compute_elim_sig sigma princ_type in
+      let fresh_id =
+        let avoid = ref (Tacmach.New.pf_ids_of_hyps gl) in
+        fun na ->
+          let new_id =
+            match na with
+            | Name id -> fresh_id !avoid (Id.to_string id)
+            | Anonymous -> fresh_id !avoid "H"
+          in
+          avoid := new_id :: !avoid;
+          Name new_id
       in
-      avoid := new_id :: !avoid;
-      Name new_id
-  in
-  let fresh_decl = map_name fresh_id in
-  let princ_info : elim_scheme =
-    { princ_info with
-      params = List.map fresh_decl princ_info.params
-    ; predicates = List.map fresh_decl princ_info.predicates
-    ; branches = List.map fresh_decl princ_info.branches
-    ; args = List.map fresh_decl princ_info.args }
-  in
-  let wf_tac =
-    if is_mes then 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
-  let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in
-  (*   observe ( *)
-  (*     str "princ_type := " ++ pr_lconstr  princ_type ++ fnl () ++ *)
-  (*     str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++  *)
+      let fresh_decl = map_name fresh_id in
+      let princ_info : elim_scheme =
+        { princ_info with
+          params = List.map fresh_decl princ_info.params
+        ; predicates = List.map fresh_decl princ_info.predicates
+        ; branches = List.map fresh_decl princ_info.branches
+        ; args = List.map fresh_decl princ_info.args }
+      in
+      let wf_tac =
+        if is_mes then fun b ->
+          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
+      let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in
+      (*   observe ( *)
+      (*     str "princ_type := " ++ pr_lconstr  princ_type ++ fnl () ++ *)
+      (*     str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++  *)
 
-  (*       str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++  *)
-  (*     str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++  *)
-  (*           str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
-  (*           str "npost_rec_arg := " ++ int npost_rec_arg ); *)
-  let post_rec_arg, pre_rec_arg =
-    Util.List.chop npost_rec_arg princ_info.args
-  in
-  let rec_arg_id =
-    match List.rev post_rec_arg with
-    | ( LocalAssum ({binder_name = Name id}, _)
-      | LocalDef ({binder_name = Name id}, _, _) )
-      :: _ ->
-      id
-    | _ -> assert false
-  in
-  (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs =
-    List.map
-      (get_name %> Nameops.Name.get_id %> mkVar)
-      (pre_rec_arg @ princ_info.params)
-  in
-  let relation = substl subst_constrs relation in
-  let input_type = substl subst_constrs rec_arg_type in
-  let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in
-  let acc_rec_arg_id =
-    Nameops.Name.get_id
-      (fresh_id (Name (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))))
-  in
-  let revert l =
-    tclTHEN
-      (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l)))
-      (Proofview.V82.of_tactic (clear l))
-  in
-  let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
-  let prove_rec_arg_acc g =
-    ((* observe_tac "prove_rec_arg_acc"  *)
-     tclCOMPLETE
-       (tclTHEN
-          (Proofview.V82.of_tactic
+      (*       str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++  *)
+      (*     str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++  *)
+      (*           str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
+      (*           str "npost_rec_arg := " ++ int npost_rec_arg ); *)
+      let post_rec_arg, pre_rec_arg =
+        Util.List.chop npost_rec_arg princ_info.args
+      in
+      let rec_arg_id =
+        match List.rev post_rec_arg with
+        | ( LocalAssum ({binder_name = Name id}, _)
+          | LocalDef ({binder_name = Name id}, _, _) )
+          :: _ ->
+          id
+        | _ -> assert false
+      in
+      (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
+      let subst_constrs =
+        List.map
+          (get_name %> Nameops.Name.get_id %> mkVar)
+          (pre_rec_arg @ princ_info.params)
+      in
+      let relation = substl subst_constrs relation in
+      let input_type = substl subst_constrs rec_arg_type in
+      let wf_thm_id =
+        Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R")))
+      in
+      let acc_rec_arg_id =
+        Nameops.Name.get_id
+          (fresh_id (Name (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))))
+      in
+      let open Tacticals.New in
+      let revert l =
+        tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l)
+      in
+      let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
+      let prove_rec_arg_acc =
+        (* observe_tac "prove_rec_arg_acc"  *)
+        tclCOMPLETE
+          (tclTHEN
              (assert_by (Name wf_thm_id)
                 (mkApp (delayed_force well_founded, [|input_type; relation|]))
-                (Proofview.V82.tactic (fun g ->
-                     (* observe_tac "prove wf" *)
-                     (tclCOMPLETE (wf_tac is_mes)) g))))
-          ((* observe_tac  *)
-           (*                 "apply wf_thm"  *)
-           Proofview.V82.of_tactic
-             (Tactics.Simple.apply
-                (mkApp (mkVar wf_thm_id, [|mkVar rec_arg_id|]))))))
-      g
-  in
-  let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in
-  let lemma =
-    match !tcc_lemma_ref with
-    | Undefined -> user_err Pp.(str "No tcc proof !!")
-    | Value lemma -> EConstr.of_constr lemma
-    | Not_needed ->
-      EConstr.of_constr
-        (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I")
-  in
-  (*   let rec list_diff del_list check_list = *)
-  (*     match del_list with *)
-  (*          [] -> *)
-  (*            [] *)
-  (*       | f::r -> *)
-  (*           if List.mem f check_list then *)
-  (*                list_diff r check_list *)
-  (*           else *)
-  (*                f::(list_diff r check_list) *)
-  (*   in *)
-  let tcc_list = ref [] in
-  let start_tac gls =
-    let hyps = pf_ids_of_hyps gls in
-    let hid =
-      next_ident_away_in_goal (Id.of_string "prov") (Id.Set.of_list hyps)
-    in
-    tclTHENLIST
-      [ Proofview.V82.of_tactic (generalize [lemma])
-      ; Proofview.V82.of_tactic (Simple.intro hid)
-      ; Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid))
-      ; (fun g ->
-          let new_hyps = pf_ids_of_hyps g in
-          tcc_list := List.rev (List.subtract Id.equal new_hyps (hid :: hyps));
-          if List.is_empty !tcc_list then begin
-            tcc_list := [hid];
-            tclIDTAC g
-          end
-          else thin [hid] g) ]
-      gls
-  in
-  tclTHENLIST
-    [ observe_tac "start_tac" start_tac
-    ; h_intros
-        (List.rev_map
-           (get_name %> Nameops.Name.get_id)
-           ( princ_info.args @ princ_info.branches @ princ_info.predicates
-           @ princ_info.params ))
-    ; Proofview.V82.of_tactic
-        (assert_by (Name acc_rec_arg_id)
-           (mkApp
-              (delayed_force acc_rel, [|input_type; relation; mkVar rec_arg_id|]))
-           (Proofview.V82.tactic prove_rec_arg_acc))
-    ; revert (List.rev (acc_rec_arg_id :: args_ids))
-    ; Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))
-    ; h_intros (List.rev (acc_rec_arg_id :: args_ids))
-    ; Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref))
-    ; (fun gl' ->
-        let body =
-          let _, args = destApp (project gl') (pf_concl gl') in
-          Array.last args
-        in
-        let body_info rec_hyps =
-          { nb_rec_hyps = List.length rec_hyps
-          ; rec_hyps
-          ; eq_hyps = []
-          ; info = body }
-        in
-        let acc_inv =
-          lazy
+                (* observe_tac "prove wf" *)
+                (tclCOMPLETE (wf_tac is_mes)))
+             ((* observe_tac  *)
+              (*                 "apply wf_thm"  *)
+              Tactics.Simple.apply
+                (mkApp (mkVar wf_thm_id, [|mkVar rec_arg_id|]))))
+      in
+      let args_ids =
+        List.map (get_name %> Nameops.Name.get_id) princ_info.args
+      in
+      let lemma =
+        match !tcc_lemma_ref with
+        | Undefined -> user_err Pp.(str "No tcc proof !!")
+        | Value lemma -> EConstr.of_constr lemma
+        | Not_needed ->
+          EConstr.of_constr
+            ( UnivGen.constr_of_monomorphic_global
+            @@ Coqlib.lib_ref "core.True.I" )
+      in
+      (*   let rec list_diff del_list check_list = *)
+      (*     match del_list with *)
+      (*          [] -> *)
+      (*            [] *)
+      (*       | f::r -> *)
+      (*           if List.mem f check_list then *)
+      (*                list_diff r check_list *)
+      (*           else *)
+      (*                f::(list_diff r check_list) *)
+      (*   in *)
+      let tcc_list = ref [] in
+      let start_tac =
+        Proofview.Goal.enter (fun gls ->
+            let hyps = Tacmach.New.pf_ids_of_hyps gls in
+            let hid =
+              next_ident_away_in_goal (Id.of_string "prov")
+                (Id.Set.of_list hyps)
+            in
+            tclTHENLIST
+              [ generalize [lemma]
+              ; Simple.intro hid
+              ; Elim.h_decompose_and (mkVar hid)
+              ; Proofview.Goal.enter (fun g ->
+                    let new_hyps = Tacmach.New.pf_ids_of_hyps g in
+                    tcc_list :=
+                      List.rev (List.subtract Id.equal new_hyps (hid :: hyps));
+                    if List.is_empty !tcc_list then begin
+                      tcc_list := [hid];
+                      Proofview.tclUNIT ()
+                    end
+                    else clear [hid]) ])
+      in
+      tclTHENLIST
+        [ observe_tac "start_tac" start_tac
+        ; h_intros
+            (List.rev_map
+               (get_name %> Nameops.Name.get_id)
+               ( princ_info.args @ princ_info.branches @ princ_info.predicates
+               @ princ_info.params ))
+        ; assert_by (Name acc_rec_arg_id)
             (mkApp
-               ( delayed_force acc_inv_id
+               ( delayed_force acc_rel
                , [|input_type; relation; mkVar rec_arg_id|] ))
-        in
-        let acc_inv =
-          lazy (mkApp (Lazy.force acc_inv, [|mkVar acc_rec_arg_id|]))
-        in
-        let predicates_names =
-          List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
-        in
-        let pte_info =
-          { proving_tac =
-              (fun eqs ->
-                (*                msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id  !tcc_list); *)
-                (*                msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
-                (*                msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
-                (*                msgnl (str "acc_rec_arg_id := "++  Ppconstr.pr_id acc_rec_arg_id); *)
-                (*                msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id  eqs); *)
+            prove_rec_arg_acc
+        ; revert (List.rev (acc_rec_arg_id :: args_ids))
+        ; fix fix_id (List.length args_ids + 1)
+        ; h_intros (List.rev (acc_rec_arg_id :: args_ids))
+        ; Equality.rewriteLR (mkConst eq_ref)
+        ; Proofview.Goal.enter (fun gl' ->
+              let body =
+                let _, args =
+                  destApp (Proofview.Goal.sigma gl') (Proofview.Goal.concl gl')
+                in
+                Array.last args
+              in
+              let body_info rec_hyps =
+                { nb_rec_hyps = List.length rec_hyps
+                ; rec_hyps
+                ; eq_hyps = []
+                ; info = body }
+              in
+              let acc_inv =
+                lazy
+                  (mkApp
+                     ( delayed_force acc_inv_id
+                     , [|input_type; relation; mkVar rec_arg_id|] ))
+              in
+              let acc_inv =
+                lazy (mkApp (Lazy.force acc_inv, [|mkVar acc_rec_arg_id|]))
+              in
+              let predicates_names =
+                List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
+              in
+              let pte_info =
+                { proving_tac =
+                    (fun eqs ->
+                      (*                msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id  !tcc_list); *)
+                      (*                msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
+                      (*                msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
+                      (*                msgnl (str "acc_rec_arg_id := "++  Ppconstr.pr_id acc_rec_arg_id); *)
+                      (*                msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id  eqs); *)
 
-                (* observe_tac "new_prove_with_tcc"  *)
-                new_prove_with_tcc is_mes acc_inv fix_id
-                  ( !tcc_list
-                  @ List.map
-                      (get_name %> Nameops.Name.get_id)
-                      (princ_info.args @ princ_info.params)
-                  @ [acc_rec_arg_id] )
-                  eqs)
-          ; is_valid = is_valid_hypothesis (project gl') predicates_names }
-        in
-        let ptes_info : pte_info Id.Map.t =
-          List.fold_left
-            (fun map pte_id -> Id.Map.add pte_id pte_info map)
-            Id.Map.empty predicates_names
-        in
-        let make_proof rec_hyps =
-          build_proof false [f_ref] ptes_info (body_info rec_hyps)
-        in
-        (* observe_tac "instantiate_hyps_with_args"  *)
-        (instantiate_hyps_with_args make_proof
-           (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
-           (List.rev args_ids))
-          gl') ]
-    gl
+                      (* observe_tac "new_prove_with_tcc"  *)
+                      new_prove_with_tcc is_mes acc_inv fix_id
+                        ( !tcc_list
+                        @ List.map
+                            (get_name %> Nameops.Name.get_id)
+                            (princ_info.args @ princ_info.params)
+                        @ [acc_rec_arg_id] )
+                        eqs)
+                ; is_valid =
+                    is_valid_hypothesis (Proofview.Goal.sigma gl')
+                      predicates_names }
+              in
+              let ptes_info : pte_info Id.Map.t =
+                List.fold_left
+                  (fun map pte_id -> Id.Map.add pte_id pte_info map)
+                  Id.Map.empty predicates_names
+              in
+              let make_proof rec_hyps =
+                build_proof false [f_ref] ptes_info (body_info rec_hyps)
+              in
+              (* observe_tac "instantiate_hyps_with_args"  *)
+              instantiate_hyps_with_args make_proof
+                (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
+                (List.rev args_ids)) ])
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 52089ca7fb..096ea5fed5 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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 Names
 
 val prove_princ_for_struct :
@@ -7,7 +17,7 @@ val prove_princ_for_struct :
   -> Constant.t array
   -> EConstr.constr array
   -> int
-  -> Tacmach.tactic
+  -> unit Proofview.tactic
 
 val prove_principle_for_gen :
      Constant.t * Constant.t * Constant.t
@@ -22,6 +32,6 @@ val prove_principle_for_gen :
   -> (* the type of the recursive argument *)
      EConstr.constr
   -> (* the wf relation used to prove the function *)
-     Tacmach.tactic
+     unit Proofview.tactic
 
 (* val is_pte  : rel_declaration -> bool  *)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 45b1713441..1ea803f561 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -13,7 +13,8 @@ open Names
 open Indfun_common
 module RelDecl = Context.Rel.Declaration
 
-let observe_tac s = observe_tac (fun _ _ -> Pp.str s)
+let observe_tac s =
+  New.observe_tac ~header:(Pp.str "observation") (fun _ _ -> Pp.str s)
 
 (*
    Construct a fixpoint as a Glob_term
@@ -210,9 +211,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
       (EConstr.of_constr new_principle_type)
   in
   let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
-  let ftac =
-    Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)
-  in
+  let ftac = proof_tac (Array.map map funs) mutr_nparams in
   let env = Global.env () in
   let uctx = Evd.evar_universe_context sigma in
   let typ = EConstr.of_constr new_principle_type in
@@ -335,7 +334,7 @@ let generate_principle (evd : Evd.evar_map ref) pconstants on_error is_general
       -> Names.Constant.t array
       -> EConstr.constr array
       -> int
-      -> Tacmach.tactic) : unit =
+      -> unit Proofview.tactic) : unit =
   let names =
     List.map (function {Vernacexpr.fname = {CAst.v = name}} -> name) fix_rec_l
   in
@@ -442,7 +441,7 @@ let register_struct is_rec fixpoint_exprl =
 let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref
     eq_ref rec_arg_num rec_arg_type relation (_ : int)
     (_ : Names.Constant.t array) (_ : EConstr.constr array) (_ : int) :
-    Tacmach.tactic =
+    unit Proofview.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
@@ -593,250 +592,241 @@ let rec generate_fresh_id x avoid i =
     id :: generate_fresh_id x (id :: avoid) (pred i)
 
 let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i :
-    Tacmach.tactic =
+    unit Proofview.tactic =
   let open Constr in
   let open EConstr in
   let open Context.Rel.Declaration in
-  let open Tacmach in
+  let open Tacmach.New 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))
-          []
+  let open Tacticals.New in
+  Proofview.Goal.enter (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 (Proofview.Goal.sigma g) (Proofview.Goal.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
-      (* and get the real args of the branch by unfolding the defined constant *)
-      (*
+      (* 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_branch i pat =
+        (* 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."))
+            pat []
+        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_get_hyp_typ g hid in
-            let sigma = project g in
-            match EConstr.kind sigma type_of_hid with
-            | Prod (_, _, t') -> (
-              match EConstr.kind sigma t' with
-              | Prod (_, t'', t''') -> (
-                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
+        let constructor_args g =
+          List.fold_right
+            (fun hid acc ->
+              let type_of_hid = pf_get_hyp_typ hid g in
+              let sigma = Proofview.Goal.sigma g in
+              match EConstr.kind sigma type_of_hid with
+              | Prod (_, _, t') -> (
+                match EConstr.kind sigma t' with
+                | Prod (_, t'', t''') -> (
+                  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 )
                 | _ -> mkVar hid :: acc )
-              | _ -> mkVar hid :: acc )
-            | _ -> 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)
+              | _ -> mkVar hid :: acc)
+            pre_args []
         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 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
-        if constructor_num <= length then ((kn, !ind_number), constructor_num)
-        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)
+        (* 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 ((kn, !ind_number), constructor_num)
+          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 "
+              (match pat with [] -> tclIDTAC | _ -> intro_patterns false pat)
+          ; (* unfolding of all the defined variables introduced by this branch *)
+            (* observe_tac "unfolding" pre_tac; *)
+            (* $zeta$ normalizing of the conclusion *)
+            reduce
+              (Genredexpr.Cbv
+                 { Redops.all_flags with
+                   Genredexpr.rDelta = false
+                 ; Genredexpr.rConst = [] })
+              Locusops.onConcl
+          ; observe_tac "toto " (Proofview.tclUNIT ())
+          ; (* introducing the result of the graph and the equality hypothesis *)
+            observe_tac "introducing" (tclMAP Simple.intro [res; hres])
+          ; (* replacing [res] with its value *)
+            observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres))
+          ; (* Conclusion *)
+            observe_tac "exact"
+              (Proofview.Goal.enter (fun g -> exact_check (app_constructor 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
+      (* 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
-      (* 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)
+      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
-      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))
+      (* 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 (Proofview.Goal.env g)
+                        (Proofview.Goal.sigma g) p
+                      :: bindings
+                    , id :: avoid ))
+                  ([], avoid) princ_infos.predicates lemmas))
+        in
+        params_bindings @ lemmas_bindings
       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
+      tclTHENLIST
+        [ observe_tac "principle"
+            (assert_by (Name principle_id) princ_type (exact_check f_principle))
+        ; observe_tac "intro args_names" (tclMAP Simple.intro 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
+        ; tclTHENS
+            (observe_tac "functional_induction"
+               (Proofview.Goal.enter (fun gl ->
+                    let term =
+                      mkApp (mkVar principle_id, Array.of_list bindings)
+                    in
+                    tclTYPEOFTHEN ~refresh:true term (fun _ _ -> apply term))))
+            (List.map_i
+               (fun i pat ->
+                 observe_tac
+                   ("proving branch " ^ string_of_int i)
+                   (prove_branch i pat))
+               1 intro_pats) ])
 
 (* [prove_fun_complete funs graphs schemes lemmas_types_infos i]
    is the tactic used to prove completeness lemma.
@@ -865,7 +855,7 @@ let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i :
 
 *)
 
-let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
+let thin = Tactics.clear
 
 (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis
        (unfolding, substituting, destructing cases \ldots)
@@ -882,347 +872,343 @@ let tauto =
 (* [generalize_dependent_of x hyp g]
    generalize every hypothesis which depends of [x] but [hyp]
 *)
-let generalize_dependent_of x hyp g =
+let generalize_dependent_of x hyp =
   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 Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      tclMAP
+        (function
+          | LocalAssum ({Context.binder_name = id}, t)
+            when (not (Id.equal id hyp))
+                 && Termops.occur_var (Proofview.Goal.env g)
+                      (Proofview.Goal.sigma g) x t ->
+            tclTHEN (Tactics.generalize [EConstr.mkVar id]) (thin [id])
+          | _ -> Proofview.tclUNIT ())
+        (Proofview.Goal.hyps g))
+
+let rec intros_with_rewrite () =
+  observe_tac "intros_with_rewrite" (intros_with_rewrite_aux ())
+
+and intros_with_rewrite_aux () : unit Proofview.tactic =
   let open Constr in
   let open EConstr in
-  let open Tacmach in
+  let open Tacmach.New 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') -> (
-      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
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let eq_ind = make_eq () in
+      let sigma = Proofview.Goal.sigma g in
+      match EConstr.kind sigma (Proofview.Goal.concl g) with
+      | Prod (_, t, t') -> (
+        match EConstr.kind sigma t with
+        | App (eq, args) when EConstr.eq_constr sigma eq eq_ind ->
+          if
+            Reductionops.is_conv (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+              args.(1) args.(2)
+          then
+            let id = pf_get_new_id (Id.of_string "y") g in
+            tclTHENLIST [Simple.intro id; thin [id]; intros_with_rewrite ()]
+          else if
+            isVar sigma args.(1)
+            && Environ.evaluable_named
+                 (destVar sigma args.(1))
+                 (Proofview.Goal.env g)
+          then
+            tclTHENLIST
+              [ unfold_in_concl
+                  [ ( Locus.AllOccurrences
+                    , Names.EvalVarRef (destVar sigma args.(1)) ) ]
+              ; tclMAP
+                  (fun id ->
+                    tclTRY
+                      (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 () ]
+          else if
+            isVar sigma args.(2)
+            && Environ.evaluable_named
+                 (destVar sigma args.(2))
+                 (Proofview.Goal.env g)
+          then
+            tclTHENLIST
+              [ unfold_in_concl
+                  [ ( Locus.AllOccurrences
+                    , Names.EvalVarRef (destVar sigma args.(2)) ) ]
+              ; tclMAP
+                  (fun id ->
+                    tclTRY
+                      (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 () ]
+          else if isVar sigma args.(1) then
+            let id = pf_get_new_id (Id.of_string "y") g in
+            tclTHENLIST
+              [ Simple.intro id
+              ; generalize_dependent_of (destVar sigma args.(1)) id
+              ; tclTRY (Equality.rewriteLR (mkVar id))
+              ; intros_with_rewrite () ]
+          else if isVar sigma args.(2) then
+            let id = pf_get_new_id (Id.of_string "y") g in
+            tclTHENLIST
+              [ Simple.intro id
+              ; generalize_dependent_of (destVar sigma args.(2)) id
+              ; tclTRY (Equality.rewriteRL (mkVar id))
+              ; intros_with_rewrite () ]
+          else
+            let id = pf_get_new_id (Id.of_string "y") g in
+            tclTHENLIST
+              [ Simple.intro id
+              ; tclTRY (Equality.rewriteLR (mkVar id))
+              ; intros_with_rewrite () ]
+        | Ind _
+          when EConstr.eq_constr sigma t
+                 (EConstr.of_constr
+                    ( UnivGen.constr_of_monomorphic_global
+                    @@ Coqlib.lib_ref "core.False.type" )) ->
+          tauto
+        | Case (_, _, _, v, _) ->
+          tclTHENLIST [simplest_case v; intros_with_rewrite ()]
+        | LetIn _ ->
           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
+            [ reduce
+                (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false})
+                Locusops.onConcl
+            ; intros_with_rewrite () ]
+        | _ ->
           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
-      | 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
+          tclTHENLIST [Simple.intro id; intros_with_rewrite ()] )
       | 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 )
-    | 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 =
+          [ reduce
+              (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false})
+              Locusops.onConcl
+          ; intros_with_rewrite () ]
+      | _ -> Proofview.tclUNIT ())
+
+let rec reflexivity_with_destruct_cases () =
   let open Constr in
   let open EConstr in
-  let open Tacmach in
+  let open Tacmach.New 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_get_hyp_typ g 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 open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let destruct_case () =
+        try
+          match
+            EConstr.kind (Proofview.Goal.sigma g)
+              (snd (destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g))).(
+              2)
+          with
+          | Case (_, _, _, v, _) ->
+            tclTHENLIST
+              [ simplest_case v
+              ; intros
+              ; observe_tac "reflexivity_with_destruct_cases"
+                  (reflexivity_with_destruct_cases ()) ]
+          | _ -> reflexivity
+        with e when CErrors.noncritical e -> 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 =
+        onAllHypsAndConcl (fun sc ->
+            match sc with
+            | None -> Proofview.tclUNIT ()
+            | Some id ->
+              Proofview.Goal.enter (fun g ->
+                  match
+                    EConstr.kind (Proofview.Goal.sigma g) (pf_get_hyp_typ id g)
+                  with
+                  | App (eq, [|_; t1; t2|])
+                    when EConstr.eq_constr (Proofview.Goal.sigma g) eq eq_ind ->
+                    if
+                      Equality.discriminable (Proofview.Goal.env g)
+                        (Proofview.Goal.sigma g) t1 t2
+                    then Equality.discrHyp id
+                    else if
+                      Equality.injectable (Proofview.Goal.env g)
+                        (Proofview.Goal.sigma g) ~keep_proofs:None t1 t2
+                    then
+                      tclTHENLIST
+                        [ Equality.injHyp my_inj_flags None id
+                        ; thin [id]
+                        ; intros_with_rewrite () ]
+                    else Proofview.tclUNIT ()
+                  | _ -> Proofview.tclUNIT ()))
+      in
+      tclFIRST
+        [ observe_tac "reflexivity_with_destruct_cases : reflexivity" 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 ())) ])
 
 let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
-    Tacmach.tactic =
+    unit Proofview.tactic =
   let open EConstr in
-  let open Tacmach in
+  let open Tacmach.New 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 g, princ_type = tac_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 =
-        match find_Function_infos (fst (destConst (project g) funcs.(j))) with
-        | None -> CErrors.user_err Pp.(str "No graph found")
-        | Some infos -> infos
+  let open Tacticals.New in
+  Proofview.Goal.enter (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 (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+              (EConstr.it_mkLambda_or_LetIn concl ctxt))
+          lemmas_types_infos
       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
+      (* We get the constant and the principle corresponding to this lemma *)
+      let f = funcs.(i) in
+      let graph_principle =
+        Reductionops.nf_zeta (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+          (EConstr.of_constr schemes.(i))
       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
+      tclTYPEOFTHEN graph_principle (fun sigma princ_type ->
+          let princ_infos = Tactics.compute_elim_sig sigma 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 sigma (Proofview.Goal.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 (Proofview.Goal.sigma 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 : unit Proofview.tactic =
+            let graph_def = graphs.(j) in
+            let infos =
+              match
+                find_Function_infos
+                  (fst (destConst (Proofview.Goal.sigma g) funcs.(j)))
+              with
+              | None -> CErrors.user_err Pp.(str "No graph found")
+              | Some infos -> infos
+            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 Simple.intro ids
+                ; Equality.rewriteLR (mkConst eq_lemma)
+                ; (* Don't forget to $\zeta$ normlize the term since the principles
+                     have been $\zeta$-normalized *)
+                  reduce
+                    (Genredexpr.Cbv
+                       {Redops.all_flags with Genredexpr.rDelta = false})
+                    Locusops.onConcl
+                ; generalize (List.map mkVar ids)
+                ; thin ids ]
+            else
+              unfold_in_concl
+                [ ( Locus.AllOccurrences
+                  , Names.EvalConstRef
+                      (fst (destConst (Proofview.Goal.sigma g) f)) ) ]
+          in
+          (* The proof of each branche itself *)
+          let ind_number = ref 0 in
+          let min_constr_number = ref 0 in
+          let prove_branch i this_branche_ids =
+            (* 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
+            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 ())
+              ]
+          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 Simple.intro (args_names @ [res; hres])
+            ; observe_tac "h_generalize"
+                (generalize
+                   [ mkApp
+                       ( applist (graph_principle, params)
+                       , Array.map (fun c -> applist (c, params)) lemmas ) ])
+            ; Simple.intro graph_principle_id
+            ; observe_tac ""
+                (tclTHENS
+                   (observe_tac "elim"
+                      (elim false None
+                         (mkVar hres, Tactypes.NoBindings)
+                         (Some (mkVar graph_principle_id, Tactypes.NoBindings))))
+                   (List.map_i
+                      (fun i pat ->
+                        observe_tac "prove_branch" (prove_branch i pat))
+                      1 intro_pats)) ]))
 
 exception No_graph_found
 
@@ -1523,9 +1509,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let info = Declare.Info.make () in
           let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in
           let lemma = Declare.Proof.start ~cinfo ~info !evd in
-          let lemma =
-            fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
-          in
+          let lemma = fst @@ Declare.Proof.by (proving_tac i) lemma in
           let (_ : _ list) =
             Declare.Proof.save_regular ~proof:lemma
               ~opaque:Vernacexpr.Transparent ~idopt:None
@@ -1592,10 +1576,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lemma =
             fst
               (Declare.Proof.by
-                 (Proofview.V82.tactic
-                    (observe_tac
-                       ("prove completeness (" ^ Id.to_string f_id ^ ")")
-                       (proving_tac i)))
+                 (observe_tac
+                    ("prove completeness (" ^ Id.to_string f_id ^ ")")
+                    (proving_tac i))
                  lemma)
           in
           let (_ : _ list) =
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index af53f16e1f..0179215d6a 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -394,10 +394,7 @@ let jmeq_refl () =
     @@ Coqlib.lib_ref "core.JMeq.refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
-let h_intros l =
-  Proofview.V82.of_tactic
-    (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l)
-
+let h_intros l = Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
 
@@ -428,13 +425,12 @@ let evaluable_of_global_reference r =
   | _ -> assert false
 
 let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
-  let open Tacticals in
+  let open Tacticals.New in
   (tclREPEAT
      (List.fold_right
         (fun (eq, b) i ->
           tclORELSE
-            (Proofview.V82.of_tactic
-               ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
+            ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)
             i)
         (if rev then List.rev eqs else eqs)
         (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"])
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 396db55458..7b7044fdaf 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -90,7 +90,7 @@ exception Defining_principle of exn
 exception ToShow of exn
 
 val is_strict_tcc : unit -> bool
-val h_intros : Names.Id.t list -> Tacmach.tactic
+val h_intros : Names.Id.t list -> unit Proofview.tactic
 val h_id : Names.Id.t
 val hrec_id : Names.Id.t
 val acc_inv_id : EConstr.constr Util.delayed
@@ -102,7 +102,7 @@ val well_founded : EConstr.constr Util.delayed
 val evaluable_of_global_reference :
   GlobRef.t -> Names.evaluable_global_reference
 
-val list_rewrite : bool -> (EConstr.constr * bool) list -> Tacmach.tactic
+val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic
 
 val decompose_lam_n :
      Evd.evar_map
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 066ade07d2..33076a876b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -23,8 +23,7 @@ open Nameops
 open CErrors
 open Util
 open UnivGen
-open Tacticals
-open Tacmach
+open Tacticals.New
 open Tactics
 open Nametab
 open Tacred
@@ -94,7 +93,7 @@ let const_of_ref = function
 
 (* Generic values *)
 let pf_get_new_ids idl g =
-  let ids = pf_ids_of_hyps g in
+  let ids = Tacmach.New.pf_ids_of_hyps g in
   let ids = Id.Set.of_list ids in
   List.fold_right
     (fun id acc ->
@@ -105,8 +104,9 @@ let next_ident_away_in_goal ids avoid =
   next_ident_away_in_goal ids (Id.Set.of_list avoid)
 
 let compute_renamed_type gls id =
-  rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty
-    (*no rels*) [] (pf_get_hyp_typ gls id)
+  rename_bound_vars_as_displayed (Proofview.Goal.sigma gls)
+    (*no avoid*) Id.Set.empty (*no rels*) []
+    (Tacmach.New.pf_get_hyp_typ id gls)
 
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
@@ -218,20 +218,6 @@ let (declare_f :
  fun f_id kind input_type fterm_ref ->
   declare_fun f_id kind (value_f input_type fterm_ref)
 
-let observe_tclTHENLIST s tacl =
-  if do_observe () 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
   open Tacticals.New
 
@@ -364,11 +350,11 @@ type ('a, 'b) journey_info_tac =
   -> (* the arguments of the constructor *)
      'b infos
   -> (* infos of the caller *)
-     ('b infos -> tactic)
+     ('b infos -> unit Proofview.tactic)
   -> (* the continuation tactic of the caller *)
      'b infos
   -> (* argument of the tactic *)
-     tactic
+     unit Proofview.tactic
 
 (* journey_info : specifies the actions to do on the different term constructors during the traveling of the term
 *)
@@ -376,7 +362,9 @@ type journey_info =
   { letiN : (Name.t * constr * types * constr, constr) journey_info_tac
   ; lambdA : (Name.t * types * constr, constr) journey_info_tac
   ; casE :
-         ((constr infos -> tactic) -> constr infos -> tactic)
+         (   (constr infos -> unit Proofview.tactic)
+          -> constr infos
+          -> unit Proofview.tactic)
       -> ( case_info
            * constr
            * (constr, EInstance.t) case_invert
@@ -397,133 +385,131 @@ let add_vars sigma forbidden e =
   in
   aux forbidden e
 
-let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
- fun g ->
-  let rev_context, b = decompose_lam_n (project g) nb_lam e in
-  let ids =
-    List.fold_left
-      (fun acc (na, _) ->
-        let pre_id =
-          match na.binder_name with Name x -> x | Anonymous -> ano_id
-        in
-        pre_id :: acc)
-      [] rev_context
-  in
-  let rev_ids = pf_get_new_ids (List.rev ids) g in
-  let new_b = substl (List.map mkVar rev_ids) b in
-  observe_tclTHENLIST
-    (fun _ _ -> str "treat_case1")
-    [ h_intros (List.rev rev_ids)
-    ; Proofview.V82.of_tactic
-        (intro_using_then teq_id (fun _ -> Proofview.tclUNIT ()))
-    ; onLastHypId (fun heq ->
-          observe_tclTHENLIST
-            (fun _ _ -> str "treat_case2")
-            [ Proofview.V82.of_tactic (clear to_intros)
-            ; h_intros to_intros
-            ; (fun g' ->
-                let ty_teq = pf_get_hyp_typ g' heq in
-                let teq_lhs, teq_rhs =
-                  let _, args =
-                    try destApp (project g') ty_teq
-                    with DestKO -> assert false
-                  in
-                  (args.(1), args.(2))
-                in
-                let new_b' =
-                  Termops.replace_term (project g') teq_lhs teq_rhs new_b
-                in
-                let new_infos =
-                  { infos with
-                    info = new_b'
-                  ; eqs = heq :: infos.eqs
-                  ; forbidden_ids =
-                      ( if forbid_new_ids then
-                        add_vars (project g') infos.forbidden_ids new_b'
-                      else infos.forbidden_ids ) }
-                in
-                finalize_tac new_infos g') ]) ]
-    g
-
-let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
-  let sigma = project g in
-  let env = pf_env g in
-  match EConstr.kind sigma expr_info.info with
-  | CoFix _ | Fix _ ->
-    user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
-  | Array _ -> user_err Pp.(str "Function cannot treat arrays")
-  | Proj _ -> user_err Pp.(str "Function cannot treat projections")
-  | LetIn (na, b, t, e) ->
-    let new_continuation_tac =
-      jinfo.letiN (na.binder_name, b, t, e) expr_info continuation_tac
-    in
-    travel jinfo new_continuation_tac
-      {expr_info with info = b; is_final = false}
-      g
-  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
-  | Prod _ -> (
-    try
-      check_not_nested env sigma
-        (expr_info.f_id :: expr_info.forbidden_ids)
-        expr_info.info;
-      jinfo.otherS () expr_info continuation_tac expr_info g
-    with e when CErrors.noncritical e ->
-      user_err ~hdr:"Recdef.travel"
-        ( str "the term "
-        ++ Printer.pr_leconstr_env env sigma expr_info.info
-        ++ str " can not contain a recursive call to "
-        ++ Id.print expr_info.f_id ) )
-  | Lambda (n, t, b) -> (
-    try
-      check_not_nested env sigma
-        (expr_info.f_id :: expr_info.forbidden_ids)
-        expr_info.info;
-      jinfo.otherS () expr_info continuation_tac expr_info g
-    with e when CErrors.noncritical e ->
-      user_err ~hdr:"Recdef.travel"
-        ( str "the term "
-        ++ Printer.pr_leconstr_env env sigma expr_info.info
-        ++ str " can not contain a recursive call to "
-        ++ Id.print expr_info.f_id ) )
-  | Case (ci, t, iv, a, l) ->
-    let continuation_tac_a =
-      jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
-    in
-    travel jinfo continuation_tac_a
-      {expr_info with info = a; is_main_branch = false; is_final = false}
-      g
-  | App _ -> (
-    let f, args = decompose_app sigma expr_info.info in
-    if EConstr.eq_constr sigma f expr_info.f_constr then
-      jinfo.app_reC (f, args) expr_info continuation_tac expr_info g
-    else
-      match EConstr.kind sigma f with
-      | App _ -> assert false (* f is coming from a decompose_app *)
-      | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
-       |Prod _ | Var _ ->
-        let new_infos = {expr_info with info = (f, args)} in
+let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos :
+    unit Proofview.tactic =
+  Proofview.Goal.enter (fun g ->
+      let rev_context, b = decompose_lam_n (Proofview.Goal.sigma g) nb_lam e in
+      let ids =
+        List.fold_left
+          (fun acc (na, _) ->
+            let pre_id =
+              match na.binder_name with Name x -> x | Anonymous -> ano_id
+            in
+            pre_id :: acc)
+          [] rev_context
+      in
+      let rev_ids = pf_get_new_ids (List.rev ids) g in
+      let new_b = substl (List.map mkVar rev_ids) b in
+      New.observe_tclTHENLIST
+        (fun _ _ -> str "treat_case1")
+        [ h_intros (List.rev rev_ids)
+        ; intro_using_then teq_id (fun _ -> Proofview.tclUNIT ())
+        ; Tacticals.New.onLastHypId (fun heq ->
+              New.observe_tclTHENLIST
+                (fun _ _ -> str "treat_case2")
+                [ clear to_intros
+                ; h_intros to_intros
+                ; Proofview.Goal.enter (fun g' ->
+                      let sigma = Proofview.Goal.sigma g' in
+                      let ty_teq = Tacmach.New.pf_get_hyp_typ heq g' in
+                      let teq_lhs, teq_rhs =
+                        let _, args =
+                          try destApp sigma ty_teq with DestKO -> assert false
+                        in
+                        (args.(1), args.(2))
+                      in
+                      let new_b' =
+                        Termops.replace_term sigma teq_lhs teq_rhs new_b
+                      in
+                      let new_infos =
+                        { infos with
+                          info = new_b'
+                        ; eqs = heq :: infos.eqs
+                        ; forbidden_ids =
+                            ( if forbid_new_ids then
+                              add_vars sigma infos.forbidden_ids new_b'
+                            else infos.forbidden_ids ) }
+                      in
+                      finalize_tac new_infos) ]) ])
+
+let rec travel_aux jinfo continuation_tac (expr_info : constr infos) =
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      let env = Proofview.Goal.env g in
+      match EConstr.kind sigma expr_info.info with
+      | CoFix _ | Fix _ ->
+        user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
+      | Array _ -> user_err Pp.(str "Function cannot treat arrays")
+      | Proj _ -> user_err Pp.(str "Function cannot treat projections")
+      | LetIn (na, b, t, e) ->
         let new_continuation_tac =
-          jinfo.apP (f, args) expr_info continuation_tac
+          jinfo.letiN (na.binder_name, b, t, e) expr_info continuation_tac
+        in
+        travel jinfo new_continuation_tac
+          {expr_info with info = b; is_final = false}
+      | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
+      | Prod _ -> (
+        try
+          check_not_nested env sigma
+            (expr_info.f_id :: expr_info.forbidden_ids)
+            expr_info.info;
+          jinfo.otherS () expr_info continuation_tac expr_info
+        with e when CErrors.noncritical e ->
+          user_err ~hdr:"Recdef.travel"
+            ( str "the term "
+            ++ Printer.pr_leconstr_env env sigma expr_info.info
+            ++ str " can not contain a recursive call to "
+            ++ Id.print expr_info.f_id ) )
+      | Lambda (n, t, b) -> (
+        try
+          check_not_nested env sigma
+            (expr_info.f_id :: expr_info.forbidden_ids)
+            expr_info.info;
+          jinfo.otherS () expr_info continuation_tac expr_info
+        with e when CErrors.noncritical e ->
+          user_err ~hdr:"Recdef.travel"
+            ( str "the term "
+            ++ Printer.pr_leconstr_env env sigma expr_info.info
+            ++ str " can not contain a recursive call to "
+            ++ Id.print expr_info.f_id ) )
+      | Case (ci, t, iv, a, l) ->
+        let continuation_tac_a =
+          jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
         in
-        travel_args jinfo expr_info.is_main_branch new_continuation_tac
-          new_infos g
-      | Case _ ->
-        user_err ~hdr:"Recdef.travel"
-          ( str "the term "
-          ++ Printer.pr_leconstr_env env sigma expr_info.info
-          ++ str
-               " can not contain an applied match (See Limitation in Section \
-                2.3 of refman)" )
-      | _ ->
-        anomaly
-          ( Pp.str "travel_aux : unexpected "
-          ++ Printer.pr_leconstr_env env sigma expr_info.info
-          ++ Pp.str "." ) )
-  | Cast (t, _, _) -> travel jinfo continuation_tac {expr_info with info = t} g
-  | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _
-   |Float _ ->
-    let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in
-    new_continuation_tac expr_info g
+        travel jinfo continuation_tac_a
+          {expr_info with info = a; is_main_branch = false; is_final = false}
+      | App _ -> (
+        let f, args = decompose_app sigma expr_info.info in
+        if EConstr.eq_constr sigma f expr_info.f_constr then
+          jinfo.app_reC (f, args) expr_info continuation_tac expr_info
+        else
+          match EConstr.kind sigma f with
+          | App _ -> assert false (* f is coming from a decompose_app *)
+          | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _
+           |Prod _ | Var _ ->
+            let new_infos = {expr_info with info = (f, args)} in
+            let new_continuation_tac =
+              jinfo.apP (f, args) expr_info continuation_tac
+            in
+            travel_args jinfo expr_info.is_main_branch new_continuation_tac
+              new_infos
+          | Case _ ->
+            user_err ~hdr:"Recdef.travel"
+              ( str "the term "
+              ++ Printer.pr_leconstr_env env sigma expr_info.info
+              ++ str
+                   " can not contain an applied match (See Limitation in \
+                    Section 2.3 of refman)" )
+          | _ ->
+            anomaly
+              ( Pp.str "travel_aux : unexpected "
+              ++ Printer.pr_leconstr_env env sigma expr_info.info
+              ++ Pp.str "." ) )
+      | Cast (t, _, _) -> travel jinfo continuation_tac {expr_info with info = t}
+      | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _
+       |Int _ | Float _ ->
+        let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in
+        new_continuation_tac expr_info)
 
 and travel_args jinfo is_final continuation_tac infos =
   let f_args', args = infos.info in
@@ -538,139 +524,131 @@ and travel_args jinfo is_final continuation_tac infos =
     travel jinfo new_continuation_tac {infos with info = arg; is_final = false}
 
 and travel jinfo continuation_tac expr_info =
-  observe_tac
+  New.observe_tac
     (fun env sigma ->
       str jinfo.message ++ Printer.pr_leconstr_env env sigma expr_info.info)
     (travel_aux jinfo continuation_tac expr_info)
 
 (* Termination proof *)
 
-let rec prove_lt hyple g =
-  let sigma = project g in
-  begin
-    try
-      let varx, varz =
-        match decompose_app sigma (pf_concl g) with
-        | _, x :: z :: _ when isVar sigma x && isVar sigma z -> (x, z)
-        | _ -> assert false
-      in
-      let h =
-        List.find
-          (fun id ->
-            match decompose_app sigma (pf_get_hyp_typ g id) with
-            | _, t :: _ -> EConstr.eq_constr sigma t varx
-            | _ -> false)
-          hyple
-      in
-      let y =
-        List.hd (List.tl (snd (decompose_app sigma (pf_get_hyp_typ g h))))
-      in
-      observe_tclTHENLIST
-        (fun _ _ -> str "prove_lt1")
-        [ Proofview.V82.of_tactic
-            (apply (mkApp (le_lt_trans (), [|varx; y; varz; mkVar h|])))
-        ; observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ]
-    with Not_found ->
-      observe_tclTHENLIST
-        (fun _ _ -> str "prove_lt2")
-        [ Proofview.V82.of_tactic (apply (delayed_force lt_S_n))
-        ; observe_tac
-            (fun _ _ -> str "assumption: " ++ Printer.pr_goal g)
-            (Proofview.V82.of_tactic assumption) ]
-  end
-    g
-
-let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds g =
-  match lbounds with
-  | [] ->
-    let ids = pf_ids_of_hyps g in
-    let s_max = mkApp (delayed_force coq_S, [|bound|]) in
-    let k = next_ident_away_in_goal k_id ids in
-    let ids = k :: ids in
-    let h' = next_ident_away_in_goal h'_id ids in
-    let ids = h' :: ids in
-    let def = next_ident_away_in_goal def_id ids in
-    observe_tclTHENLIST
-      (fun _ _ -> str "destruct_bounds_aux1")
-      [ Proofview.V82.of_tactic (split (ImplicitBindings [s_max]))
-      ; Proofview.V82.of_tactic
-          (intro_then (fun id ->
-               Proofview.V82.tactic
-                 (observe_tac
-                    (fun _ _ -> str "destruct_bounds_aux")
-                    (tclTHENS
-                       (Proofview.V82.of_tactic (simplest_case (mkVar id)))
-                       [ observe_tclTHENLIST
-                           (fun _ _ -> str "")
-                           [ Proofview.V82.of_tactic
-                               (intro_using_then h_id
-                                  (* We don't care about the refreshed name,
-                                     accessed only through auto? *)
-                                  (fun _ -> Proofview.tclUNIT ()))
-                           ; Proofview.V82.of_tactic
-                               (simplest_elim
-                                  (mkApp (delayed_force lt_n_O, [|s_max|])))
-                           ; Proofview.V82.of_tactic default_full_auto ]
-                       ; observe_tclTHENLIST
-                           (fun _ _ -> str "destruct_bounds_aux2")
-                           [ observe_tac
-                               (fun _ _ -> str "clearing k ")
-                               (Proofview.V82.of_tactic (clear [id]))
-                           ; h_intros [k; h'; def]
-                           ; observe_tac
-                               (fun _ _ -> str "simple_iter")
-                               (Proofview.V82.of_tactic
-                                  (simpl_iter Locusops.onConcl))
-                           ; observe_tac
-                               (fun _ _ -> str "unfold functional")
-                               (Proofview.V82.of_tactic
-                                  (unfold_in_concl
-                                     [ ( Locus.OnlyOccurrences [1]
-                                       , evaluable_of_global_reference
-                                           infos.func ) ]))
-                           ; observe_tclTHENLIST
-                               (fun _ _ -> str "test")
-                               [ list_rewrite true
-                                   (List.fold_right
-                                      (fun e acc -> (mkVar e, true) :: acc)
-                                      infos.eqs
-                                      (List.map (fun e -> (e, true)) rechyps))
-                               ; (* list_rewrite true *)
-                                 (*   (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
-                                 (*   ; *)
-                                 observe_tac
-                                   (fun _ _ -> str "finishing")
-                                   (tclORELSE
-                                      (Proofview.V82.of_tactic
-                                         intros_reflexivity)
-                                      (observe_tac
-                                         (fun _ _ -> str "calling prove_lt")
-                                         (prove_lt hyple))) ] ] ])))) ]
-      g
-  | (_, v_bound) :: l ->
-    observe_tclTHENLIST
-      (fun _ _ -> str "destruct_bounds_aux3")
-      [ Proofview.V82.of_tactic (simplest_elim (mkVar v_bound))
-      ; Proofview.V82.of_tactic (clear [v_bound])
-      ; tclDO 2 (Proofview.V82.of_tactic intro)
-      ; onNthHypId 1 (fun p_hyp ->
-            onNthHypId 2 (fun p ->
-                observe_tclTHENLIST
-                  (fun _ _ -> str "destruct_bounds_aux4")
-                  [ Proofview.V82.of_tactic
-                      (simplest_elim
-                         (mkApp (delayed_force max_constr, [|bound; mkVar p|])))
-                  ; tclDO 3 (Proofview.V82.of_tactic intro)
-                  ; onNLastHypsId 3 (fun lids ->
-                        match lids with
-                        | [hle2; hle1; pmax] ->
-                          destruct_bounds_aux infos
-                            ( mkVar pmax
-                            , hle1 :: hle2 :: hyple
-                            , mkVar p_hyp :: rechyps )
-                            l
-                        | _ -> assert false) ])) ]
-      g
+let rec prove_lt hyple =
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      try
+        let varx, varz =
+          match decompose_app sigma (Proofview.Goal.concl g) with
+          | _, x :: z :: _ when isVar sigma x && isVar sigma z -> (x, z)
+          | _ -> assert false
+        in
+        let h =
+          List.find
+            (fun id ->
+              match decompose_app sigma (Tacmach.New.pf_get_hyp_typ id g) with
+              | _, t :: _ -> EConstr.eq_constr sigma t varx
+              | _ -> false)
+            hyple
+        in
+        let y =
+          List.hd
+            (List.tl
+               (snd (decompose_app sigma (Tacmach.New.pf_get_hyp_typ h g))))
+        in
+        New.observe_tclTHENLIST
+          (fun _ _ -> str "prove_lt1")
+          [ apply (mkApp (le_lt_trans (), [|varx; y; varz; mkVar h|]))
+          ; New.observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ]
+      with Not_found ->
+        New.observe_tclTHENLIST
+          (fun _ _ -> str "prove_lt2")
+          [ apply (delayed_force lt_S_n)
+          ; New.observe_tac
+              (fun _ _ ->
+                str "assumption: "
+                ++ Printer.pr_goal Evd.{it = Proofview.Goal.goal g; sigma})
+              assumption ])
+
+let rec destruct_bounds_aux infos (bound, hyple, rechyps) lbounds =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      match lbounds with
+      | [] ->
+        let ids = Tacmach.New.pf_ids_of_hyps g in
+        let s_max = mkApp (delayed_force coq_S, [|bound|]) in
+        let k = next_ident_away_in_goal k_id ids in
+        let ids = k :: ids in
+        let h' = next_ident_away_in_goal h'_id ids in
+        let ids = h' :: ids in
+        let def = next_ident_away_in_goal def_id ids in
+        New.observe_tclTHENLIST
+          (fun _ _ -> str "destruct_bounds_aux1")
+          [ split (ImplicitBindings [s_max])
+          ; intro_then (fun id ->
+                New.observe_tac
+                  (fun _ _ -> str "destruct_bounds_aux")
+                  (tclTHENS
+                     (simplest_case (mkVar id))
+                     [ New.observe_tclTHENLIST
+                         (fun _ _ -> str "")
+                         [ intro_using_then h_id
+                             (* We don't care about the refreshed name,
+                                accessed only through auto? *)
+                             (fun _ -> Proofview.tclUNIT ())
+                         ; simplest_elim
+                             (mkApp (delayed_force lt_n_O, [|s_max|]))
+                         ; default_full_auto ]
+                     ; New.observe_tclTHENLIST
+                         (fun _ _ -> str "destruct_bounds_aux2")
+                         [ New.observe_tac
+                             (fun _ _ -> str "clearing k ")
+                             (clear [id])
+                         ; h_intros [k; h'; def]
+                         ; New.observe_tac
+                             (fun _ _ -> str "simple_iter")
+                             (simpl_iter Locusops.onConcl)
+                         ; New.observe_tac
+                             (fun _ _ -> str "unfold functional")
+                             (unfold_in_concl
+                                [ ( Locus.OnlyOccurrences [1]
+                                  , evaluable_of_global_reference infos.func )
+                                ])
+                         ; New.observe_tclTHENLIST
+                             (fun _ _ -> str "test")
+                             [ list_rewrite true
+                                 (List.fold_right
+                                    (fun e acc -> (mkVar e, true) :: acc)
+                                    infos.eqs
+                                    (List.map (fun e -> (e, true)) rechyps))
+                             ; (* list_rewrite true *)
+                               (*   (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
+                               (*   ; *)
+                               New.observe_tac
+                                 (fun _ _ -> str "finishing")
+                                 (tclORELSE intros_reflexivity
+                                    (New.observe_tac
+                                       (fun _ _ -> str "calling prove_lt")
+                                       (prove_lt hyple))) ] ] ])) ]
+      | (_, v_bound) :: l ->
+        New.observe_tclTHENLIST
+          (fun _ _ -> str "destruct_bounds_aux3")
+          [ simplest_elim (mkVar v_bound)
+          ; clear [v_bound]
+          ; tclDO 2 intro
+          ; onNthHypId 1 (fun p_hyp ->
+                onNthHypId 2 (fun p ->
+                    New.observe_tclTHENLIST
+                      (fun _ _ -> str "destruct_bounds_aux4")
+                      [ simplest_elim
+                          (mkApp (delayed_force max_constr, [|bound; mkVar p|]))
+                      ; tclDO 3 intro
+                      ; onNLastHypsId 3 (fun lids ->
+                            match lids with
+                            | [hle2; hle1; pmax] ->
+                              destruct_bounds_aux infos
+                                ( mkVar pmax
+                                , hle1 :: hle2 :: hyple
+                                , mkVar p_hyp :: rechyps )
+                                l
+                            | _ -> assert false) ])) ])
 
 let destruct_bounds infos =
   destruct_bounds_aux infos
@@ -679,47 +657,51 @@ let destruct_bounds infos =
 
 let terminate_app f_and_args expr_info continuation_tac infos =
   if expr_info.is_final && expr_info.is_main_branch then
-    observe_tclTHENLIST
+    New.observe_tclTHENLIST
       (fun _ _ -> str "terminate_app1")
       [ continuation_tac infos
-      ; observe_tac
+      ; New.observe_tac
           (fun _ _ -> str "first split")
-          (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])))
-      ; observe_tac
+          (split (ImplicitBindings [infos.info]))
+      ; New.observe_tac
           (fun _ _ -> str "destruct_bounds (1)")
           (destruct_bounds infos) ]
   else continuation_tac infos
 
 let terminate_others _ expr_info continuation_tac infos =
   if expr_info.is_final && expr_info.is_main_branch then
-    observe_tclTHENLIST
+    New.observe_tclTHENLIST
       (fun _ _ -> str "terminate_others")
       [ continuation_tac infos
-      ; observe_tac
+      ; New.observe_tac
           (fun _ _ -> str "first split")
-          (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])))
-      ; observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos)
-      ]
+          (split (ImplicitBindings [infos.info]))
+      ; New.observe_tac
+          (fun _ _ -> str "destruct_bounds")
+          (destruct_bounds infos) ]
   else continuation_tac infos
 
-let terminate_letin (na, b, t, e) expr_info continuation_tac info g =
-  let sigma = project g in
-  let env = pf_env g in
-  let new_e = subst1 info.info e in
-  let new_forbidden =
-    let forbid =
-      try
-        check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids) b;
-        true
-      with e when CErrors.noncritical e -> false
-    in
-    if forbid then
-      match na with
-      | Anonymous -> info.forbidden_ids
-      | Name id -> id :: info.forbidden_ids
-    else info.forbidden_ids
-  in
-  continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
+let terminate_letin (na, b, t, e) expr_info continuation_tac info =
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      let env = Proofview.Goal.env g in
+      let new_e = subst1 info.info e in
+      let new_forbidden =
+        let forbid =
+          try
+            check_not_nested env sigma
+              (expr_info.f_id :: expr_info.forbidden_ids)
+              b;
+            true
+          with e when CErrors.noncritical e -> false
+        in
+        if forbid then
+          match na with
+          | Anonymous -> info.forbidden_ids
+          | Name id -> id :: info.forbidden_ids
+        else info.forbidden_ids
+      in
+      continuation_tac {info with info = new_e; forbidden_ids = new_forbidden})
 
 let pf_type c tac =
   let open Tacticals.New in
@@ -729,9 +711,6 @@ let pf_type c tac =
       let evars, ty = Typing.type_of env sigma c in
       tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty))
 
-let pf_type c tac =
-  Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty)))
-
 let pf_typel l tac =
   let rec aux tys l =
     match l with
@@ -745,8 +724,8 @@ let pf_typel l tac =
   modified hypotheses are generalized in the process and should be
   introduced back later; the result is the pair of the tactic and the
   list of hypotheses that have been generalized and cleared. *)
-let mkDestructEq not_on_hyp expr g =
-  let hyps = pf_hyps g in
+let mkDestructEq not_on_hyp env sigma expr =
+  let hyps = EConstr.named_context env in
   let to_revert =
     Util.List.map_filter
       (fun decl ->
@@ -754,173 +733,169 @@ let mkDestructEq not_on_hyp expr g =
         let id = get_id decl in
         if
           Id.List.mem id not_on_hyp
-          || not (Termops.dependent (project g) expr (get_type decl))
+          || not (Termops.dependent sigma expr (get_type decl))
         then None
         else Some id)
       hyps
   in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let g, type_of_expr = tac_type_of g expr in
+  let sigma, type_of_expr = Typing.type_of env sigma expr in
   let new_hyps =
     mkApp (Lazy.force refl_equal, [|type_of_expr; expr|]) :: to_revert_constr
   in
   let tac =
     pf_typel new_hyps (fun _ ->
-        observe_tclTHENLIST
+        New.observe_tclTHENLIST
           (fun _ _ -> str "mkDestructEq")
-          [ Proofview.V82.of_tactic (generalize new_hyps)
-          ; (fun g2 ->
-              let changefun patvars env sigma =
-                pattern_occs
-                  [(Locus.AllOccurrencesBut [1], expr)]
-                  (pf_env g2) sigma (pf_concl g2)
-              in
-              Proofview.V82.of_tactic
-                (change_in_concl ~check:true None changefun)
-                g2)
-          ; Proofview.V82.of_tactic (simplest_case expr) ])
+          [ generalize new_hyps
+          ; Proofview.Goal.enter (fun g2 ->
+                let changefun patvars env sigma =
+                  pattern_occs
+                    [(Locus.AllOccurrencesBut [1], expr)]
+                    (Proofview.Goal.env g2) sigma (Proofview.Goal.concl g2)
+                in
+                change_in_concl ~check:true None changefun)
+          ; simplest_case expr ])
   in
-  (g, tac, to_revert)
+  (sigma, tac, to_revert)
 
 let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
-    g =
-  let sigma = project g in
-  let env = pf_env g in
-  let f_is_present =
-    try
-      check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids) a;
-      false
-    with e when CErrors.noncritical e -> true
-  in
-  let a' = infos.info in
-  let new_info =
-    { infos with
-      info = mkCase (ci, t, iv, a', l)
-    ; is_main_branch = expr_info.is_main_branch
-    ; is_final = expr_info.is_final }
-  in
-  let g, destruct_tac, rev_to_thin_intro =
-    mkDestructEq [expr_info.rec_arg_id] a' g
-  in
-  let to_thin_intro = List.rev rev_to_thin_intro in
-  observe_tac
-    (fun _ _ ->
-      str "treating cases ("
-      ++ int (Array.length l)
-      ++ str ")" ++ spc ()
-      ++ Printer.pr_leconstr_env (pf_env g) sigma a')
-    ( try
-        tclTHENS destruct_tac
-          (List.map_i
-             (fun i e ->
-               observe_tac
-                 (fun _ _ -> str "do treat case")
-                 (treat_case f_is_present to_thin_intro
-                    (next_step continuation_tac)
-                    ci.ci_cstr_ndecls.(i) e new_info))
-             0 (Array.to_list l))
-      with
-      | UserError (Some "Refiner.thensn_tac3", _)
-       |UserError (Some "Refiner.tclFAIL_s", _)
-      ->
-        observe_tac
-          (fun _ _ ->
-            str "is computable "
-            ++ Printer.pr_leconstr_env env sigma new_info.info)
-          (next_step continuation_tac
-             { new_info with
-               info =
-                 Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info })
-    )
-    g
-
-let terminate_app_rec (f, args) expr_info continuation_tac _ g =
-  let sigma = project g in
-  let env = pf_env g in
-  List.iter
-    (check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids))
-    args;
-  try
-    let v =
-      List.assoc_f
-        (List.equal (EConstr.eq_constr sigma))
-        args expr_info.args_assoc
-    in
-    let new_infos = {expr_info with info = v} in
-    observe_tclTHENLIST
-      (fun _ _ -> str "terminate_app_rec")
-      [ continuation_tac new_infos
-      ; ( if expr_info.is_final && expr_info.is_main_branch then
-          observe_tclTHENLIST
-            (fun _ _ -> str "terminate_app_rec1")
-            [ observe_tac
-                (fun _ _ -> str "first split")
-                (Proofview.V82.of_tactic
-                   (split (ImplicitBindings [new_infos.info])))
-            ; observe_tac
-                (fun _ _ -> str "destruct_bounds (3)")
-                (destruct_bounds new_infos) ]
-        else tclIDTAC ) ]
-      g
-  with Not_found ->
-    observe_tac
-      (fun _ _ -> str "terminate_app_rec not found")
-      (tclTHENS
-         (Proofview.V82.of_tactic
-            (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args))))
-         [ observe_tclTHENLIST
-             (fun _ _ -> str "terminate_app_rec2")
-             [ Proofview.V82.of_tactic
-                 (intro_using_then rec_res_id
-                    (* refreshed name gotten from onNthHypId *)
-                    (fun _ -> Proofview.tclUNIT ()))
-             ; Proofview.V82.of_tactic intro
-             ; onNthHypId 1 (fun v_bound ->
-                   onNthHypId 2 (fun v ->
-                       let new_infos =
-                         { expr_info with
-                           info = mkVar v
-                         ; values_and_bounds =
-                             (v, v_bound) :: expr_info.values_and_bounds
-                         ; args_assoc = (args, mkVar v) :: expr_info.args_assoc
-                         }
-                       in
-                       observe_tclTHENLIST
-                         (fun _ _ -> str "terminate_app_rec3")
-                         [ continuation_tac new_infos
-                         ; ( if expr_info.is_final && expr_info.is_main_branch
-                           then
-                             observe_tclTHENLIST
-                               (fun _ _ -> str "terminate_app_rec4")
-                               [ observe_tac
-                                   (fun _ _ -> str "first split")
-                                   (Proofview.V82.of_tactic
-                                      (split
-                                         (ImplicitBindings [new_infos.info])))
-                               ; observe_tac
-                                   (fun _ _ -> str "destruct_bounds (2)")
-                                   (destruct_bounds new_infos) ]
-                           else tclIDTAC ) ])) ]
-         ; observe_tac
-             (fun _ _ -> str "proving decreasing")
-             (tclTHENS (* proof of args < formal args *)
-                (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
-                [ observe_tac
-                    (fun _ _ -> str "assumption")
-                    (Proofview.V82.of_tactic assumption)
-                ; observe_tclTHENLIST
-                    (fun _ _ -> str "terminate_app_rec5")
-                    [ tclTRY
-                        (list_rewrite true
-                           (List.map (fun e -> (mkVar e, true)) expr_info.eqs))
-                    ; Proofview.V82.of_tactic
-                      @@ tclUSER expr_info.concl_tac true
-                           (Some
-                              ( expr_info.ih :: expr_info.acc_id
-                              :: (fun (x, y) -> y)
-                                   (List.split expr_info.values_and_bounds) ))
-                    ] ]) ])
-      g
+    =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      let env = Proofview.Goal.env g in
+      let f_is_present =
+        try
+          check_not_nested env sigma
+            (expr_info.f_id :: expr_info.forbidden_ids)
+            a;
+          false
+        with e when CErrors.noncritical e -> true
+      in
+      let a' = infos.info in
+      let new_info =
+        { infos with
+          info = mkCase (ci, t, iv, a', l)
+        ; is_main_branch = expr_info.is_main_branch
+        ; is_final = expr_info.is_final }
+      in
+      let sigma, destruct_tac, rev_to_thin_intro =
+        mkDestructEq [expr_info.rec_arg_id] env sigma a'
+      in
+      let to_thin_intro = List.rev rev_to_thin_intro in
+      New.observe_tac
+        (fun _ _ ->
+          str "treating cases ("
+          ++ int (Array.length l)
+          ++ str ")" ++ spc ()
+          ++ Printer.pr_leconstr_env env sigma a')
+        ( try
+            tclTHENS destruct_tac
+              (List.map_i
+                 (fun i e ->
+                   New.observe_tac
+                     (fun _ _ -> str "do treat case")
+                     (treat_case f_is_present to_thin_intro
+                        (next_step continuation_tac)
+                        ci.ci_cstr_ndecls.(i) e new_info))
+                 0 (Array.to_list l))
+          with
+          | UserError (Some "Refiner.thensn_tac3", _)
+           |UserError (Some "Refiner.tclFAIL_s", _)
+          ->
+            New.observe_tac
+              (fun _ _ ->
+                str "is computable "
+                ++ Printer.pr_leconstr_env env sigma new_info.info)
+              (next_step continuation_tac
+                 { new_info with
+                   info = Reductionops.nf_betaiotazeta env sigma new_info.info
+                 }) ))
+
+let terminate_app_rec (f, args) expr_info continuation_tac _ =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      let env = Proofview.Goal.env g in
+      List.iter
+        (check_not_nested env sigma (expr_info.f_id :: expr_info.forbidden_ids))
+        args;
+      try
+        let v =
+          List.assoc_f
+            (List.equal (EConstr.eq_constr sigma))
+            args expr_info.args_assoc
+        in
+        let new_infos = {expr_info with info = v} in
+        New.observe_tclTHENLIST
+          (fun _ _ -> str "terminate_app_rec")
+          [ continuation_tac new_infos
+          ; ( if expr_info.is_final && expr_info.is_main_branch then
+              New.observe_tclTHENLIST
+                (fun _ _ -> str "terminate_app_rec1")
+                [ New.observe_tac
+                    (fun _ _ -> str "first split")
+                    (split (ImplicitBindings [new_infos.info]))
+                ; New.observe_tac
+                    (fun _ _ -> str "destruct_bounds (3)")
+                    (destruct_bounds new_infos) ]
+            else Proofview.tclUNIT () ) ]
+      with Not_found ->
+        New.observe_tac
+          (fun _ _ -> str "terminate_app_rec not found")
+          (tclTHENS
+             (simplest_elim (mkApp (mkVar expr_info.ih, Array.of_list args)))
+             [ New.observe_tclTHENLIST
+                 (fun _ _ -> str "terminate_app_rec2")
+                 [ intro_using_then rec_res_id
+                     (* refreshed name gotten from onNthHypId *)
+                     (fun _ -> Proofview.tclUNIT ())
+                 ; intro
+                 ; onNthHypId 1 (fun v_bound ->
+                       onNthHypId 2 (fun v ->
+                           let new_infos =
+                             { expr_info with
+                               info = mkVar v
+                             ; values_and_bounds =
+                                 (v, v_bound) :: expr_info.values_and_bounds
+                             ; args_assoc =
+                                 (args, mkVar v) :: expr_info.args_assoc }
+                           in
+                           New.observe_tclTHENLIST
+                             (fun _ _ -> str "terminate_app_rec3")
+                             [ continuation_tac new_infos
+                             ; ( if
+                                 expr_info.is_final && expr_info.is_main_branch
+                               then
+                                 New.observe_tclTHENLIST
+                                   (fun _ _ -> str "terminate_app_rec4")
+                                   [ New.observe_tac
+                                       (fun _ _ -> str "first split")
+                                       (split
+                                          (ImplicitBindings [new_infos.info]))
+                                   ; New.observe_tac
+                                       (fun _ _ -> str "destruct_bounds (2)")
+                                       (destruct_bounds new_infos) ]
+                               else Proofview.tclUNIT () ) ])) ]
+             ; New.observe_tac
+                 (fun _ _ -> str "proving decreasing")
+                 (tclTHENS (* proof of args < formal args *)
+                    (apply (Lazy.force expr_info.acc_inv))
+                    [ New.observe_tac (fun _ _ -> str "assumption") assumption
+                    ; New.observe_tclTHENLIST
+                        (fun _ _ -> str "terminate_app_rec5")
+                        [ tclTRY
+                            (list_rewrite true
+                               (List.map
+                                  (fun e -> (mkVar e, true))
+                                  expr_info.eqs))
+                        ; tclUSER expr_info.concl_tac true
+                            (Some
+                               ( expr_info.ih :: expr_info.acc_id
+                               :: (fun (x, y) -> y)
+                                    (List.split expr_info.values_and_bounds) ))
+                        ] ]) ]))
 
 let terminate_info =
   { message = "prove_terminate with term "
@@ -936,194 +911,197 @@ let prove_terminate = travel terminate_info
 (* Equation proof *)
 
 let equation_case next_step case expr_info continuation_tac infos =
-  observe_tac
+  New.observe_tac
     (fun _ _ -> str "equation case")
     (terminate_case next_step case expr_info continuation_tac infos)
 
-let rec prove_le g =
-  let sigma = project g in
-  let x, z =
-    let _, args = decompose_app sigma (pf_concl g) in
-    (List.hd args, List.hd (List.tl args))
-  in
-  tclFIRST
-    [ Proofview.V82.of_tactic assumption
-    ; Proofview.V82.of_tactic (apply (delayed_force le_n))
-    ; begin
-        try
-          let matching_fun c =
-            match EConstr.kind sigma c with
-            | App (c, [|x0; _|]) ->
-              EConstr.isVar sigma x0
-              && Id.equal (destVar sigma x0) (destVar sigma x)
-              && EConstr.isRefX sigma (le ()) c
-            | _ -> false
-          in
-          let h, t =
-            List.find (fun (_, t) -> matching_fun t) (pf_hyps_types g)
-          in
-          let h = h.binder_name in
-          let y =
-            let _, args = decompose_app sigma t in
-            List.hd (List.tl args)
-          in
-          observe_tclTHENLIST
-            (fun _ _ -> str "prove_le")
-            [ Proofview.V82.of_tactic
-                (apply (mkApp (le_trans (), [|x; y; z; mkVar h|])))
-            ; observe_tac (fun _ _ -> str "prove_le (rec)") prove_le ]
-        with Not_found -> tclFAIL 0 (mt ())
-      end ]
-    g
+let rec prove_le () =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      let x, z =
+        let _, args = decompose_app sigma (Proofview.Goal.concl g) in
+        (List.hd args, List.hd (List.tl args))
+      in
+      tclFIRST
+        [ assumption
+        ; apply (delayed_force le_n)
+        ; begin
+            try
+              let matching_fun c =
+                match EConstr.kind sigma c with
+                | App (c, [|x0; _|]) ->
+                  EConstr.isVar sigma x0
+                  && Id.equal (destVar sigma x0) (destVar sigma x)
+                  && EConstr.isRefX sigma (le ()) c
+                | _ -> false
+              in
+              let h, t =
+                List.find
+                  (fun (_, t) -> matching_fun t)
+                  (Tacmach.New.pf_hyps_types g)
+              in
+              let y =
+                let _, args = decompose_app sigma t in
+                List.hd (List.tl args)
+              in
+              New.observe_tclTHENLIST
+                (fun _ _ -> str "prove_le")
+                [ apply (mkApp (le_trans (), [|x; y; z; mkVar h|]))
+                ; New.observe_tac
+                    (fun _ _ -> str "prove_le (rec)")
+                    (prove_le ()) ]
+            with Not_found -> Tacticals.New.tclFAIL 0 (mt ())
+          end ])
 
 let rec make_rewrite_list expr_info max = function
-  | [] -> tclIDTAC
+  | [] -> Proofview.tclUNIT ()
   | (_, p, hp) :: l ->
-    observe_tac
+    let open Tacticals.New in
+    New.observe_tac
       (fun _ _ -> str "make_rewrite_list")
       (tclTHENS
-         (observe_tac
+         (New.observe_tac
             (fun _ _ -> str "rewrite heq on " ++ Id.print p)
-            (fun g ->
-              let sigma = project g in
-              let t_eq = compute_renamed_type g hp in
-              let k, def =
-                let k_na, _, t = destProd sigma t_eq in
-                let _, _, t = destProd sigma t in
-                let def_na, _, _ = destProd sigma t in
-                ( Nameops.Name.get_id k_na.binder_name
-                , Nameops.Name.get_id def_na.binder_name )
-              in
-              Proofview.V82.of_tactic
-                (general_rewrite_bindings false Locus.AllOccurrences true
+            (Proofview.Goal.enter (fun g ->
+                 let sigma = Proofview.Goal.sigma g in
+                 let t_eq = compute_renamed_type g hp in
+                 let k, def =
+                   let k_na, _, t = destProd sigma t_eq in
+                   let _, _, t = destProd sigma t in
+                   let def_na, _, _ = destProd sigma t in
+                   ( Nameops.Name.get_id k_na.binder_name
+                   , Nameops.Name.get_id def_na.binder_name )
+                 in
+                 general_rewrite_bindings false Locus.AllOccurrences true
                    (* dep proofs also: *) true
                    ( mkVar hp
                    , ExplicitBindings
                        [ CAst.make @@ (NamedHyp def, expr_info.f_constr)
                        ; CAst.make @@ (NamedHyp k, f_S max) ] )
-                   false)
-                g))
+                   false)))
          [ make_rewrite_list expr_info max l
-         ; observe_tclTHENLIST
+         ; New.observe_tclTHENLIST
              (fun _ _ -> str "make_rewrite_list")
              [ (* x < S max proof *)
-               Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm))
-             ; observe_tac (fun _ _ -> str "prove_le(2)") prove_le ] ])
+               apply (delayed_force le_lt_n_Sm)
+             ; New.observe_tac (fun _ _ -> str "prove_le(2)") (prove_le ()) ] ])
 
 let make_rewrite expr_info l hp max =
+  let open Tacticals.New in
   tclTHENFIRST
-    (observe_tac
+    (New.observe_tac
        (fun _ _ -> str "make_rewrite")
        (make_rewrite_list expr_info max l))
-    (observe_tac
+    (New.observe_tac
        (fun _ _ -> str "make_rewrite")
        (tclTHENS
-          (fun g ->
-            let sigma = project g in
-            let t_eq = compute_renamed_type g hp in
-            let k, def =
-              let k_na, _, t = destProd sigma t_eq in
-              let _, _, t = destProd sigma t in
-              let def_na, _, _ = destProd sigma t in
-              ( Nameops.Name.get_id k_na.binder_name
-              , Nameops.Name.get_id def_na.binder_name )
-            in
-            observe_tac
-              (fun _ _ -> str "general_rewrite_bindings")
-              (Proofview.V82.of_tactic
+          (Proofview.Goal.enter (fun g ->
+               let sigma = Proofview.Goal.sigma g in
+               let t_eq = compute_renamed_type g hp in
+               let k, def =
+                 let k_na, _, t = destProd sigma t_eq in
+                 let _, _, t = destProd sigma t in
+                 let def_na, _, _ = destProd sigma t in
+                 ( Nameops.Name.get_id k_na.binder_name
+                 , Nameops.Name.get_id def_na.binder_name )
+               in
+               New.observe_tac
+                 (fun _ _ -> str "general_rewrite_bindings")
                  (general_rewrite_bindings false Locus.AllOccurrences true
                     (* dep proofs also: *) true
                     ( mkVar hp
                     , ExplicitBindings
                         [ CAst.make @@ (NamedHyp def, expr_info.f_constr)
                         ; CAst.make @@ (NamedHyp k, f_S (f_S max)) ] )
-                    false))
-              g)
-          [ observe_tac
+                    false)))
+          [ New.observe_tac
               (fun _ _ -> str "make_rewrite finalize")
               ((* tclORELSE( h_reflexivity) *)
-               observe_tclTHENLIST
+               New.observe_tclTHENLIST
                  (fun _ _ -> str "make_rewrite")
-                 [ Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)
-                 ; observe_tac
+                 [ simpl_iter Locusops.onConcl
+                 ; New.observe_tac
                      (fun _ _ -> str "unfold functional")
-                     (Proofview.V82.of_tactic
-                        (unfold_in_concl
-                           [ ( Locus.OnlyOccurrences [1]
-                             , evaluable_of_global_reference expr_info.func ) ]))
+                     (unfold_in_concl
+                        [ ( Locus.OnlyOccurrences [1]
+                          , evaluable_of_global_reference expr_info.func ) ])
                  ; list_rewrite true
                      (List.map (fun e -> (mkVar e, true)) expr_info.eqs)
-                 ; observe_tac
+                 ; New.observe_tac
                      (fun _ _ -> str "h_reflexivity")
-                     (Proofview.V82.of_tactic intros_reflexivity) ])
-          ; observe_tclTHENLIST
+                     intros_reflexivity ])
+          ; New.observe_tclTHENLIST
               (fun _ _ -> str "make_rewrite1")
               [ (* x < S (S max) proof *)
-                Proofview.V82.of_tactic
-                  (apply (EConstr.of_constr (delayed_force le_lt_SS)))
-              ; observe_tac (fun _ _ -> str "prove_le (3)") prove_le ] ]))
+                apply (EConstr.of_constr (delayed_force le_lt_SS))
+              ; New.observe_tac (fun _ _ -> str "prove_le (3)") (prove_le ()) ]
+          ]))
 
 let rec compute_max rew_tac max l =
   match l with
   | [] -> rew_tac max
   | (_, p, _) :: l ->
-    observe_tclTHENLIST
+    let open Tacticals.New in
+    New.observe_tclTHENLIST
       (fun _ _ -> str "compute_max")
-      [ Proofview.V82.of_tactic
-          (simplest_elim (mkApp (delayed_force max_constr, [|max; mkVar p|])))
-      ; tclDO 3 (Proofview.V82.of_tactic intro)
+      [ simplest_elim (mkApp (delayed_force max_constr, [|max; mkVar p|]))
+      ; tclDO 3 intro
       ; onNLastHypsId 3 (fun lids ->
             match lids with
             | [hle2; hle1; pmax] -> compute_max rew_tac (mkVar pmax) l
             | _ -> assert false) ]
 
 let rec destruct_hex expr_info acc l =
+  let open Tacticals.New in
   match l with
   | [] -> (
     match List.rev acc with
-    | [] -> tclIDTAC
+    | [] -> Proofview.tclUNIT ()
     | (_, p, hp) :: tl ->
-      observe_tac
+      New.observe_tac
         (fun _ _ -> str "compute max ")
         (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) )
   | (v, hex) :: l ->
-    observe_tclTHENLIST
+    New.observe_tclTHENLIST
       (fun _ _ -> str "destruct_hex")
-      [ Proofview.V82.of_tactic (simplest_case (mkVar hex))
-      ; Proofview.V82.of_tactic (clear [hex])
-      ; tclDO 2 (Proofview.V82.of_tactic intro)
+      [ simplest_case (mkVar hex)
+      ; clear [hex]
+      ; tclDO 2 intro
       ; onNthHypId 1 (fun hp ->
             onNthHypId 2 (fun p ->
-                observe_tac
+                New.observe_tac
                   (fun _ _ ->
                     str "destruct_hex after " ++ Id.print hp ++ spc ()
                     ++ Id.print p)
                   (destruct_hex expr_info ((v, p, hp) :: acc) l))) ]
 
 let rec intros_values_eq expr_info acc =
+  let open Tacticals.New in
   tclORELSE
-    (observe_tclTHENLIST
+    (New.observe_tclTHENLIST
        (fun _ _ -> str "intros_values_eq")
-       [ tclDO 2 (Proofview.V82.of_tactic intro)
+       [ tclDO 2 intro
        ; onNthHypId 1 (fun hex ->
              onNthHypId 2 (fun v ->
                  intros_values_eq expr_info ((v, hex) :: acc))) ])
     (tclCOMPLETE (destruct_hex expr_info [] acc))
 
 let equation_others _ expr_info continuation_tac infos =
+  let open Tacticals.New in
   if expr_info.is_final && expr_info.is_main_branch then
-    observe_tac
+    New.observe_tac
       (fun env sigma ->
         str "equation_others (cont_tac +intros) "
         ++ Printer.pr_leconstr_env env sigma expr_info.info)
       (tclTHEN (continuation_tac infos)
-         (observe_tac
+         (New.observe_tac
             (fun env sigma ->
               str "intros_values_eq equation_others "
               ++ Printer.pr_leconstr_env env sigma expr_info.info)
             (intros_values_eq expr_info [])))
   else
-    observe_tac
+    New.observe_tac
       (fun env sigma ->
         str "equation_others (cont_tac) "
         ++ Printer.pr_leconstr_env env sigma expr_info.info)
@@ -1131,47 +1109,46 @@ let equation_others _ expr_info continuation_tac infos =
 
 let equation_app f_and_args expr_info continuation_tac infos =
   if expr_info.is_final && expr_info.is_main_branch then
-    observe_tac
+    New.observe_tac
       (fun _ _ -> str "intros_values_eq equation_app")
       (intros_values_eq expr_info [])
   else continuation_tac infos
 
-let equation_app_rec (f, args) expr_info continuation_tac info g =
-  let sigma = project g in
-  try
-    let v =
-      List.assoc_f
-        (List.equal (EConstr.eq_constr sigma))
-        args expr_info.args_assoc
-    in
-    let new_infos = {expr_info with info = v} in
-    observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) g
-  with Not_found ->
-    if expr_info.is_final && expr_info.is_main_branch then
-      observe_tclTHENLIST
-        (fun _ _ -> str "equation_app_rec")
-        [ Proofview.V82.of_tactic
-            (simplest_case (mkApp (expr_info.f_terminate, Array.of_list args)))
-        ; continuation_tac
-            { expr_info with
-              args_assoc = (args, delayed_force coq_O) :: expr_info.args_assoc
-            }
-        ; observe_tac
-            (fun _ _ -> str "app_rec intros_values_eq")
-            (intros_values_eq expr_info []) ]
-        g
-    else
-      observe_tclTHENLIST
-        (fun _ _ -> str "equation_app_rec1")
-        [ Proofview.V82.of_tactic
-            (simplest_case (mkApp (expr_info.f_terminate, Array.of_list args)))
-        ; observe_tac
-            (fun _ _ -> str "app_rec not_found")
-            (continuation_tac
-               { expr_info with
-                 args_assoc =
-                   (args, delayed_force coq_O) :: expr_info.args_assoc }) ]
-        g
+let equation_app_rec (f, args) expr_info continuation_tac info =
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      try
+        let v =
+          List.assoc_f
+            (List.equal (EConstr.eq_constr sigma))
+            args expr_info.args_assoc
+        in
+        let new_infos = {expr_info with info = v} in
+        New.observe_tac
+          (fun _ _ -> str "app_rec found")
+          (continuation_tac new_infos)
+      with Not_found ->
+        if expr_info.is_final && expr_info.is_main_branch then
+          New.observe_tclTHENLIST
+            (fun _ _ -> str "equation_app_rec")
+            [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))
+            ; continuation_tac
+                { expr_info with
+                  args_assoc =
+                    (args, delayed_force coq_O) :: expr_info.args_assoc }
+            ; New.observe_tac
+                (fun _ _ -> str "app_rec intros_values_eq")
+                (intros_values_eq expr_info []) ]
+        else
+          New.observe_tclTHENLIST
+            (fun _ _ -> str "equation_app_rec1")
+            [ simplest_case (mkApp (expr_info.f_terminate, Array.of_list args))
+            ; New.observe_tac
+                (fun _ _ -> str "app_rec not_found")
+                (continuation_tac
+                   { expr_info with
+                     args_assoc =
+                       (args, delayed_force coq_O) :: expr_info.args_assoc }) ])
 
 let equation_info =
   { message = "prove_equation with term "
@@ -1231,73 +1208,68 @@ let compute_terminate_type nb_args func =
   compose_prod rev_args value
 
 let termination_proof_header is_mes input_type ids args_id relation rec_arg_num
-    rec_arg_id tac wf_tac : tactic =
- fun g ->
-  let nargs = List.length args_id in
-  let pre_rec_args =
-    List.rev_map mkVar (fst (List.chop (rec_arg_num - 1) args_id))
-  in
-  let relation = substl pre_rec_args relation in
-  let input_type = substl pre_rec_args input_type in
-  let wf_thm = next_ident_away_in_goal (Id.of_string "wf_R") ids in
-  let wf_rec_arg =
-    next_ident_away_in_goal
-      (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))
-      (wf_thm :: ids)
-  in
-  let hrec = next_ident_away_in_goal hrec_id (wf_rec_arg :: wf_thm :: ids) in
-  let acc_inv =
-    lazy
-      (mkApp
-         (delayed_force acc_inv_id, [|input_type; relation; mkVar rec_arg_id|]))
-  in
-  tclTHEN (h_intros args_id)
-    (tclTHENS
-       (observe_tac
-          (fun _ _ -> str "first assert")
-          (Proofview.V82.of_tactic
-             (assert_before (Name wf_rec_arg)
-                (mkApp
-                   ( delayed_force acc_rel
-                   , [|input_type; relation; mkVar rec_arg_id|] )))))
-       [ (* accesibility proof *)
-         tclTHENS
-           (observe_tac
-              (fun _ _ -> str "second assert")
-              (Proofview.V82.of_tactic
-                 (assert_before (Name wf_thm)
-                    (mkApp
-                       (delayed_force well_founded, [|input_type; relation|])))))
-           [ (* interactive proof that the relation is well_founded *)
-             observe_tac
-               (fun _ _ -> str "wf_tac")
-               (wf_tac is_mes (Some args_id))
-           ; (* this gives the accessibility argument *)
-             observe_tac
-               (fun _ _ -> str "apply wf_thm")
-               (Proofview.V82.of_tactic
-                  (Simple.apply (mkApp (mkVar wf_thm, [|mkVar rec_arg_id|]))))
-           ]
-       ; (* rest of the proof *)
-         observe_tclTHENLIST
-           (fun _ _ -> str "rest of proof")
-           [ observe_tac
-               (fun _ _ -> str "generalize")
-               (onNLastHypsId (nargs + 1)
-                  (tclMAP (fun id ->
-                       tclTHEN
-                         (Proofview.V82.of_tactic
-                            (Tactics.generalize [mkVar id]))
-                         (Proofview.V82.of_tactic (clear [id])))))
-           ; observe_tac
-               (fun _ _ -> str "fix")
-               (Proofview.V82.of_tactic (fix hrec (nargs + 1)))
-           ; h_intros args_id
-           ; Proofview.V82.of_tactic (Simple.intro wf_rec_arg)
-           ; observe_tac
-               (fun _ _ -> str "tac")
-               (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ])
-    g
+    rec_arg_id tac wf_tac : unit Proofview.tactic =
+  let open Tacticals.New in
+  Proofview.Goal.enter (fun g ->
+      let nargs = List.length args_id in
+      let pre_rec_args =
+        List.rev_map mkVar (fst (List.chop (rec_arg_num - 1) args_id))
+      in
+      let relation = substl pre_rec_args relation in
+      let input_type = substl pre_rec_args input_type in
+      let wf_thm = next_ident_away_in_goal (Id.of_string "wf_R") ids in
+      let wf_rec_arg =
+        next_ident_away_in_goal
+          (Id.of_string ("Acc_" ^ Id.to_string rec_arg_id))
+          (wf_thm :: ids)
+      in
+      let hrec =
+        next_ident_away_in_goal hrec_id (wf_rec_arg :: wf_thm :: ids)
+      in
+      let acc_inv =
+        lazy
+          (mkApp
+             ( delayed_force acc_inv_id
+             , [|input_type; relation; mkVar rec_arg_id|] ))
+      in
+      tclTHEN (h_intros args_id)
+        (tclTHENS
+           (New.observe_tac
+              (fun _ _ -> str "first assert")
+              (assert_before (Name wf_rec_arg)
+                 (mkApp
+                    ( delayed_force acc_rel
+                    , [|input_type; relation; mkVar rec_arg_id|] ))))
+           [ (* accesibility proof *)
+             tclTHENS
+               (New.observe_tac
+                  (fun _ _ -> str "second assert")
+                  (assert_before (Name wf_thm)
+                     (mkApp
+                        (delayed_force well_founded, [|input_type; relation|]))))
+               [ (* interactive proof that the relation is well_founded *)
+                 New.observe_tac
+                   (fun _ _ -> str "wf_tac")
+                   (wf_tac is_mes (Some args_id))
+               ; (* this gives the accessibility argument *)
+                 New.observe_tac
+                   (fun _ _ -> str "apply wf_thm")
+                   (Simple.apply (mkApp (mkVar wf_thm, [|mkVar rec_arg_id|])))
+               ]
+           ; (* rest of the proof *)
+             New.observe_tclTHENLIST
+               (fun _ _ -> str "rest of proof")
+               [ New.observe_tac
+                   (fun _ _ -> str "generalize")
+                   (onNLastHypsId (nargs + 1)
+                      (tclMAP (fun id ->
+                           tclTHEN (Tactics.generalize [mkVar id]) (clear [id]))))
+               ; New.observe_tac (fun _ _ -> str "fix") (fix hrec (nargs + 1))
+               ; h_intros args_id
+               ; Simple.intro wf_rec_arg
+               ; New.observe_tac
+                   (fun _ _ -> str "tac")
+                   (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ]))
 
 let rec instantiate_lambda sigma t l =
   match l with
@@ -1307,62 +1279,61 @@ let rec instantiate_lambda sigma t l =
     instantiate_lambda sigma (subst1 a body) l
 
 let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num :
-    tactic =
- fun g ->
-  let sigma = project g in
-  let ids = Termops.ids_of_named_context (pf_hyps g) in
-  let func_body = def_of_const (constr_of_monomorphic_global func) in
-  let func_body = EConstr.of_constr func_body in
-  let f_name, _, body1 = destLambda sigma func_body in
-  let f_id =
-    match f_name.binder_name with
-    | Name f_id -> next_ident_away_in_goal f_id ids
-    | Anonymous -> anomaly (Pp.str "Anonymous function.")
-  in
-  let n_names_types, _ = decompose_lam_n sigma nb_args body1 in
-  let n_ids, ids =
-    List.fold_left
-      (fun (n_ids, ids) (n_name, _) ->
-        match n_name.binder_name with
-        | Name id ->
-          let n_id = next_ident_away_in_goal id ids in
-          (n_id :: n_ids, n_id :: ids)
-        | _ -> anomaly (Pp.str "anonymous argument."))
-      ([], f_id :: ids)
-      n_names_types
-  in
-  let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
-  let expr =
-    instantiate_lambda sigma func_body (mkVar f_id :: List.map mkVar n_ids)
-  in
-  termination_proof_header is_mes input_type ids n_ids relation rec_arg_num
-    rec_arg_id
-    (fun rec_arg_id hrec acc_id acc_inv g ->
-      (prove_terminate
-         (fun infos -> tclIDTAC)
-         { is_main_branch = true
-         ; (* we are on the main branche (i.e. still on a match ... with .... end *)
-           is_final = true
-         ; (* and on leaf (more or less) *)
-           f_terminate = delayed_force coq_O
-         ; nb_arg = nb_args
-         ; concl_tac
-         ; rec_arg_id
-         ; is_mes
-         ; ih = hrec
-         ; f_id
-         ; f_constr = mkVar f_id
-         ; func
-         ; info = expr
-         ; acc_inv
-         ; acc_id
-         ; values_and_bounds = []
-         ; eqs = []
-         ; forbidden_ids = []
-         ; args_assoc = [] })
-        g)
-    (fun b ids -> Proofview.V82.of_tactic (tclUSER_if_not_mes concl_tac b ids))
-    g
+    unit Proofview.tactic =
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      let hyps = Proofview.Goal.hyps g in
+      let ids = Termops.ids_of_named_context hyps in
+      let func_body = def_of_const (constr_of_monomorphic_global func) in
+      let func_body = EConstr.of_constr func_body in
+      let f_name, _, body1 = destLambda sigma func_body in
+      let f_id =
+        match f_name.binder_name with
+        | Name f_id -> next_ident_away_in_goal f_id ids
+        | Anonymous -> anomaly (Pp.str "Anonymous function.")
+      in
+      let n_names_types, _ = decompose_lam_n sigma nb_args body1 in
+      let n_ids, ids =
+        List.fold_left
+          (fun (n_ids, ids) (n_name, _) ->
+            match n_name.binder_name with
+            | Name id ->
+              let n_id = next_ident_away_in_goal id ids in
+              (n_id :: n_ids, n_id :: ids)
+            | _ -> anomaly (Pp.str "anonymous argument."))
+          ([], f_id :: ids)
+          n_names_types
+      in
+      let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
+      let expr =
+        instantiate_lambda sigma func_body (mkVar f_id :: List.map mkVar n_ids)
+      in
+      termination_proof_header is_mes input_type ids n_ids relation rec_arg_num
+        rec_arg_id
+        (fun rec_arg_id hrec acc_id acc_inv ->
+          prove_terminate
+            (fun infos -> Proofview.tclUNIT ())
+            { is_main_branch = true
+            ; (* we are on the main branche (i.e. still on a match ... with .... end *)
+              is_final = true
+            ; (* and on leaf (more or less) *)
+              f_terminate = delayed_force coq_O
+            ; nb_arg = nb_args
+            ; concl_tac
+            ; rec_arg_id
+            ; is_mes
+            ; ih = hrec
+            ; f_id
+            ; f_constr = mkVar f_id
+            ; func
+            ; info = expr
+            ; acc_inv
+            ; acc_id
+            ; values_and_bounds = []
+            ; eqs = []
+            ; forbidden_ids = []
+            ; args_assoc = [] })
+        (fun b ids -> tclUSER_if_not_mes concl_tac b ids))
 
 let get_current_subgoals_types pstate =
   let p = Declare.Proof.get pstate in
@@ -1397,9 +1368,7 @@ let build_and_l sigma l =
       let c, tac, nb = f pl in
       ( mk_and p1 c
       , tclTHENS
-          (Proofview.V82.of_tactic
-             (apply
-                (EConstr.of_constr (constr_of_monomorphic_global conj_constr))))
+          (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr)))
           [tclIDTAC; tac]
       , nb + 1 )
   in
@@ -1521,29 +1490,23 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
   let lemma = Declare.Proof.start ~cinfo ~info sigma in
   let lemma =
     if Indfun_common.is_strict_tcc () then
-      fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
+      fst @@ Declare.Proof.by tclIDTAC lemma
     else
       fst
       @@ Declare.Proof.by
-           (Proofview.V82.tactic (fun g ->
-                tclTHEN decompose_and_tac
-                  (tclORELSE
-                     (tclFIRST
-                        (List.map
-                           (fun c ->
-                             Proofview.V82.of_tactic
-                               (Tacticals.New.tclTHENLIST
-                                  [ intros
-                                  ; Simple.apply
-                                      (fst
-                                         (interp_constr (Global.env ())
-                                            Evd.empty c))
-                                    (*FIXME*)
-                                  ; Tacticals.New.tclCOMPLETE Auto.default_auto
-                                  ]))
-                           using_lemmas))
-                     tclIDTAC)
-                  g))
+           (tclTHEN decompose_and_tac
+              (tclORELSE
+                 (tclFIRST
+                    (List.map
+                       (fun c ->
+                         Tacticals.New.tclTHENLIST
+                           [ intros
+                           ; Simple.apply
+                               (fst (interp_constr (Global.env ()) Evd.empty c))
+                             (*FIXME*)
+                           ; Tacticals.New.tclCOMPLETE Auto.default_auto ])
+                       using_lemmas))
+                 tclIDTAC))
            lemma
   in
   if Declare.Proof.get_open_goals lemma = 0 then (defined lemma; None)
@@ -1568,11 +1531,10 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
     in
     fst
     @@ Declare.Proof.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)))
+         (New.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 =
@@ -1591,31 +1553,28 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
     if interactive_proof then Some lemma else (defined lemma; None)
 
 let start_equation (f : GlobRef.t) (term_f : GlobRef.t)
-    (cont_tactic : Id.t list -> tactic) g =
-  let sigma = project g in
-  let ids = pf_ids_of_hyps g in
-  let terminate_constr = constr_of_monomorphic_global term_f in
-  let terminate_constr = EConstr.of_constr terminate_constr in
-  let nargs =
-    nb_prod (project g)
-      (EConstr.of_constr (type_of_const sigma terminate_constr))
-  in
-  let x = n_x_id ids nargs in
-  observe_tac
-    (fun _ _ -> str "start_equation")
-    (observe_tclTHENLIST
-       (fun _ _ -> str "start_equation")
-       [ h_intros x
-       ; Proofview.V82.of_tactic
-           (unfold_in_concl
-              [(Locus.AllOccurrences, evaluable_of_global_reference f)])
-       ; observe_tac
-           (fun _ _ -> str "simplest_case")
-           (Proofview.V82.of_tactic
-              (simplest_case
-                 (mkApp (terminate_constr, Array.of_list (List.map mkVar x)))))
-       ; observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x) ])
-    g
+    (cont_tactic : Id.t list -> unit Proofview.tactic) =
+  Proofview.Goal.enter (fun g ->
+      let sigma = Proofview.Goal.sigma g in
+      let ids = Tacmach.New.pf_ids_of_hyps g in
+      let terminate_constr = constr_of_monomorphic_global term_f in
+      let terminate_constr = EConstr.of_constr terminate_constr in
+      let nargs =
+        nb_prod sigma (EConstr.of_constr (type_of_const sigma terminate_constr))
+      in
+      let x = n_x_id ids nargs in
+      New.observe_tac
+        (fun _ _ -> str "start_equation")
+        (New.observe_tclTHENLIST
+           (fun _ _ -> str "start_equation")
+           [ h_intros x
+           ; unfold_in_concl
+               [(Locus.AllOccurrences, evaluable_of_global_reference f)]
+           ; New.observe_tac
+               (fun _ _ -> str "simplest_case")
+               (simplest_case
+                  (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))
+           ; New.observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x) ]))
 
 let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
     equation_lemma_type =
@@ -1638,35 +1597,34 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let lemma =
     fst
     @@ Declare.Proof.by
-         (Proofview.V82.tactic
-            (start_equation f_ref terminate_ref (fun x ->
-                 prove_eq
-                   (fun _ -> tclIDTAC)
-                   { nb_arg
-                   ; f_terminate =
-                       EConstr.of_constr
-                         (constr_of_monomorphic_global terminate_ref)
-                   ; f_constr = EConstr.of_constr f_constr
-                   ; 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)))
-                         (EConstr.of_constr f_constr :: List.map mkVar x)
-                   ; is_main_branch = true
-                   ; is_final = true
-                   ; values_and_bounds = []
-                   ; eqs = []
-                   ; forbidden_ids = []
-                   ; acc_inv = lazy (assert false)
-                   ; acc_id = Id.of_string "____"
-                   ; args_assoc = []
-                   ; f_id = Id.of_string "______"
-                   ; rec_arg_id = Id.of_string "______"
-                   ; is_mes = false
-                   ; ih = Id.of_string "______" })))
+         (start_equation f_ref terminate_ref (fun x ->
+              prove_eq
+                (fun _ -> Proofview.tclUNIT ())
+                { nb_arg
+                ; f_terminate =
+                    EConstr.of_constr
+                      (constr_of_monomorphic_global terminate_ref)
+                ; f_constr = EConstr.of_constr f_constr
+                ; 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)))
+                      (EConstr.of_constr f_constr :: List.map mkVar x)
+                ; is_main_branch = true
+                ; is_final = true
+                ; values_and_bounds = []
+                ; eqs = []
+                ; forbidden_ids = []
+                ; acc_inv = lazy (assert false)
+                ; acc_id = Id.of_string "____"
+                ; args_assoc = []
+                ; f_id = Id.of_string "______"
+                ; rec_arg_id = Id.of_string "______"
+                ; is_mes = false
+                ; ih = Id.of_string "______" }))
          lemma
   in
   let _ =