From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 15 Dec 2016 10:45:19 +0100
Subject: Removing most nf_enter in tactics.

Now they are useless because all of the primitives are (should?) be
evar-insensitive.
---
 ltac/extratactics.ml4      |  24 ++++----
 ltac/g_class.ml4           |   6 +-
 ltac/rewrite.ml            |   8 +--
 ltac/tacinterp.ml          |  30 +++++-----
 plugins/cc/cctac.ml        |  44 +++++++-------
 plugins/omega/coq_omega.ml |  35 +++++++-----
 proofs/clenv.ml            |  17 ++++--
 proofs/clenv.mli           |  11 ++--
 proofs/clenvtac.ml         |   4 +-
 tactics/auto.ml            |  16 +++---
 tactics/autorewrite.ml     |   2 +-
 tactics/class_tactics.ml   |  42 +++++++-------
 tactics/class_tactics.mli  |   2 +-
 tactics/contradiction.ml   |   2 +-
 tactics/eauto.ml           |  17 +++---
 tactics/elim.ml            |   4 +-
 tactics/eqdecide.ml        |   4 +-
 tactics/equality.ml        |  24 ++++----
 tactics/inv.ml             |  14 ++---
 tactics/leminv.ml          |   5 +-
 tactics/tacticals.ml       | 140 ++++++++++++++++++++++-----------------------
 tactics/tacticals.mli      |   5 +-
 tactics/tactics.ml         | 107 ++++++++++++++++++----------------
 tactics/tactics.mli        |   4 +-
 toplevel/auto_ind_decl.ml  |  32 +++++------
 25 files changed, 305 insertions(+), 294 deletions(-)

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 58c5823c5..e9d91fe47 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -354,7 +354,7 @@ let constr_flags = {
   Pretyping.expand_evars = true }
 
 let refine_tac ist simple c =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags = constr_flags in
@@ -645,7 +645,7 @@ let subst_hole_with_term occ tc t =
 open Tacmach
 
 let hResolve id c occ t =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
@@ -708,7 +708,7 @@ END
 exception Found of unit Proofview.tactic
 
 let rewrite_except h =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
   Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else 
       Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
@@ -727,11 +727,11 @@ let refl_equal =
   should be replaced by a call to the tactic but I don't know how to
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
        Tacticals.New.tclTHENLIST
          [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
-          Proofview.Goal.nf_enter { enter = begin fun gl ->
+          Proofview.Goal.enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
@@ -743,16 +743,16 @@ let  mkCaseEq a  : unit Proofview.tactic =
 
 
 let case_eq_intros_rewrite x =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in
   (* Pp.msgnl (Printer.pr_lconstr x); *)
   Tacticals.New.tclTHENLIST [
       mkCaseEq x;
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let hyps = Tacmach.New.pf_ids_of_hyps gl in
       let n' = nb_prod (Tacmach.New.project gl) concl in
-      let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in
+      let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl)  in
       Tacticals.New.tclTHENLIST [
                     Tacticals.New.tclDO (n'-n-1) intro;
 		    introduction h;
@@ -783,15 +783,15 @@ let destauto t =
   with Found tac -> tac
 
 let destauto_in id = 
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
   end }
 
 TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
+| [ "destauto" ] -> [ Proofview.Goal.enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index b7f0881f1..f47c03dfc 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -74,7 +74,7 @@ TACTIC EXTEND is_ground
 END
 
 TACTIC EXTEND autoapply
-  [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ]
+  [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ]
 END
 
 (** TODO: DEPRECATE *)
@@ -90,10 +90,10 @@ let rec eq_constr_mod_evars sigma x y =
   | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y
 
 let progress_evars t =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let check =
-      Proofview.Goal.nf_enter { enter = begin fun gl' ->
+      Proofview.Goal.enter { enter = begin fun gl' ->
         let sigma = Tacmach.New.project gl' in
         let newconcl = Proofview.Goal.concl gl' in
         if eq_constr_mod_evars sigma concl newconcl
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index bc57fcf56..810f02c4f 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1543,7 +1543,7 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with
     insert_dependent env sigma decl (ndecl :: accu) rem
 
 let assert_replacing id newt tac = 
-  let prf = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let prf = Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
@@ -1611,7 +1611,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             Proofview.Unsafe.tclEVARS undef <*>
             convert_concl_no_check newt DEFAULTcast
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
@@ -2095,7 +2095,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
   let unify env evars t = unify_abs res l2r sort env evars t in
   let app = apply_rule unify occs in
@@ -2129,7 +2129,7 @@ let not_declared env sigma ty rel =
      str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
 let setoid_proof ty fn fallback =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 62d0cc529..167501de2 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -844,10 +844,10 @@ let rec message_of_value v =
     Ftactic.return (str "<tactic>")
   else if has_type v (topwit wit_constr) then
     let v = out_gen (topwit wit_constr) v in
-    Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end }
+    Ftactic.enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end }
   else if has_type v (topwit wit_constr_under_binders) then
     let c = out_gen (topwit wit_constr_under_binders) v in
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
       Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
     end }
   else if has_type v (topwit wit_unit) then
@@ -860,21 +860,21 @@ let rec message_of_value v =
       let (c, sigma) = Tactics.run_delayed env sigma c in
       pr_econstr_env env sigma c
     in
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
       Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
     end }
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
-    Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end }
+    Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end }
   else if has_type v (topwit wit_uconstr) then
     let c = out_gen (topwit wit_uconstr) v in
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
       Ftactic.return (pr_closed_glob_env (pf_env gl)
                         (project gl) c)
     end }
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
-    Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
+    Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
   else match Value.to_list v with
   | Some l ->
     Ftactic.List.map message_of_value l >>= fun l ->
@@ -1213,7 +1213,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
            tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
          end
   | TacAbstract (tac,ido) ->
-      Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT
+      Proofview.Goal.enter { enter = begin fun gl -> Tactics.tclABSTRACT
         (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
       end }
   | TacThen (t1,t) ->
@@ -1521,7 +1521,7 @@ and interp_match ist lz constr lmr =
 
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr =
-    Ftactic.nf_enter { enter = begin fun gl ->
+    Ftactic.enter { enter = begin fun gl ->
       let sigma = project gl in
       let env = Proofview.Goal.env gl in
       let hyps = Proofview.Goal.hyps gl in
@@ -1750,8 +1750,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (Tactics.generalize_gen cl)) sigma
       end }
   | TacLetTac (na,c,clp,b,eqpat) ->
-      Proofview.V82.nf_evar_goals <*>
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let clp = interp_clause ist env sigma clp in
@@ -1788,7 +1787,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacInductionDestruct (isrec,ev,(l,el)) ->
       (* spiwack: some unknown part of destruct needs the goal to be
          prenormalised. *)
-      Proofview.V82.nf_evar_goals <*>
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
@@ -1824,8 +1822,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacChange (None,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
-      Proofview.V82.nf_evar_goals <*>
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
         let is_onhyps = match cl.onhyps with
           | None | Some [] -> true
           | _ -> false
@@ -1854,7 +1851,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacChange (Some op,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
-      Proofview.V82.nf_evar_goals <*>
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
@@ -1899,7 +1895,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
                 by))
       end }
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let (sigma,c_interp) =
@@ -2050,7 +2046,7 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
   Sigma.Unsafe.of_pair (c, sigma)
   }
 
-let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl ->
+let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl ->
   Ftactic.return (interp_destruction_arg ist gl c)
 end }
 
@@ -2080,7 +2076,7 @@ let () =
   register_interp0 wit_ltac interp
 
 let () =
-  register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
+  register_interp0 wit_uconstr (fun ist c -> Ftactic.enter { enter = begin fun gl ->
     Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c)
   end })
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5d894c677..c9c904e35 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -182,9 +182,10 @@ let litteral_of_constr env sigma term=
 (* store all equalities from the context *)
 
 let make_prb gls depth additionnal_terms =
+  let open Tacmach.New in
   let env=pf_env gls in
-  let sigma=sig_sig gls in
-  let state = empty depth gls in
+  let sigma=project gls in
+  let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in
   let pos_hyps = ref [] in
   let neg_hyps =ref [] in
     List.iter
@@ -196,7 +197,7 @@ let make_prb gls depth additionnal_terms =
          let id = NamedDecl.get_id decl in
 	 begin
 	   let cid=Constr.mkVar id in
-	   match litteral_of_constr env sigma (EConstr.of_constr (NamedDecl.get_type decl)) with
+	   match litteral_of_constr env sigma (NamedDecl.get_type decl) with
 	       `Eq (t,a,b) -> add_equality state cid a b
 	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
 	     | `Other ph ->
@@ -213,7 +214,7 @@ let make_prb gls depth additionnal_terms =
 		 neg_hyps:=(cid,nh):: !neg_hyps
 	     | `Rule patts -> add_quant state id true patts
 	     | `Nrule patts -> add_quant state id false patts
-	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
+	 end) (Proofview.Goal.hyps gls);
     begin
       match atom_of_constr env sigma (pf_concl gls) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
@@ -227,6 +228,7 @@ let make_prb gls depth additionnal_terms =
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
 let build_projection intype (cstr:pconstructor) special default gls=
+  let open Tacmach.New in
   let ci= (snd(fst cstr)) in
   let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
@@ -266,7 +268,7 @@ let refresh_universes ty k =
 let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
@@ -296,7 +298,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	refresh_universes (type_of tf1) (fun typf ->
 	refresh_universes (type_of tx1) (fun typx ->
 	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
-        let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
+        let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
 	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
@@ -322,7 +324,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
          let proj =
-           Tacmach.New.of_old (build_projection intype cstr special default) gl
+           build_projection intype cstr special default gl
          in
 	 let injt=
            app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
@@ -331,9 +333,9 @@ let rec proof_tac p : unit Proofview.tactic =
   end }
 
 let refute_tac c t1 t2 p =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
+  let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
   let k intype =
     let neweq= new_app_global _eq [|intype;tt1;tt2|] in
@@ -347,12 +349,12 @@ let refine_exact_check c gl =
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let k sort =
     let neweq= new_app_global _eq [|sort;tt1;tt2|] in
-    let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
-    let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
+    let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
     let identity=mkLambda (Name x,sort,mkRel 1) in
     let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
@@ -361,9 +363,9 @@ let convert_to_goal_tac c t1 t2 p =
   end }
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let tt2=constr_of_term t2 in
-  let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
+  let h = Tacmach.New.pf_get_new_id (Id.of_string "H") gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
@@ -371,11 +373,11 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
   end }
 
 let discriminate_tac (cstr,u as cstru) p =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
     let identity = Universes.constr_of_global (Lazy.force _I) in
     let identity = EConstr.of_constr identity in
     let trivial = Universes.constr_of_global (Lazy.force _True) in
@@ -385,8 +387,8 @@ let discriminate_tac (cstr,u as cstru) p =
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
-    let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
-    let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
+    let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
+    let proj = build_projection intype cstru trivial concl gl in
     let injt=app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
@@ -409,11 +411,11 @@ let build_term_to_complete uf meta pac =
     applist (mkConstructU cinfo.ci_constr, all_args)
 
 let cc_tactic depth additionnal_terms =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library Coqlib.logic_module_name;
     let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
-    let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
+    let state = make_prb gl depth additionnal_terms in
     let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
     let sol = execute true state in
     let _ = debug (fun () -> Pp.str "Computation completed.") in
@@ -498,7 +500,7 @@ let mk_eq f c1 c2 k =
     end })
 
 let f_equal =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let cut_eq c1 c2 =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 72aeb9066..adf926958 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -38,7 +38,7 @@ open OmegaSolver
 (* Added by JCF, 09/03/98 *)
 
 let elim_id id =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     simplest_elim (Tacmach.New.pf_global id gl)
   end }
 let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
@@ -1391,7 +1391,10 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
   else
     (tactic,defs)
 
+let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
+
 let destructure_omega gl tac_def (id,c) =
+  let open Tacmach.New in
   let sigma = project gl in
   if String.equal (atompart_of_id id) "State" then
     tac_def
@@ -1433,10 +1436,10 @@ let reintroduce id =
 open Proofview.Notations
 
 let coq_omega =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
-  let destructure_omega = Tacmach.New.of_old destructure_omega gl in
+  let destructure_omega = destructure_omega gl in
   let tactic_normalisation, system =
     List.fold_left destructure_omega ([],[]) hyps_types in
   let prelude,sys =
@@ -1486,7 +1489,7 @@ let coq_omega =
 let coq_omega = coq_omega
 
 let nat_inject =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
   let rec explore p t : unit Proofview.tactic =
     Proofview.tclEVARMAP >>= fun sigma ->
@@ -1657,6 +1660,7 @@ let not_binop = function
 exception Undecidable
 
 let rec decidability gl t =
+  let open Tacmach.New in
   match destructurate_prop (project gl) t with
     | Kapp(Or,[t1;t2]) ->
 	mkApp (Lazy.force coq_dec_or, [| t1; t2;
@@ -1687,22 +1691,25 @@ let rec decidability gl t =
     | Kapp(True,[]) -> Lazy.force coq_dec_True
     | _ -> raise Undecidable
 
+let fresh_id avoid id gl =
+  fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
 let onClearedName id tac =
   (* We cannot ensure that hyps can be cleared (because of dependencies), *)
   (* so renaming may be necessary *)
   Tacticals.New.tclTHEN
     (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
-     let id = Tacmach.New.of_old (fresh_id [] id) gl in
+    (Proofview.Goal.enter { enter = begin fun gl ->
+     let id = fresh_id [] id gl in
      Tacticals.New.tclTHEN (introduction id) (tac id)
     end })
 
 let onClearedName2 id tac =
   Tacticals.New.tclTHEN
     (Tacticals.New.tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
-     let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
-     let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
+    (Proofview.Goal.enter { enter = begin fun gl ->
+     let id1 = fresh_id [] (add_suffix id "_left") gl in
+     let id2 = fresh_id [] (add_suffix id "_right") gl in
       Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
     end })
 
@@ -1712,10 +1719,10 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
   | _ -> false
 
 let destructure_hyps =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = Tacmach.New.pf_unsafe_type_of gl in
-  let decidability = Tacmach.New.of_old decidability gl in
-  let pf_nf = Tacmach.New.of_old pf_nf gl in
+  let decidability = decidability gl in
+  let pf_nf = pf_nf gl in
     let rec loop = function
       | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
       | decl::lit ->
@@ -1854,9 +1861,9 @@ let destructure_hyps =
   end }
 
 let destructure_goal =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let decidability = Tacmach.New.of_old decidability gl in
+    let decidability = decidability gl in
     let rec loop t =
       Proofview.tclEVARMAP >>= fun sigma ->
       let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5645850b2..f9ebc4233 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -129,11 +129,13 @@ let mk_clenv_from_env env sigma n (c,cty) =
     env = env }
 
 let mk_clenv_from_n gls n (c,cty) =
-  mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+  let env = Proofview.Goal.env gls in
+  let sigma = Tacmach.New.project gls in
+  mk_clenv_from_env env sigma n (c, cty)
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
 
 (******************************************************************)
 
@@ -263,8 +265,7 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
-  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
   if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
@@ -272,6 +273,14 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
+let old_clenv_unique_resolver ?flags clenv gl =
+  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  clenv_unique_resolver_gen ?flags clenv concl
+
+let clenv_unique_resolver ?flags clenv gl =
+  let concl = Proofview.Goal.concl gl in
+  clenv_unique_resolver_gen ?flags clenv concl
+
 let adjust_meta_source evd mv = function
   | loc,Evar_kinds.VarInstance id ->
     let rec match_name c l =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f7ff4bed3..4bcd50591 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -41,10 +41,10 @@ val clenv_nf_meta   : clausenv -> EConstr.constr -> EConstr.constr
 (** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
-val mk_clenv_from : Goal.goal sigma -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
-  Goal.goal sigma -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : Goal.goal sigma -> EConstr.constr -> clausenv
+  ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
 (** Refresh the universes in a clenv *)
@@ -62,9 +62,12 @@ val clenv_unify :
   ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (** unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
+val old_clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
+val clenv_unique_resolver :
+  ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv
+
 val clenv_dependent : clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 32c887ff5..0722ea047 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -105,8 +105,8 @@ let dft = default_unify_flags
 
 let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
   Proofview.Goal.enter { enter = begin fun gl ->
-    let clenv gl = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
+    let clenv = clenv_unique_resolver ~flags clenv gl in
+    clenv_refine with_evars ~with_classes clenv
   end }
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b548f8b92..c8c119aee 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -101,9 +101,9 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
   in clenv, c
 
 let unify_resolve poly flags ((c : raw_hint), clenv) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
-  let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
+  let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine false clenv
   end }
 
@@ -330,7 +330,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
       end })
   in
   Proofview.Goal.enter { enter = begin fun gl ->
-    let concl = Tacmach.New.pf_nf_concl gl in
+    let concl = Tacmach.New.pf_concl gl in
     let sigma = Tacmach.New.project gl in
     let secvars = compute_secvars gl in
     Tacticals.New.tclFIRST
@@ -421,7 +421,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
     "nocore" amongst the databases. *)
 
 let trivial ?(debug=Off) lems dbnames =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
@@ -432,7 +432,7 @@ let trivial ?(debug=Off) lems dbnames =
   end }
 
 let full_trivial ?(debug=Off) lems =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
@@ -490,7 +490,7 @@ let search d n mod_delta db_list local_db =
         Tacticals.New.tclORELSE0 (dbg_assumption d)
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter { enter = begin fun gl ->
-               let concl = Tacmach.New.pf_nf_concl gl in
+               let concl = Tacmach.New.pf_concl gl in
                let sigma = Tacmach.New.project gl in
                let secvars = compute_secvars gl in
 	       let d' = incr_dbg d in
@@ -506,7 +506,7 @@ let search d n mod_delta db_list local_db =
 let default_search_depth = ref 5
 
 let delta_auto debug mod_delta n lems dbnames =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
@@ -529,7 +529,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n
 let default_auto = auto !default_search_depth [] []
 
 let delta_full_auto ?(debug=Off) mod_delta n lems =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index f43f4b250..e58ec5a31 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -92,7 +92,7 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.
 let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = find_rewrites bas in
   let try_rewrite dir ctx c tc =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
     let c' = Vars.subst_univs_level_constr subst c in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 669d80814..8ada9e6a7 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -231,13 +231,13 @@ let e_give_exact flags poly (c,clenv) gl =
 
 let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
-  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
     Clenvtac.clenv_refine true ~with_classes:false clenv'
   end }
 
 let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
   let clenv', _ = connect_hint_clenv poly c clenv gls in
-  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
     Clenvtac.clenv_refine false ~with_classes:false clenv'
   end }
 
@@ -285,16 +285,16 @@ let clenv_of_prods poly nprods (c, clenv) gl =
     if Pervasives.(>=) diff 0 then
       (* Was Some clenv... *)
       Some (Some diff,
-            Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
+            mk_clenv_from_n gl (Some diff) (c,ty))
     else None
 
 let with_prods nprods poly (c, clenv) f =
   if get_typeclasses_limit_intros () then
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
      match clenv_of_prods poly nprods (c, clenv) gl with
      | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
      | Some (diff, clenv') -> f.enter gl (c, diff, clenv') end }
-  else Proofview.Goal.nf_enter
+  else Proofview.Goal.enter
          { enter = begin fun gl ->
                    if Int.equal nprods 0 then f.enter gl (c, None, clenv)
                    else Tacticals.New.tclZEROMSG (str"Not enough premisses") end }
@@ -345,7 +345,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
   let open Tacticals.New in
   let open Tacmach.New in
   let trivial_fail =
-    Proofview.Goal.nf_enter { enter =
+    Proofview.Goal.enter { enter =
     begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
@@ -356,7 +356,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
       end }
   in
   let trivial_resolve =
-    Proofview.Goal.nf_enter { enter =
+    Proofview.Goal.enter { enter =
     begin fun gl ->
     let tacs = e_trivial_resolve db_list local_db secvars only_classes
                                  (project gl) (pf_concl gl) in
@@ -944,7 +944,7 @@ module Search = struct
              Hint_db.transparent_state cached_hints == st
     then cached_hints
     else
-      let hints = make_hints {it = Goal.goal g; sigma = project g}
+      let hints = make_hints {it = Goal.goal (Proofview.Goal.assume g); sigma = project g}
                              st only_classes sign
       in
       autogoal_cache := (cwd, only_classes, sign, hints); hints
@@ -1024,16 +1024,16 @@ module Search = struct
            (pr_depth (!idx :: info.search_depth) ++ str": trying " ++
               Lazy.force pp ++
               (if !foundone != true then
-                 str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
+                 str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
                else mt ())));
-      let tac_of gls i j = Goal.nf_enter { enter = fun gl' ->
+      let tac_of gls i j = Goal.enter { enter = fun gl' ->
         let sigma' = Goal.sigma gl' in
         let s' = Sigma.to_evar_map sigma' in
         let _concl = Goal.concl gl' in
         if !typeclasses_debug > 0 then
           Feedback.msg_debug
             (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
-               pr_ev s' (Proofview.Goal.goal gl'));
+               pr_ev s' (Proofview.Goal.goal (Proofview.Goal.assume gl')));
         let eq c1 c2 = EConstr.eq_constr s' c1 c2 in
         let hints' =
           if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
@@ -1042,7 +1042,7 @@ module Search = struct
             make_autogoal_hints info.search_only_classes ~st gl'
           else info.search_hints
         in
-        let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal gl') gls in
+        let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal (Proofview.Goal.assume gl')) gls in
         let info' =
           { search_depth = succ j :: i :: info.search_depth;
             last_tac = pp;
@@ -1059,7 +1059,7 @@ module Search = struct
         (if !typeclasses_debug > 0 then
            Feedback.msg_debug
              (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp
-              ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
+              ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
               ++ str", " ++ int j ++ str" subgoal(s)" ++
                 (Option.cata (fun k -> str " in addition to the first " ++ int k)
                              (mt()) k)));
@@ -1130,7 +1130,7 @@ module Search = struct
     else tclONCE (aux (NotApplicableEx,Exninfo.null) poss)
 
   let hints_tac hints info kont : unit Proofview.tactic =
-    Proofview.Goal.nf_enter
+    Proofview.Goal.enter
       { enter = fun gl -> hints_tac_gl hints info kont gl }
 
   let intro_tac info kont gl =
@@ -1150,7 +1150,7 @@ module Search = struct
 
   let intro info kont =
     Proofview.tclBIND Tactics.intro
-     (fun _ -> Proofview.Goal.nf_enter { enter = fun gl -> intro_tac info kont gl })
+     (fun _ -> Proofview.Goal.enter { enter = fun gl -> intro_tac info kont gl })
 
   let rec search_tac hints limit depth =
     let kont info =
@@ -1173,7 +1173,7 @@ module Search = struct
         unit Proofview.tactic =
     let open Proofview in
     let open Proofview.Notations in
-    let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+    let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in
     let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
     search_tac hints depth 1 info
 
@@ -1510,11 +1510,11 @@ let is_ground c gl =
   if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
   else tclFAIL 0 (str"Not ground") gl
 
-let autoapply c i gl =
+let autoapply c i = Proofview.Goal.enter { enter = begin fun gl ->
   let flags = auto_unif_flags Evar.Set.empty
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
-  let cty = pf_unsafe_type_of gl c in
+  let cty = Tacmach.New.pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
-    ((c,cty,Univ.ContextSet.empty),0,ce) } in
-  Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
+  (unify_e_resolve false flags).enter gl
+    ((c,cty,Univ.ContextSet.empty),0,ce)
+end }
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 171b5c4ea..8855093ee 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -31,7 +31,7 @@ val not_evar : constr -> unit Proofview.tactic
 
 val is_ground : constr -> tactic
 
-val autoapply : constr -> Hints.hint_db_name -> tactic
+val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
 
 module Search : sig
   val eauto_tac :
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 0e28aa980..63f923dfd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -110,7 +110,7 @@ let is_negation_of env sigma typ t =
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7453fff5c..14082bb8d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -112,13 +112,12 @@ open Auto
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
-      Proofview.V82.tactic
-	(fun gls ->
-	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
-	 tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+      let clenv' = clenv_unique_resolver ~flags clenv' gl in
+      Proofview.tclTHEN
+        (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+        (Tactics.Simple.eapply c)
     end }
 
 let hintmap_of sigma secvars hdc concl =
@@ -139,7 +138,7 @@ let e_exact poly flags (c,clenv) =
   end }
 
 let rec e_trivial_fail_db db_list local_db =
-  let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let next = Proofview.Goal.enter { enter = begin fun gl ->
     let d = Tacmach.New.pf_last_hyp gl in
     let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
     e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
@@ -149,7 +148,7 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
@@ -501,7 +500,7 @@ let unfold_head env sigma (ids, csts) c =
   in aux c
 
 let autounfold_one db cl =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index a4158f821..e37ec6bce 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -133,7 +133,7 @@ let induction_trailer abs_i abs_j bargs =
     (tclDO (abs_j - abs_i) intro)
     (onLastHypId
        (fun id ->
-          Proofview.Goal.nf_enter { enter = begin fun gl ->
+          Proofview.Goal.enter { enter = begin fun gl ->
 	  let idty = pf_unsafe_type_of gl (mkVar id) in
 	  let fvty = global_vars (pf_env gl) (project gl) idty in
 	  let possible_bring_hyps =
@@ -155,7 +155,7 @@ let induction_trailer abs_i abs_j bargs =
           ))
 
 let double_ind h1 h2 =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let abs_i = depth_of_quantified_hypothesis true h1 gl in
   let abs_j = depth_of_quantified_hypothesis true h2 gl in
   let abs =
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index df60f2c66..bac3980d2 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -176,7 +176,7 @@ let solveEqBranch rectype =
   Proofview.tclORELSE
     begin
       Proofview.Goal.enter { enter = begin fun gl ->
-        let concl = pf_nf_concl gl in
+        let concl = pf_concl gl in
         let sigma = project gl in
         match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) ->
           let (mib,mip) = Global.lookup_inductive rectype in
@@ -202,7 +202,7 @@ let decideGralEquality =
   Proofview.tclORELSE
     begin
       Proofview.Goal.enter { enter = begin fun gl ->
-        let concl = pf_nf_concl gl in
+        let concl = pf_concl gl in
         let sigma = project gl in
         match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) ->
         let headtyp = hd_app sigma (pf_compute gl typ) in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d9b668517..6fcf529c2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -306,7 +306,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
       else instantiate_lemma_all frzevars gl c t l l2r concl
     in
     let typ = match cls with
-    | None -> pf_nf_concl gl
+    | None -> pf_concl gl
     | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
     in
     let cs = instantiate_lemma typ in
@@ -406,7 +406,7 @@ let type_of_clause cls gl = match cls with
   | Some id -> pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let isatomic = isProd evd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
@@ -1009,7 +1009,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     match find_positions env sigma t1 t2 with
     | Inr _ ->
@@ -1019,7 +1019,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   end }
 
 let onEquality with_evars tac (c,lbindc) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
@@ -1034,7 +1034,7 @@ let onEquality with_evars tac (c,lbindc) =
   end }
 
 let onNegatedEquality with_evars tac =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -1302,7 +1302,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let inject_if_homogenous_dependent_pair ty =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   try
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
@@ -1458,7 +1458,7 @@ let injConcl = injClause None false None
 let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
       match find_positions env sigma t1 t2 with
@@ -1567,7 +1567,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1586,7 +1586,7 @@ let cutSubstInConcl l2r eqn =
   end }
 
 let cutSubstInHyp l2r eqn id =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1812,7 +1812,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
           Proofview.tclUNIT ()
     end }
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let ids = find_equations gl in
     tclMAP process ids
   end }
@@ -1822,7 +1822,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 (* Old implementation, not able to manage configurations like a=b, a=t,
    or situations like "a = S b, b = S a", or also accidentally unfolding
    let-ins *)
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
@@ -1877,7 +1877,7 @@ let rewrite_assumption_cond cond_eq_term cl =
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
     let hyps = Proofview.Goal.hyps gl in
     arec hyps gl
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 632a29721..904a17417 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -273,7 +273,7 @@ Nota: with Inversion_clear, only four useless hypotheses
 
 let generalizeRewriteIntros as_mode tac depids id =
   Proofview.tclENV >>= fun env ->
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let dids = dependent_hyps env id depids gl in
   let reintros = if as_mode then intros_replacing else intros_possibly_replacing in
   (tclTHENLIST
@@ -342,7 +342,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = project gl in
     (** We only look at the type of hypothesis "id" *)
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
@@ -378,7 +378,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
     id
 
 let nLastDecls i tac =
-  Proofview.Goal.nf_enter { enter = begin fun gl -> tac (nLastDecls gl i) end }
+  Proofview.Goal.enter { enter = begin fun gl -> tac (nLastDecls gl i) end }
 
 (* Introduction of the equations on arguments
    othin: discriminates Simple Inversion, Inversion and Inversion_clear
@@ -386,7 +386,7 @@ let nLastDecls i tac =
      Some thin: the equations are rewritten, and cleared if thin is true *)
 
 let rewrite_equations as_mode othin neqns names ba =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
   let first_eq = ref MoveLast in
   let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in
@@ -436,7 +436,7 @@ let rewrite_equations_tac as_mode othin id neqns names ba =
     tac
 
 let raw_inversion inv_kind id status names =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let sigma = Sigma.to_evar_map sigma in
     let env = Proofview.Goal.env gl in
@@ -517,14 +517,14 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
  * back to their places in the hyp-list. *)
 
 let invIn k names ids id =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
     let nb_prod_init = nb_prod sigma concl in
     let intros_replace_ids =
       Proofview.Goal.enter { enter = begin fun gl ->
-        let concl = pf_nf_concl gl in
+        let concl = pf_concl gl in
         let sigma = project gl in
         let nb_of_new_hyp =
           nb_prod sigma concl - (List.length hyps + nb_prod_init)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d864e547c..daa962f1d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -262,7 +262,8 @@ let add_inversion_lemma_exn na com comsort bool tac =
 
 let lemInv id c gls =
   try
-    let clause = mk_clenv_type_of gls c in
+    let open Tacmach in
+    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
@@ -277,7 +278,7 @@ let lemInv id c gls =
 let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
 
 let lemInvIn id c ids =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let intros_replace_ids =
       let concl = Proofview.Goal.concl gl in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 94f22f903..27c1987a0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -267,40 +267,6 @@ let pf_with_evars glsev k gls =
 let pf_constr_of_global gr k =
   pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
 
-(* computing the case/elim combinators *)
-
-let gl_make_elim ind gl =
-  let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
-  let (sigma, c) = pf_apply Evd.fresh_global gl gr in
-  (sigma, EConstr.of_constr c)
-
-let gl_make_case_dep ind gl =
-  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
-  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
-    (elimination_sort_of_goal gl)
-  in
-  (Sigma.to_evar_map sigma, EConstr.of_constr r)
-
-let gl_make_case_nodep ind gl =
-  let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
-  let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
-    (elimination_sort_of_goal gl)
-  in
-  (Sigma.to_evar_map sigma, EConstr.of_constr r)
-
-let make_elim_branch_assumptions ba gl =
-  let assums =
-    try List.rev (List.firstn ba.nassums (pf_hyps gl))
-    with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
-  { ba = ba; assums = assums }
-
-let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
-
-let make_case_branch_assumptions = make_elim_branch_assumptions
-
-let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
-
-
 (** Tacticals of Ltac defined directly in term of Proofview *)
 module New = struct
   open Proofview
@@ -534,7 +500,7 @@ module New = struct
         Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
   let tclDELAYEDWITHHOLES check x tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
       let Sigma (x, sigma, _) = x.delayed env sigma in
@@ -578,13 +544,13 @@ module New = struct
   let onLastHyp   = onNthHyp 1
 
   let onNthDecl m tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       Proofview.tclUNIT (nthDecl m gl) >>= tac
     end }
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
     if pred (id,typ) then
       tac1 id
@@ -592,7 +558,7 @@ module New = struct
       tac2 id
     end }
 
-  let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
+  let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end }
 
   let afterHyp id tac =
     Proofview.Goal.enter { enter = begin fun gl ->
@@ -625,13 +591,13 @@ module New = struct
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
       isrec allnames tac predicate ind (c, t) =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let sigma, elim = (mk_elim ind).enter gl in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
+    (Proofview.Goal.enter { enter = begin fun gl ->
+    let indclause = mk_clenv_from gl (c, t) in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
+    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim)  in
     let indmv =
       match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
@@ -660,7 +626,7 @@ module New = struct
       | None   -> elimclause'
       | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
     in
-    let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
+    let clenv' = clenv_unique_resolver ~flags elimclause' gl in
     let after_tac i =
       let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in
       let ba = { branchsign = branchsigns.(i);
@@ -679,8 +645,64 @@ module New = struct
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end }) end }
 
+  let elimination_sort_of_goal gl =
+    (** Retyping will expand evars anyway. *)
+    let c = Proofview.Goal.concl (Goal.assume gl) in
+    pf_apply Retyping.get_sort_family_of gl c
+
+  let elimination_sort_of_hyp id gl =
+    (** Retyping will expand evars anyway. *)
+    let c = pf_get_hyp_typ id (Goal.assume gl) in
+    pf_apply Retyping.get_sort_family_of gl c
+
+  let elimination_sort_of_clause id gl = match id with
+  | None -> elimination_sort_of_goal gl
+  | Some id -> elimination_sort_of_hyp id gl
+
+  (* computing the case/elim combinators *)
+
+  let gl_make_elim ind = { enter = begin fun gl ->
+    let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
+    let (sigma, c) = pf_apply Evd.fresh_global gl gr in
+    (sigma, EConstr.of_constr c)
+  end }
+
+  let gl_make_case_dep ind = { enter = begin fun gl ->
+    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
+      (elimination_sort_of_goal gl)
+    in
+    (Sigma.to_evar_map sigma, EConstr.of_constr r)
+  end }
+
+  let gl_make_case_nodep ind = { enter = begin fun gl ->
+    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
+      (elimination_sort_of_goal gl)
+    in
+    (Sigma.to_evar_map sigma, EConstr.of_constr r)
+  end }
+
+  let make_elim_branch_assumptions ba hyps =
+    let assums =
+      try List.rev (List.firstn ba.nassums hyps)
+      with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
+    { ba = ba; assums = assums }
+
+  let elim_on_ba tac ba =
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+    tac branches
+    end }
+
+  let case_on_ba tac ba = 
+    Proofview.Goal.enter { enter = begin fun gl ->
+    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+    tac branches
+    end }
+
   let elimination_then tac c =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
     let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
@@ -696,34 +718,8 @@ module New = struct
   let case_nodep_then_using =
     general_elim_then_using gl_make_case_nodep false
 
-  let elim_on_ba tac ba =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
-    tac branches
-    end }
-
-  let case_on_ba tac ba = 
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
-    tac branches
-    end }
-
-  let elimination_sort_of_goal gl =
-    (** Retyping will expand evars anyway. *)
-    let c = Proofview.Goal.concl (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
-
-  let elimination_sort_of_hyp id gl =
-    (** Retyping will expand evars anyway. *)
-    let c = pf_get_hyp_typ id (Goal.assume gl) in
-    pf_apply Retyping.get_sort_family_of gl c
-
-  let elimination_sort_of_clause id gl = match id with
-  | None -> elimination_sort_of_goal gl
-  | Some id -> elimination_sort_of_hyp id gl
-
   let pf_constr_of_global ref tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Tacmach.New.project gl in
       let (sigma, c) = Evd.fresh_global env sigma ref in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4bb745875..c9ff77716 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -137,9 +137,6 @@ val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family
 val pf_with_evars :  (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
 val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
 
-val elim_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
-val case_on_ba : (branch_assumptions -> tactic) -> branch_args  -> tactic
-
 (** Tacticals defined directly in term of Proofview *)
 
 (** The tacticals in the module [New] are the tactical of Ltac. Their
@@ -240,7 +237,7 @@ module New : sig
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
-  val onHyps      : ([ `NF ], named_context) Proofview.Goal.enter ->
+  val onHyps      : ([ `LZ ], named_context) Proofview.Goal.enter ->
                     (named_context -> unit tactic) -> unit tactic
   val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 13ffbc52f..5ad43a7d6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -515,7 +515,7 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast
 | _ -> error "Not enough products."
 
 (* Refine as a fixpoint *)
-let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
+let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
@@ -571,7 +571,7 @@ let rec check_is_mutcoind env sigma cl =
       error "All methods must construct elements in coinductive types."
 
 (* Refine as a cofixpoint *)
-let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
+let mutual_cofix f others j = Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
@@ -697,12 +697,12 @@ let bind_red_expr_occurrences occs nbcl redexp =
    certain hypothesis *)
 
 let reduct_in_concl (redfun,sty) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
   end }
 
 let reduct_in_hyp ?(check=false) redfun (id,where) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl)
   end }
 
@@ -731,14 +731,14 @@ let pf_e_reduce_decl redfun where decl gl =
       Sigma (LocalDef (id, b', ty'), sigma, p +> q)
 
 let e_reduct_in_concl ~check (redfun, sty) =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
     Sigma (convert_concl ~check c' sty, sigma, p)
   end }
 
 let e_reduct_in_hyp ?(check=false) redfun (id, where) =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let Sigma (decl', sigma, p) = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
     Sigma (convert_hyp ~check decl', sigma, p)
   end }
@@ -1112,7 +1112,7 @@ let depth_of_quantified_hypothesis red h gl =
 	  str".")
 
 let intros_until_gen red h =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let n = depth_of_quantified_hypothesis red h gl in
   Tacticals.New.tclDO n (if red then introf else intro)
   end }
@@ -1226,7 +1226,7 @@ let cut c =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
-    let concl = Tacmach.New.pf_nf_concl gl in
+    let concl = Proofview.Goal.concl gl in
     let is_sort =
       try
         (** Backward compat: ensure that [c] is well-typed. *)
@@ -1360,7 +1360,7 @@ let enforce_prop_bound_names rename tac =
             mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
         | _ -> assert false in
       let rename_branch i =
-        Proofview.Goal.nf_enter { enter = begin fun gl ->
+        Proofview.Goal.enter { enter = begin fun gl ->
           let env = Proofview.Goal.env gl in
           let sigma = Tacmach.New.project gl in
           let t = Proofview.Goal.concl gl in
@@ -1438,7 +1438,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
 (* Case analysis tactics *)
 
 let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
@@ -1629,7 +1629,7 @@ let make_projection env sigma params cstr sign elim i n c u =
   in elim
 
 let descend_in_conjunctions avoid tac (err, info) c =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   try
@@ -1676,7 +1676,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
 (****************************************************)
 
 let solve_remaining_apply_goals =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   if !apply_solve_class_goals then
     try 
@@ -1701,7 +1701,7 @@ let tclORELSEOPT t k =
     | Some tac -> tac)
 
 let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : EConstr.constr with_bindings)) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   let sigma = Tacmach.New.project gl in
   let flags =
@@ -1854,7 +1854,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
 let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     id (clear_flag,(loc,(d,lbind))) tac =
   let open Context.Rel.Declaration in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let flags =
@@ -1915,7 +1915,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
 *)
 
 let cut_and_apply c =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
       | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
@@ -1969,7 +1969,7 @@ let native_cast_no_check c = cast_no_check Term.NATIVEcast c
 
 let exact_proof c =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   Refine.refine { run = begin fun sigma ->
     let sigma = Sigma.to_evar_map sigma in
     let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in
@@ -2005,7 +2005,7 @@ let assumption =
     let hyps = Proofview.Goal.hyps gl in
     arec gl true hyps
   end } in
-  Proofview.Goal.nf_enter assumption_tac
+  Proofview.Goal.enter assumption_tac
 
 (*****************************************************************)
 (*          Modification of a local context                      *)
@@ -2110,7 +2110,7 @@ let rec intros_clearing = function
 (* Keeping only a few hypotheses *)
 
 let keep hyps =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   Proofview.tclENV >>= fun env ->
   let ccl = Proofview.Goal.concl gl in
   let sigma = Tacmach.New.project gl in
@@ -2158,7 +2158,7 @@ let bring_hyps hyps =
     Proofview.Goal.enter { enter = begin fun gl ->
       let env = Proofview.Goal.env gl in
       let store = Proofview.Goal.extra gl in
-      let concl = Tacmach.New.pf_nf_concl gl in
+      let concl = Tacmach.New.pf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
       Refine.refine { run = begin fun sigma ->
@@ -2192,7 +2192,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
 let constructor_tac with_evars expctdnumopt i lbind =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let cl = Tacmach.New.pf_nf_concl gl in
+    let cl = Tacmach.New.pf_concl gl in
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
@@ -2231,7 +2231,7 @@ let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
   let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in
   Proofview.Goal.enter { enter = begin fun gl ->
-    let cl = Tacmach.New.pf_nf_concl gl in
+    let cl = Tacmach.New.pf_concl gl in
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
@@ -2291,7 +2291,7 @@ let my_find_eq_data_decompose gl t =
   | Constr_matching.PatternMatchingFailure -> None
 
 let intro_decomp_eq loc l thin tac id =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
@@ -2702,7 +2702,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       Sigma (mkNamedLetIn id c t x, sigma, p)
 
 let letin_tac with_eq id c ty occs =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let ccl = Proofview.Goal.concl gl in
@@ -2719,7 +2719,7 @@ let letin_tac with_eq id c ty occs =
   end }
 
 let letin_pat_tac with_eq id c occs =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let ccl = Proofview.Goal.concl gl in
@@ -2805,6 +2805,12 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
   let sigma, t = Typing.type_of env sigma c in
   generalize_goal_gen env sigma ids i o t cl
 
+let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
+  let env = Tacmach.New.pf_env gl in
+  let ids = Tacmach.New.pf_ids_of_hyps gl in
+  let sigma, t = Typing.type_of env sigma c in
+  generalize_goal_gen env sigma ids i o t cl
+
 let old_generalize_dep ?(with_let=false) c gl =
   let env = pf_env gl in
   let sign = pf_hyps gl in
@@ -2849,10 +2855,10 @@ let generalize_dep ?(with_let = false) c =
   Proofview.V82.tactic (old_generalize_dep ~with_let c)
 
 (**  *)
-let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let newcl, evd =
-    List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
+    List.fold_right_i (new_generalize_goal gl) 0 lconstr
       (Tacmach.New.pf_concl gl,Tacmach.New.project gl)
   in
   let (evd, _) = Typing.type_of env evd newcl in
@@ -3618,14 +3624,15 @@ let is_defined_variable env id =
   env |> lookup_named id |> is_local_def
 
 let abstract_args gl generalize_vars dep id defined f args =
+  let open Tacmach.New in
   let open Context.Rel.Declaration in
-  let sigma = ref (Tacmach.project gl) in
-  let env = Tacmach.pf_env gl in
-  let concl = Tacmach.pf_concl gl in
+  let sigma = ref (Tacmach.New.project gl) in
+  let env = Tacmach.New.pf_env gl in
+  let concl = Tacmach.New.pf_concl gl in
   let dep = dep || local_occur_var !sigma id concl in
   let avoid = ref [] in
   let get_id name =
-    let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
+    let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
       avoid := id :: !avoid; id
   in
     (* Build application generalized w.r.t. the argument plus the necessary eqs.
@@ -3640,7 +3647,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       let decl = List.hd rel in
       RelDecl.get_name decl, RelDecl.get_type decl, c
     in
-    let argty = Tacmach.pf_unsafe_type_of gl arg in
+    let argty = Tacmach.New.pf_unsafe_type_of gl arg in
     let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
     let () = sigma := sigma' in
     let lenctx = List.length ctx in
@@ -3681,7 +3688,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	      true, mkApp (f', before), after
   in
     if dogen then
-      let tyf' = Tacmach.pf_unsafe_type_of gl f' in
+      let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
 	Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
       in
@@ -3689,14 +3696,14 @@ let abstract_args gl generalize_vars dep id defined f args =
       let vars =
 	if generalize_vars then
 	  let nogen = Id.Set.add id nogen in
-	    hyps_of_vars (pf_env gl) (project gl) (pf_hyps gl) nogen vars
+	    hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars
 	else []
       in
       let body, c' =
 	if defined then Some c', Retyping.get_type_of ctxenv !sigma c'
 	else None, c'
       in
-      let typ = Tacmach.pf_get_hyp_typ gl id in
+      let typ = Tacmach.New.pf_get_hyp_typ id gl in
       let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in
       let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in
 	Some (tac, dep, succ (List.length ctx), vars)
@@ -3704,7 +3711,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
   let open Context.Named.Declaration in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   Coqlib.check_required_library Coqlib.jmeq_module_name;
   let sigma = Tacmach.New.project gl in
   let (f, args, def, id, oldid) =
@@ -3719,7 +3726,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
   if List.is_empty args then Proofview.tclUNIT ()
   else
     let args = Array.of_list args in
-    let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in
+    let newc = abstract_args gl generalize_vars force_dep id def f args in
       match newc with
       | None -> Proofview.tclUNIT ()
       | Some (tac, dep, n, vars) ->
@@ -3799,7 +3806,7 @@ let specialize_eqs id gl =
     else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
 
 
-let specialize_eqs id = Proofview.Goal.nf_enter { enter = begin fun gl ->
+let specialize_eqs id = Proofview.Goal.enter { enter = begin fun gl ->
   let msg = str "Specialization not allowed on dependent hypotheses" in
   Proofview.tclOR (clear [id])
     (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
@@ -4123,7 +4130,7 @@ let recolle_clenv i params args elimclause gl =
       (* from_n (Some 0) means that x should be taken "as is" without
          trying to unify (which would lead to trying to apply it to
          evars if y is a product). *)
-      let indclause  = Tacmach.New.of_old (fun gl -> mk_clenv_from_n gl (Some 0) (x,y)) gl in
+      let indclause  = mk_clenv_from_n gl (Some 0) (x,y) in
       let elimclause' = clenv_fchain ~with_univs:false i acc indclause in
       elimclause')
     (List.rev clauses)
@@ -4134,18 +4141,18 @@ let recolle_clenv i params args elimclause gl =
     produce new ones). Then refine with the resulting term with holes.
 *)
 let induction_tac with_evars params indvars elim =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = Tacmach.New.project gl in
   let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
   let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimc = contract_letin_in_lam_header sigma elimc in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
-  let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
+  let elimclause = Tacmach.New.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
   (* elimclause' is built from elimclause by instanciating all args and params. *)
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
-  let resolved = Tacmach.New.of_old (clenv_unique_resolver ~flags:(elim_flags ()) elimclause') gl in
+  let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
   enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)
   end }
 
@@ -4158,7 +4165,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let sigma = Sigma.to_evar_map sigma in
-    let concl = Tacmach.New.pf_nf_concl gl in
+    let concl = Tacmach.New.pf_concl gl in
     let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in
     let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in
     let dep = dep_in_hyps || dep_in_concl in
@@ -4212,7 +4219,7 @@ let msg_not_right_number_induction_arguments scheme =
    must be given, so we help a bit the unifier by making the "pattern"
    by hand before calling induction_tac *)
 let induction_without_atomization isrec with_evars elim names lid =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in
   let nargs_indarg_farg =
     scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in
@@ -4247,7 +4254,7 @@ let induction_without_atomization isrec with_evars elim names lid =
 
 (* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
   then user_err 
@@ -4493,7 +4500,7 @@ let induction_destruct isrec with_evars (lc,elim) =
   match lc with
   | [] -> assert false (* ensured by syntax, but if called inside caml? *)
   | [c,(eqname,names as allnames),cls] ->
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     match elim with
@@ -4594,8 +4601,8 @@ let simple_destruct = function
  *)
 
 let elim_scheme_type elim t =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in
+  Proofview.Goal.enter { enter = begin fun gl ->
+  let clause = mk_clenv_type_of gl elim in
   match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with
     | Meta mv ->
         let clause' =
@@ -4634,7 +4641,7 @@ let case_type t =
 let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
 
 let maybe_betadeltaiota_concl allowred gl =
-  let concl = Tacmach.New.pf_nf_concl gl in
+  let concl = Tacmach.New.pf_concl gl in
   let sigma = Tacmach.New.project gl in
   if not allowred then concl
   else
@@ -4891,7 +4898,7 @@ let abstract_subproof id gk tac =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let current_sign = Global.named_context_val ()
   and global_sign = Proofview.Goal.hyps gl in
@@ -4980,7 +4987,7 @@ let tclABSTRACT name_op tac =
   abstract_subproof s gk tac
 
 let unify ?(state=full_transparent_state) x y =
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   try
     let core_flags =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0087d607d..67e29cf56 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -29,7 +29,7 @@ open Locus
 
 (** {6 General functions. } *)
 
-val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool
+val is_quantified_hypothesis : Id.t -> ('a, 'r) Proofview.Goal.t -> bool
 
 (** {6 Primitive tactics. } *)
 
@@ -75,7 +75,7 @@ val intros               : unit Proofview.tactic
 (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
    the conclusion of goal [g], up to head-reduction if [b] is [true] *)
 val depth_of_quantified_hypothesis :
-  bool -> quantified_hypothesis -> ([`NF],'b) Proofview.Goal.t -> int
+  bool -> quantified_hypothesis -> ('a, 'r) Proofview.Goal.t -> int
 
 val intros_until         : quantified_hypothesis -> unit Proofview.tactic
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f343cc73d..e90d8a4fd 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -364,8 +364,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
         )))
       )
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
     let sigma = Tacmach.New.project gl in
     let u,v = destruct_ind sigma type_of_pq
     in let lb_type_of_p =
@@ -574,12 +574,10 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
         ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
       in
       let fresh_id s gl =
-        Tacmach.New.of_old begin fun gsig ->
-          let fresh = fresh_id (!avoid) s gsig in
+          let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
           avoid := fresh::(!avoid); fresh
-        end gl
       in
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
       let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
       let freshn = fresh_id (Id.of_string "x") gl in
       let freshm = fresh_id (Id.of_string "y") gl in
@@ -602,7 +600,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                     Tacticals.New.tclREPEAT (
                       Tacticals.New.tclTHENLIST [
                          Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
-                         Proofview.Goal.nf_enter { enter = begin fun gl ->
+                         Proofview.Goal.enter { enter = begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
                             destruct_on_as (EConstr.mkVar freshz)
                                   (IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht);
@@ -613,7 +611,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
   Ci a1 ... an = Ci b1 ... bn
  replace bi with ai; auto || replace bi with ai by  apply typeofbi_prod ; auto
 *)
-                      Proofview.Goal.nf_enter { enter = begin fun gl ->
+                      Proofview.Goal.enter { enter = begin fun gl ->
                         let concl = Proofview.Goal.concl gl in
                         let sigma = Tacmach.New.project gl in
                         match EConstr.kind sigma concl with
@@ -720,12 +718,10 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
         ( List.map (fun (_,_,_,slb) -> slb) list_id )
       in
       let fresh_id s gl =
-        Tacmach.New.of_old begin fun gsig ->
-          let fresh = fresh_id (!avoid) s gsig in
+          let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
           avoid := fresh::(!avoid); fresh
-        end gl
       in
-      Proofview.Goal.nf_enter { enter = begin fun gl ->
+      Proofview.Goal.enter { enter = begin fun gl ->
       let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
       let freshn = fresh_id (Id.of_string "x") gl in
       let freshm = fresh_id (Id.of_string "y") gl in
@@ -748,7 +744,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
                       Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
                                   simplest_split ;Auto.default_auto ]
                       );
-                      Proofview.Goal.nf_enter { enter = begin fun gls ->
+                      Proofview.Goal.enter { enter = begin fun gls ->
                         let concl = Proofview.Goal.concl gls in
                         let sigma = Tacmach.New.project gl in
                         (* assume the goal to be eq (eq_type ...) = true *)
@@ -869,12 +865,10 @@ let compute_dec_tact ind lnamesparrec nparrec =
       ( List.map (fun (_,_,_,slb) -> slb) list_id )
   in
   let fresh_id s gl =
-    Tacmach.New.of_old begin fun gsig ->
-      let fresh = fresh_id (!avoid) s gsig in
+      let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
       avoid := fresh::(!avoid); fresh
-    end gl
   in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
   let freshn = fresh_id (Id.of_string "x") gl in
   let freshm = fresh_id (Id.of_string "y") gl in
@@ -905,7 +899,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 	))
 	  (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
 
-        Proofview.Goal.nf_enter { enter = begin fun gl ->
+        Proofview.Goal.enter { enter = begin fun gl ->
           let freshH2 = fresh_id (Id.of_string "H") gl in
 	  Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
 	    (* left *)
@@ -917,7 +911,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
             ;
 
 	    (*right *)
-            Proofview.Goal.nf_enter { enter = begin fun gl ->
+            Proofview.Goal.enter { enter = begin fun gl ->
             let freshH3 = fresh_id (Id.of_string "H") gl in
             Tacticals.New.tclTHENLIST [
 	      simplest_right ;
-- 
cgit v1.2.3