Merge PR #11538: Remove many unsafe_type_of uses

Reviewed-by: Matafou
Reviewed-by: gares
Reviewed-by: ppedrot

44 files changed, 418 insertions, 406 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 500f464ea7..fdc70ccaa8 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -492,7 +492,7 @@ let rec add_term state t=
         Not_found ->
           let b=next uf in
           let trm = constr_of_term t in
-          let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in
+          let typ = Retyping.get_type_of state.env state.sigma (EConstr.of_constr trm) in
           let typ = canonize_name state.sigma typ in
           let new_node=
             match t with
@@ -809,23 +809,23 @@ let new_state_var typ state =
 
 let complete_one_class state i=
   match (get_representative state.uf i).inductive_status with
-      Partial pac ->
-        let rec app t typ n =
-          if n<=0 then t else
-            let _,etyp,rest= destProd typ in
-            let id = new_state_var (EConstr.of_constr etyp) state in
-                app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
-        let _c = Typing.unsafe_type_of state.env state.sigma
-          (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
-        let _c = EConstr.Unsafe.to_constr _c in
-        let _args =
-          List.map (fun i -> constr_of_term (term state.uf  i))
-            pac.args in
-        let typ = Term.prod_applist _c (List.rev _args) in
-        let ct = app (term state.uf i) typ pac.arity in
-          state.uf.epsilons <- pac :: state.uf.epsilons;
-          ignore (add_term state ct)
-    | _ -> anomaly (Pp.str "wrong incomplete class.")
+  | Partial pac ->
+    let rec app t typ n =
+      if n<=0 then t else
+        let _,etyp,rest= destProd typ in
+        let id = new_state_var (EConstr.of_constr etyp) state in
+        app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
+    let c = Retyping.get_type_of state.env state.sigma
+        (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+    let c = EConstr.Unsafe.to_constr c in
+    let args =
+      List.map (fun i -> constr_of_term (term state.uf  i))
+        pac.args in
+    let typ = Term.prod_applist c (List.rev args) in
+    let ct = app (term state.uf i) typ pac.arity in
+    state.uf.epsilons <- pac :: state.uf.epsilons;
+    ignore (add_term state ct)
+  | _ -> anomaly (Pp.str "wrong incomplete class.")
 
 let complete state =
   Int.Set.iter (complete_one_class state) state.pa_classes
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 556e6b48e6..8a650d9e7a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -277,10 +277,12 @@ let refresh_type env evm ty =
   Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
                               (Some false) env evm ty
 
-let refresh_universes ty k =
+let type_and_refresh c k =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
+    (* XXX is get_type_of enough? *)
+    let evm, ty = Typing.type_of env evm c in
     let evm, ty = refresh_type env evm ty in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty)
   end
@@ -289,7 +291,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.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
       Ax c -> exact_check (EConstr.of_constr c)
@@ -297,17 +298,17 @@ let rec proof_tac p : unit Proofview.tactic =
         let c = EConstr.of_constr c in
         let l=constr_of_term p.p_lhs and
             r=constr_of_term p.p_rhs in
-        refresh_universes (type_of l) (fun typ ->
+        type_and_refresh l (fun typ ->
         app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
         let lr = constr_of_term t in
-        refresh_universes (type_of lr) (fun typ ->
+        type_and_refresh lr (fun typ ->
         app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
         let t1 = constr_of_term p1.p_lhs and
             t2 = constr_of_term p1.p_rhs and
             t3 = constr_of_term p2.p_rhs in
-        refresh_universes (type_of t2) (fun typ ->
+        type_and_refresh t2 (fun typ ->
         let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
           Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
@@ -315,9 +316,9 @@ let rec proof_tac p : unit Proofview.tactic =
         and tx1=constr_of_term p2.p_lhs
         and tf2=constr_of_term p1.p_rhs
         and tx2=constr_of_term p2.p_rhs in
-        refresh_universes (type_of tf1) (fun typf ->
-        refresh_universes (type_of tx1) (fun typx ->
-        refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
+        type_and_refresh tf1 (fun typf ->
+        type_and_refresh tx1 (fun typx ->
+        type_and_refresh (mkApp (tf1,[|tx1|])) (fun typfx ->
         let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
         let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in
         let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
@@ -341,8 +342,8 @@ let rec proof_tac p : unit Proofview.tactic =
          let tj=constr_of_term prf.p_rhs in
          let default=constr_of_term p.p_lhs in
          let special=mkRel (1+nargs-argind) in
-         refresh_universes (type_of ti) (fun intype ->
-         refresh_universes (type_of default) (fun outtype ->
+         type_and_refresh ti (fun intype ->
+         type_and_refresh default (fun outtype ->
          let sigma, proj =
            build_projection intype cstr special default gl
          in
@@ -362,7 +363,7 @@ let refute_tac c t1 t2 p =
     let neweq= app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
+  in type_and_refresh tt1 k
   end
 
 let refine_exact_check c =
@@ -382,7 +383,7 @@ let convert_to_goal_tac c t1 t2 p =
     let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
                            [proof_tac p; endt refine_exact_check]
-  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
+  in type_and_refresh tt2 k
   end
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -401,7 +402,8 @@ let discriminate_tac cstru p =
     let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
-    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in
+    let evm, intype = Typing.type_of env evm lhs in
+    let evm, intype = refresh_type env evm intype in
     let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
     let neweq=app_global _eq [|intype;lhs;rhs|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 8946587a02..9d208e1c86 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -88,7 +88,7 @@ let gen_ground_tac flag taco ids bases =
         Proofview.Goal.enter begin fun gl ->
         let seq=empty_seq !ground_depth in
         let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
-        let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
+        let seq, sigma = extend_with_auto_hints (pf_env gl) sigma bases seq in
         tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
         end
       in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e131cad7da..866b45e4df 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -100,25 +100,28 @@ let rec collect_quantified sigma seq=
 
 let dummy_bvid=Id.of_string "x"
 
-let mk_open_instance env evmap id idc m t =
-  let var_id=
-    if id==dummy_id then dummy_bvid else
-      let typ=Typing.unsafe_type_of env evmap idc in
+let mk_open_instance env sigma id idc m t =
+  let var_id =
+    (* XXX why physical equality? *)
+    if id == dummy_id then dummy_bvid else
+      let typ = Retyping.get_type_of env sigma idc in
         (* since we know we will get a product,
            reduction is not too expensive *)
-      let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
+      let (nam,_,_) = destProd sigma (whd_all env sigma typ) in
         match nam.Context.binder_name with
-            Name id -> id
-          | Anonymous ->  dummy_bvid in
-  let revt=substl (List.init m (fun i->mkRel (m-i))) t in
-  let rec aux n avoid env evmap decls =
-    if Int.equal n 0 then evmap, decls else
-      let nid=(fresh_id_in_env avoid var_id env) in
-      let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+        | Name id -> id
+        | Anonymous ->  dummy_bvid
+  in
+  let revt = substl (List.init m (fun i->mkRel (m-i))) t in
+  let rec aux n avoid env sigma decls =
+    if Int.equal n 0 then sigma, decls else
+      let nid = fresh_id_in_env avoid var_id env in
+      let (sigma, (c, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
       let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
-        aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
-  let evmap, decls = aux m Id.Set.empty env evmap [] in
-  (evmap, decls, revt)
+      aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) sigma (decl::decls)
+  in
+  let sigma, decls = aux m Id.Set.empty env sigma [] in
+  (sigma, decls, revt)
 
 (* tactics   *)
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7d84ee6851..65af123d9c 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -204,28 +204,28 @@ let extend_with_ref_list env sigma l seq =
 open Hints
 
 let extend_with_auto_hints env sigma l seq =
-  let seqref=ref seq in
-  let f p_a_t =
+  let f (seq,sigma) p_a_t =
     match repr_hint p_a_t.code with
-        Res_pf (c,_) | Give_exact (c,_)
-      | Res_pf_THEN_trivial_fail (c,_) ->
-          let (c, _, _) = c in
-          (try
-             let (gr, _) = Termops.global_of_constr sigma c in
-             let typ=(Typing.unsafe_type_of env sigma c) in
-               seqref:=add_formula env sigma Hint gr typ !seqref
-           with Not_found->())
-      | _-> () in
-  let g _ _ l = List.iter f l in
-  let h dbname=
-    let hdb=
+    | Res_pf (c,_) | Give_exact (c,_)
+    | Res_pf_THEN_trivial_fail (c,_) ->
+      let (c, _, _) = c in
+      (try
+         let (gr, _) = Termops.global_of_constr sigma c in
+         let sigma, typ = Typing.type_of env sigma c in
+         add_formula env sigma Hint gr typ seq, sigma
+       with Not_found -> seq, sigma)
+    | _ -> seq, sigma
+  in
+  let h acc dbname =
+    let hdb =
       try
         searchtable_map dbname
       with Not_found->
-        user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in
-      Hint_db.iter g hdb in
-    List.iter h l;
-    !seqref, sigma (*FIXME: forgetting about universes*)
+        user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database"))
+    in
+    Hint_db.fold (fun _ _ l acc -> List.fold_left f acc l) hdb acc
+  in
+  List.fold_left h (seq,sigma) l
 
 let print_cmap map=
   let print_entry c l s=
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6db0a1119b..9749af1e66 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -475,7 +475,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       tclIDTAC
   in
   try
-    scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
+    scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -525,7 +525,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
         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_unsafe_type_of g' (mkVar heq_id) in
+           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
@@ -536,22 +536,23 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
                            );
                    anomaly (Pp.str "cannot compute new term value.")
            in
-         let fun_body =
-           mkLambda(make_annot Anonymous Sorts.Relevant,
-                    pf_unsafe_type_of g' term,
-                    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
+           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'
-      )])
-    ]
+             }
+           in
+           clean_goal_with_heq ptes_infos continue_tac new_infos  g'
+          )])
+      ]
       g
 
 
@@ -633,7 +634,7 @@ let build_proof
                   let dyn_infos = {dyn_info' with info =
                       mkCase(ci,ct,t,cb)} in
                   let g_nb_prod = nb_prod (project g) (pf_concl g) in
-                  let type_of_term = pf_unsafe_type_of g t 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
@@ -849,7 +850,7 @@ 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_unsafe_type_of g (mkVar hyp) 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 ->
@@ -1351,7 +1352,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
     let rewrite =
       tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
-    let _,hrec_concl  = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) 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 =
@@ -1573,19 +1574,16 @@ let prove_principle_for_gen
         (List.rev_map (get_name %> Nameops.Name.get_id)
            (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
         );
-      (* observe_tac "" *) 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)
-      );
-(*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
-(*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
-(*                         str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
-      (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1)));
-(*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
+      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));
-      (* observe_tac "finish" *) (fun gl' ->
+      (fun gl' ->
          let body =
            let _,args = destApp (project gl') (pf_concl gl') in
            Array.last args
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 58efee1518..68661174ac 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -617,7 +617,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       let constructor_args g =
         List.fold_right
           (fun hid acc ->
-             let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+             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') ->
@@ -953,7 +953,7 @@ let rec reflexivity_with_destruct_cases g =
         match sc with
           None -> tclIDTAC g
         | Some id ->
-          match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
+          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
@@ -993,7 +993,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i))  in
-    let princ_type = pf_unsafe_type_of g graph_principle in
+    let 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
@@ -1210,7 +1210,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
   in
   let _ = evd := sigma in
   let l_schemes =
-    List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
+    List.map (EConstr.of_constr %> Retyping.get_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
   in
   let i = ref (-1) in
   let sorts =
@@ -2051,7 +2051,7 @@ let build_case_scheme fa =
   let (sigma, scheme) =
       Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
-  let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
+  let scheme_type = EConstr.Unsafe.to_constr ((Retyping.get_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
        fst @@ UnivGen.fresh_sort_in_family x
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e41b92d4dc..84f09c385f 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -514,8 +514,9 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
                    a pseudo value "v1 ... vn".
                    The "value" of this branch is then simply [res]
                 *)
+                (* XXX here and other [understand] calls drop the ctx *)
                 let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
-                let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+                let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in
                 let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
                 let res = fresh_id args_res.to_avoid "_res" in
                 let new_avoid = res::args_res.to_avoid in
@@ -629,7 +630,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
         let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
         let v_res = build_entry_lc env sigma funnames avoid v in
         let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
-        let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
+        let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in
         let v_r = Sorts.Relevant in (* TODO relevance *)
         let new_env =
           match n with
@@ -646,7 +647,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
         build_entry_lc_from_case env sigma funnames make_discr el brl avoid
     | GIf(b,(na,e_option),lhs,rhs) ->
         let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-        let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+        let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
         let (ind,_) =
           try Inductiveops.find_inductive env (Evd.from_env env) b_typ
           with Not_found ->
@@ -678,7 +679,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
               nal
           in
           let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
-          let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+          let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
           let (ind,_) =
             try Inductiveops.find_inductive env (Evd.from_env env) b_typ
             with Not_found ->
@@ -723,7 +724,7 @@ and build_entry_lc_from_case env sigma funname make_discr
         let types =
           List.map (fun (case_arg,_) ->
                       let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
-                      EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr)
+                      EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr)
                    ) el
         in
         (****** The next works only if the match is not dependent ****)
@@ -769,9 +770,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to
                  let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
                    List.fold_right
                      (fun id acc ->
-                        let typ_of_id =
-                          Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
-                        in
+                        let typ_of_id = Typing.type_of_variable env_with_pat_ids id in
                         let raw_typ_of_id =
                           Detyping.detype Detyping.Now false Id.Set.empty
                             env_with_pat_ids (Evd.from_env env) typ_of_id
@@ -832,7 +831,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to
                    (fun id  acc ->
                       if Id.Set.mem id this_pat_ids
                       then (Prod (Name id),
-                      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
+                      let typ_of_id = Typing.type_of_variable new_env id in
                       let raw_typ_of_id =
                         Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
                       in
@@ -1166,7 +1165,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
           let evd = (Evd.from_env env) in
           let t',ctx = Pretyping.understand env evd t in
           let evd = Evd.from_ctx ctx in
-          let type_t' = Typing.unsafe_type_of env evd t' in
+          let type_t' = Retyping.get_type_of env evd t' in
           let t' = EConstr.Unsafe.to_constr t' in
           let type_t' = EConstr.Unsafe.to_constr type_t' in
           let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a205c0744a..f28e98dcc2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -64,12 +64,10 @@ let functional_induction with_clean c princl pat =
             | InSet -> finfo.rec_lemma
             | InType -> finfo.rect_lemma
           in
-          let princ =  (* then we get the principle *)
+          let sigma, princ =  (* then we get the principle *)
             match princ_option with
             | Some princ ->
-              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in
-              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-              Proofview.tclUNIT princ
+              Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ)
             | None ->
               (*i If there is not default lemma defined then,
                       we cross our finger and try to find a lemma named f_ind
@@ -87,19 +85,18 @@ let functional_induction with_clean c princl pat =
                   user_err (str "Cannot find induction principle for "
                             ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
               in
-              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in
-              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-              Proofview.tclUNIT princ
+              Evd.fresh_global (pf_env gl) (project gl) princ_ref
           in
-          princ >>= fun princ ->
-          (* We need to refresh gl due to the updated evar_map in princ *)
-          Proofview.Goal.enter_one (fun gl ->
-          Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args))
+          let princt = Retyping.get_type_of (pf_env gl) sigma princ in
+          Proofview.Unsafe.tclEVARS sigma <*>
+          Proofview.tclUNIT (princ, Tactypes.NoBindings, princt, args)
         | _ ->
           CErrors.user_err (str "functional induction must be used with a function" )
       end
     | Some ((princ,binding)) ->
-      Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args)
+      let sigma, princt = pf_type_of gl princ in
+      Proofview.Unsafe.tclEVARS sigma <*>
+      Proofview.tclUNIT (princ, binding, princt, args)
     ) >>= fun (princ, bindings, princ_type, args) ->
   Proofview.Goal.enter (fun gl ->
   let sigma = project gl in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b55d8537d6..bce09d8fbd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -526,3 +526,7 @@ let funind_purify f x =
     let e = CErrors.push e in
     Vernacstate.unfreeze_interp_state st;
     Exninfo.iraise e
+
+let tac_type_of g c =
+  let sigma, t = Tacmach.pf_type_of g c in
+  {g with Evd.sigma}, t
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 550f727951..bd8b34088b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -119,3 +119,5 @@ type tcc_lemma_value =
   | Not_needed
 
 val funind_purify : ('a -> 'b) -> ('a -> 'b)
+
+val tac_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d72319d078..332d058ce7 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -28,7 +28,7 @@ open Indfun_common
 *)
 let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
   let sigma = project gl in
-  let typ = pf_unsafe_type_of gl (mkVar hid) in
+  let typ = pf_get_hyp_typ hid gl in
   match EConstr.kind sigma typ with
   | App(i,args) when isInd sigma i ->
     let ((kn',num) as ind'),u = destInd sigma i in
@@ -77,7 +77,7 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
 let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl ->
   let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps gl) Id.Set.empty in
   let sigma = project gl in
-  let type_of_h = pf_unsafe_type_of gl (mkVar hid) in
+  let type_of_h = pf_get_hyp_typ hid gl in
   match EConstr.kind sigma type_of_h with
   | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
     let pre_tac,f_args,res =
@@ -128,7 +128,7 @@ let invfun qhyp f =
   | None ->
     let tac_action hid gl =
       let sigma = project gl in
-      let hyp_typ = pf_unsafe_type_of gl (mkVar hid)  in
+      let hyp_typ = pf_get_hyp_typ hid gl  in
       match EConstr.kind sigma hyp_typ with
       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
         begin
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 66ed1961ba..f7f8004998 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -31,7 +31,6 @@ open Tactics
 open Nametab
 open Declare
 open Tacred
-open Goal
 open Glob_term
 open Pretyping
 open Termops
@@ -110,9 +109,10 @@ let pf_get_new_ids idl g =
 let next_ident_away_in_goal ids avoid =
   next_ident_away_in_goal ids (Id.Set.of_list avoid)
 
-let compute_renamed_type gls c =
+let compute_renamed_type gls id =
   rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) []
-    (pf_unsafe_type_of gls c)
+    (pf_get_hyp_typ gls id)
+
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -370,7 +370,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
             Proofview.V82.of_tactic (clear to_intros);
             h_intros to_intros;
             (fun g' ->
-              let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
+              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)
@@ -487,13 +487,13 @@ let rec prove_lt hyple g =
       in
       let h =
         List.find (fun id ->
-          match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with
+          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_unsafe_type_of g (mkVar h))))) in
+        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)
@@ -645,9 +645,7 @@ 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 :
-  Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list =
-  fun not_on_hyp expr g ->
+let mkDestructEq not_on_hyp expr g =
   let hyps = pf_hyps g in
   let to_revert =
     Util.List.map_filter
@@ -657,9 +655,9 @@ let mkDestructEq :
         if Id.List.mem id not_on_hyp || not (Termops.dependent (project g) expr (get_type decl))
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let type_of_expr = pf_unsafe_type_of g expr in
-  let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
-           to_revert_constr in
+  let g, type_of_expr = tac_type_of g 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 (fun _ _ -> str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
@@ -668,7 +666,9 @@ let mkDestructEq :
           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)]), to_revert
+      Proofview.V82.of_tactic (simplest_case expr)])
+  in
+  g, tac, to_revert
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let sigma = project g in
@@ -686,7 +686,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
       info = mkCase(ci,t,a',l);
       is_main_branch = expr_info.is_main_branch;
       is_final = expr_info.is_final} in
-  let destruct_tac,rev_to_thin_intro =
+  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')
@@ -842,7 +842,7 @@ let rec make_rewrite_list expr_info max = function
       (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) (
         (fun g ->
           let sigma = project g in
-          let t_eq = compute_renamed_type g (mkVar hp) 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
@@ -868,7 +868,7 @@ let make_rewrite expr_info l hp max =
     (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS
        (fun g ->
           let sigma = project g in
-          let t_eq = compute_renamed_type g (mkVar hp) 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
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 6c63a891e8..513f5ca77b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -736,7 +736,7 @@ let refl_equal () = Coqlib.lib_ref "core.eq.type"
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
-    let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
+    let type_of_a = Tacmach.New.pf_get_type_of gl a in
     Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
     Tacticals.New.tclTHENLIST
          [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
@@ -794,7 +794,7 @@ let destauto t =
 
 let destauto_in id =
   Proofview.Goal.enter begin fun gl ->
-  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
+  let ctype = Tacmach.New.pf_get_type_of gl (mkVar id) in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 98d14f3d33..a0eefd1a39 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -483,7 +483,7 @@ let rec decompose_app_rel env evd t =
   | App (f, [||]) -> assert false
   | App (f, [|arg|]) ->
     let (f', argl, argr) = decompose_app_rel env evd arg in
-    let ty = Typing.unsafe_type_of env evd argl in
+    let ty = Retyping.get_type_of env evd argl in
     let r = Retyping.relevance_of_type env evd ty in
     let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty,
       mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty,
@@ -789,7 +789,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
     let morphargs, morphobjs = Array.chop first args in
     let morphargs', morphobjs' = Array.chop first args' in
     let appm = mkApp(m, morphargs) in
-    let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
+    let evd, appmtype = Typing.type_of env (goalevars evars) appm in
+    let evars = evd, snd evars in
     let cstrs = List.map
       (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
       (Array.to_list morphobjs')
@@ -1906,7 +1907,7 @@ let declare_projection n instance_id r =
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
   let sigma = Evd.from_ctx ctx in
-  let t = Typing.unsafe_type_of env sigma m in
+  let t = Retyping.get_type_of env sigma m in
   let cstrs =
     let rec aux t =
       match EConstr.kind sigma t with
@@ -1936,7 +1937,7 @@ let build_morphism_signature env sigma m =
 let default_morphism sign m =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let t = Typing.unsafe_type_of env sigma m in
+  let t = Retyping.get_type_of env sigma m in
   let evars, _, sign, cstrs =
     PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
   in
@@ -2195,10 +2196,10 @@ let setoid_transitivity c =
     (transitivity_red true c)
 
 let setoid_symmetry_in id =
-  let open Tacmach.New in
   Proofview.Goal.enter begin fun gl ->
-  let sigma = project gl in
-  let ctype = pf_unsafe_type_of gl (mkVar id) in
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let ctype = Retyping.get_type_of env sigma (mkVar id) in
   let binders,concl = decompose_prod_assum sigma ctype in
   let (equiv, args) = decompose_app sigma concl in
   let rec split_last_two = function
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index dcd85401d6..979e5bb8d8 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1713,7 +1713,6 @@ let onClearedName2 id tac =
 
 let destructure_hyps =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let decidability = decidability env sigma in
@@ -1759,7 +1758,7 @@ let destructure_hyps =
           | Kimp(t1,t2) ->
               (* t1 and t2 might be in Type rather than Prop.
                  For t1, the decidability check will ensure being Prop. *)
-              if Termops.is_Prop sigma (type_of t2)
+              if Termops.is_Prop sigma (Retyping.get_type_of env sigma t2)
               then
                 let d1 = decidability t1 in
                 tclTHENLIST [
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index cbd04a76ad..29d6726262 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2164,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid =
         let IndType (indf, _) =
           try find_rectype env sigma (lift (-(List.length realargs)) ty)
           with Not_found -> error_case_not_inductive env sigma
-            {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty}
+            {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty}
         in
         let (ind,u), params = dest_ind_family indf in
         let params = List.map EConstr.of_constr params in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bf61d44a10..cb0c4868b5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -446,7 +446,7 @@ let pretype_ref ?loc sigma env ref us =
          Pretype_errors.error_var_not_found ?loc !!env sigma id)
   | ref ->
     let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
-    let ty = unsafe_type_of !!env sigma c in
+    let sigma, ty = type_of !!env sigma c in
     sigma, make_judge c ty
 
 let interp_sort ?loc evd : glob_sort -> _ = function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 10e8cf7e0f..f87c50b5e4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
 let pattern_occs loccs_trm = begin fun env sigma c ->
   let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
   try
-    let _ = Typing.unsafe_type_of env sigma abstr_trm in
+    let sigma, _ = Typing.type_of env sigma abstr_trm in
     (sigma, applist(abstr_trm, List.map snd loccs_trm))
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index a15134f58d..4582844b71 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -253,6 +253,9 @@ let judge_of_type u =
 let judge_of_relative env v =
   Environ.on_judgment EConstr.of_constr (judge_of_relative env v)
 
+let type_of_variable env id =
+  EConstr.of_constr (type_of_variable env id)
+
 let judge_of_variable env id =
   Environ.on_judgment EConstr.of_constr (judge_of_variable env id)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1b07b2bb78..fd2dc7c2fc 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -30,6 +30,9 @@ val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
 (** Typecheck a term has a given type (assuming the type is OK) *)
 val check : env -> evar_map -> constr -> types -> evar_map
 
+(** Type of a variable. *)
+val type_of_variable : env -> variable -> types
+
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6486435ca2..2157c4ef6a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1274,12 +1274,14 @@ let applyHead env evd n c  =
     else
       match EConstr.kind evd (whd_all env evd cty) with
       | Prod (_,c1,c2) ->
-        let (evd',evar) =
-      Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
-      apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
+        let (evd,evar) =
+          Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1
+        in
+        apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd
       | _ -> user_err Pp.(str "Apply_Head_Then")
   in
-    apprec n c (Typing.unsafe_type_of env evd c) evd
+  let evd, t = Typing.type_of env evd c in
+  apprec n c t evd
 
 let is_mimick_head sigma ts f =
   match EConstr.kind sigma f with
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index e466992721..b0eb8dc646 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -128,8 +128,6 @@ let mk_clenv_from_n gls 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,Tacmach.New.pf_unsafe_type_of gls t)
-
 (******************************************************************)
 
 (* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 3fca967395..7213c9318c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -46,7 +46,6 @@ val clenv_meta_type : clausenv -> metavariable -> types
 val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
   Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : 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 *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a361c4208e..bac13fcfc3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -79,7 +79,7 @@ let check = ref false
 let with_check = Flags.with_option check
 
 let check_typability env sigma c =
-  if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
+  if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma
 
 (************************************************************************)
 (************************************************************************)
@@ -363,7 +363,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
           gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
-        check_typability env sigma ty;
+        let sigma = check_typability env sigma ty in
         let sigma = check_conv_leq_goal env sigma trm ty conclty in
         let res = mk_refgoals sigma goal goalacc ty t in
         (* we keep the casts (in particular VMcast and NATIVEcast) except
@@ -430,13 +430,13 @@ and mk_hdgoals sigma goal goalacc trm =
     Goal.V82.mk_goal sigma hyps concl in
   match kind trm with
     | Cast (c,_, ty) when isMeta c ->
-        check_typability env sigma ty;
+        let sigma = check_typability env sigma ty in
         let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
         let ev = EConstr.Unsafe.to_constr ev in
         gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
-        check_typability env sigma ty;
+        let sigma = check_typability env sigma ty in
         mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index cd6f445503..1bbcca8827 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -238,7 +238,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     in
       try
         let others,(c1,c2) = split_last_two args in
-        let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in
+        let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in
         (* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
         let open EConstr in
         let hyp_ty = Unsafe.to_constr ty in
@@ -261,7 +261,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
         | None -> None
 
 let find_applied_relation ?loc metas env sigma c left2right =
-  let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
+  let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in
     match decompose_applied_relation metas env sigma c ctype left2right with
     | Some c -> c
     | None ->
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f8cb8870ea..ccd88d2c35 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1202,10 +1202,9 @@ let autoapply c i =
   in
   let flags = auto_unif_flags
     (Hints.Hint_db.transparent_state hintdb) in
-  let cty = Tacmach.New.pf_unsafe_type_of gl c in
+  let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-    unify_e_resolve false flags gl
-                                 ((c,cty,Univ.ContextSet.empty),0,ce) <*>
+    unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 1f5a6380fd..c7b6998c8c 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -110,8 +110,7 @@ let contradiction_term (c,lbind as cl) =
   Proofview.Goal.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
-    let typ = type_of c in
+    let typ = Tacmach.New.pf_get_type_of gl c in
     let _, ccl = splay_prod env sigma typ in
     if is_empty_type env sigma ccl then
       Tacticals.New.tclTHEN
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 361215bf38..80ca124912 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -32,11 +32,13 @@ let eauto_unif_flags = auto_flags_of_state TransparentState.full
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter begin fun gl ->
-  let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+  let sigma, t1 = Tacmach.New.pf_type_of gl c in
   let t2 = Tacmach.New.pf_concl gl in
-  let sigma = Tacmach.New.project gl in
   if occur_existential sigma t1 || occur_existential sigma t2 then
-     Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
+    Tacticals.New.tclTHENLIST
+      [Proofview.Unsafe.tclEVARS sigma;
+       Clenvtac.unify ~flags t1;
+       exact_no_check c]
   else exact_check c
   end
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ea61b8e4df..379a8d5401 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -80,14 +80,11 @@ let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = pf_unsafe_type_of gl in
-  let env = pf_env gl in
-  let sigma = project gl in
-  let typc = type_of c in
+  let typc = pf_get_type_of gl c in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
-            (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma))
+            (ifOnHyp recognizer (general_decompose_aux recognizer)
               (fun id -> clear [id])));
        exact_no_check c ]
   end
@@ -136,7 +133,7 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHypId
        (fun id ->
           Proofview.Goal.enter begin fun gl ->
-          let idty = pf_unsafe_type_of gl (mkVar id) in
+          let idty = pf_get_type_of gl (mkVar id) in
           let fvty = global_vars (pf_env gl) (project gl) idty in
           let possible_bring_hyps =
             (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bdfd200988..a82b26f428 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -195,13 +195,13 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with
   ]
 | a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter begin fun gl ->
-  let rectype = pf_unsafe_type_of gl a1 in
+  let sigma, rectype = pf_type_of gl a1 in
   let decide = mk rectype a1 a2 in
   let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
     else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
-  (tclTHENS (elim_type decide) subtacs)
+  tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (elim_type decide) subtacs)
   end
 | _ -> invalid_arg "List.fold_right2"
 
@@ -274,11 +274,12 @@ let compare c1 c2 =
   pf_constr_of_global (lib_ref "core.eq.type") >>= fun eqc ->
   pf_constr_of_global (lib_ref "core.not.type") >>= fun notc ->
   Proofview.Goal.enter begin fun gl ->
-  let rectype = pf_unsafe_type_of gl c1 in
+  let sigma, rectype = pf_type_of gl c1 in
   let ops = (opc,eqc,notc) in
   let decide = mkDecideEqGoal true ops rectype c1 c2 in
-  (tclTHENS (cut decide)
-            [(tclTHEN  intro
-             (tclTHEN (onLastHyp simplest_case) clear_last));
-             decideEquality rectype ops])
+  tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (tclTHENS (cut decide)
+       [(tclTHEN  intro
+           (tclTHEN (onLastHyp simplest_case) clear_last));
+        decideEquality rectype ops])
   end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 96b61b6994..9195746dc6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1062,14 +1062,14 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 
 let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.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
+  let t = pf_get_type_of gl c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
   let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
+  (* FIXME evar leak *)
+  let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
@@ -1165,7 +1165,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, get_type_of env sigma (mkRel i)))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1210,7 +1210,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let rec sigrec_clausal_form sigma siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-      let dflt_typ = unsafe_type_of env sigma dflt in
+      let sigma, dflt_typ = type_of env sigma dflt in
       try
         let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in
         let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
@@ -1224,29 +1224,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       let sigma, ev = Evarutil.new_evar env sigma a in
       let rty = beta_applist sigma (p_i_minus_1,[ev]) in
       let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in
-      let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in
-      match evopt with
-        | Some w ->
-          let w_type = unsafe_type_of env sigma w in
-          begin match Evarconv.unify_leq_delay env sigma w_type a with
-            | sigma ->
-              let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
-              sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
-            | exception Evarconv.UnableToUnify _ ->
-              user_err Pp.(str "Cannot solve a unification problem.")
-          end
-        | None ->
-            (* This at least happens if what has been detected as a
-               dependency is not one; use an evasive error message;
-               even if the problem is upwards: unification should be
-               tried in the first place in make_iterated_tuple instead
-               of approximatively computing the free rels; then
-               unsolved evars would mean not binding rel *)
-            user_err Pp.(str "Cannot solve a unification problem.")
+      if EConstr.isEvar sigma ev then
+        (* This at least happens if what has been detected as a
+           dependency is not one; use an evasive error message;
+           even if the problem is upwards: unification should be
+           tried in the first place in make_iterated_tuple instead
+           of approximatively computing the free rels; then
+           unsolved evars would mean not binding rel *)
+        user_err Pp.(str "Cannot solve a unification problem.")
+      else
+        let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
+        sigma, applist(exist_term,[a;p_i_minus_1;ev;tuple_tail])
   in
   let sigma = Evd.clear_metas sigma in
   let sigma, scf = sigrec_clausal_form sigma siglen ty in
-    sigma, Evarutil.nf_evar sigma scf
+  sigma, Evarutil.nf_evar sigma scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
@@ -1319,7 +1311,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
+  | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1341,7 +1333,7 @@ let inject_if_homogenous_dependent_pair ty =
   Proofview.Goal.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
+    let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in
     (* fetch the informations of the  pair *)
     let sigTconstr   = Coqlib.(lib_ref "core.sigT.type") in
     let existTconstr = Coqlib.lib_ref    "core.sigT.intro" in
@@ -1360,7 +1352,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)
@@ -1603,7 +1595,7 @@ let cutSubstInConcl l2r eqn =
   Proofview.Goal.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
+  let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
@@ -1620,7 +1612,7 @@ let cutSubstInHyp l2r eqn id =
   Proofview.Goal.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
+  let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
@@ -1715,7 +1707,7 @@ let is_eq_x gl x d =
     | _ -> false
     in
     let c = pf_nf_evar gl (NamedDecl.get_type d) in
-    let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
+    let (_,lhs,rhs) = pi3 (pf_apply find_eq_data_decompose gl c) in
     if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
     if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
   with Constr_matching.PatternMatchingFailure ->
@@ -1812,7 +1804,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
   let find_equations gl =
     let env = Proofview.Goal.env gl in
     let sigma = project gl in
-    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
     let select_equation_name decl =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
@@ -1837,7 +1829,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
     Proofview.Goal.enter begin fun gl ->
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
-    let find_eq_data_decompose = find_eq_data_decompose gl in
+    let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
     let _,_,(_,x,y) = find_eq_data_decompose c in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
@@ -1863,7 +1855,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
    let-ins *)
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
-  let find_eq_data_decompose = find_eq_data_decompose gl in
+  let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
   let test (_,c) =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
@@ -1887,19 +1879,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
 
 let cond_eq_term_left c t gl =
   try
-    let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
+    let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then true else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
-    let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
+    let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then false else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
-    let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
+    let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in
     if pf_conv_x gl c x then true
     else if pf_conv_x gl c y then false
     else failwith "not convertible"
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b3797119a..73e8331bcb 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -26,7 +26,6 @@ open Libnames
 open Smartlocate
 open Termops
 open Inductiveops
-open Typing
 open Typeclasses
 open Pattern
 open Patternops
@@ -966,16 +965,17 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
+  let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in
   let hd = head_constr sigma t in
   let ce = mk_clenv_from_env env sigma None (c,t) in
-  (Some hd, { pri=1;
-              poly = poly;
-              pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
-              name = name;
-              db = None;
-              secvars = secvars_of_constr env sigma c;
-              code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
+  (Some hd,
+   { pri=1;
+     poly = poly;
+     pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
+     name = name;
+     db = None;
+     secvars = secvars_of_constr env sigma c;
+     code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
 
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 2a9b71387e..9c9f0b7708 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -160,6 +160,8 @@ module Hint_db :
     val iter : (GlobRef.t option ->
                 hint_mode array list -> full_hint list -> unit) -> t -> unit
 
+    val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a
+
     val use_dn : t -> bool
     val transparent_state : t -> TransparentState.t
     val set_transparent_state : t -> TransparentState.t -> t
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 90a9a7acd9..c5ed02e043 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -19,7 +19,6 @@ open Inductiveops
 open Constr_matching
 open Coqlib
 open Declarations
-open Tacmach.New
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -452,26 +451,26 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
   let hd,u = destInd sigma (fst (destApp sigma eqn)) in
     d,u,k
 
-let extract_eq_args gl = function
+let extract_eq_args env sigma = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
+      let t = Retyping.get_type_of env sigma e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
-      if pf_conv_x gl t1 t2 then (t1,e1,e2)
+      if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2)
       else raise PatternMatchingFailure
 
-let find_eq_data_decompose gl eqn =
-  let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in
-  (lbeq,u,extract_eq_args gl eq_args)
+let find_eq_data_decompose env sigma eqn =
+  let (lbeq,u,eq_args) = find_eq_data sigma eqn in
+  (lbeq,u,extract_eq_args env sigma eq_args)
 
-let find_this_eq_data_decompose gl eqn =
+let find_this_eq_data_decompose env sigma eqn =
   let (lbeq,u,eq_args) =
     try (*first_match (match_eq eqn) inversible_equalities*)
-      find_eq_data (project gl) eqn
+      find_eq_data sigma eqn
     with PatternMatchingFailure ->
       user_err  (str "No primitive equality found.") in
   let eq_args =
-    try extract_eq_args gl eq_args
+    try extract_eq_args env sigma eq_args
     with PatternMatchingFailure ->
       user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in
   (lbeq,u,eq_args)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 803305a1ca..0000f81d3f 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -122,11 +122,11 @@ val match_with_equation:
 
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u]
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : Environ.env -> evar_map -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : Environ.env -> evar_map -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index be0421d42d..2181eb25af 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -464,7 +464,7 @@ let raw_inversion inv_kind id status names =
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
     let (ind, t) =
-      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
+      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c)
       with UserError _ ->
         let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in
         CErrors.user_err  msg
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cf58c9306c..def4af1ae8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -259,7 +259,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
 let lemInv id c =
   Proofview.Goal.enter begin fun gls ->
   try
-    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
+    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
     Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
   with
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ed7ab9164a..58d2097dea 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -587,7 +587,7 @@ module New = struct
   let ifOnHyp pred tac1 tac2 id =
     Proofview.Goal.enter begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
-    if pred (id,typ) then
+    if pf_apply pred gl (id,typ) then
       tac1 id
     else
       tac2 id
@@ -633,7 +633,7 @@ module New = struct
     (Proofview.Goal.enter begin fun gl ->
     let indclause = mk_clenv_from gl (c, t) in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim)  in
+    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim)  in
     let indmv =
       match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
@@ -741,7 +741,7 @@ module New = struct
 
   let elimination_then tac c =
     Proofview.Goal.enter begin fun gl ->
-    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
+    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
       | NotRecord -> true,gl_make_elim
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 31d26834d6..4b93b81d1c 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -222,7 +222,7 @@ module New : sig
 
   val nLastDecls  : Proofview.Goal.t -> int -> named_context
 
-  val ifOnHyp     : (Id.t * types -> bool) ->
+  val ifOnHyp : (Environ.env -> evar_map -> Id.t * types -> bool) ->
     (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) ->
     Id.t -> unit Proofview.tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f6f7c71dfd..609b752716 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -47,6 +47,9 @@ open Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
+let tclEVARS = Proofview.Unsafe.tclEVARS
+let tclEVARSTHEN sigma t = Proofview.tclTHEN (tclEVARS sigma) t
+
 let inj_with_occurrences e = (AllOccurrences,e)
 
 let typ_of env sigma c =
@@ -151,11 +154,12 @@ let convert_concl ~check ty k =
     Refine.refine ~typecheck:false begin fun sigma ->
       let sigma =
         if check then begin
-          ignore (Typing.unsafe_type_of env sigma ty);
+          let sigma, _ = Typing.type_of env sigma ty in
           match Reductionops.infer_conv env sigma ty conclty with
           | None -> error "Not convertible."
           | Some sigma -> sigma
-        end else sigma in
+        end else sigma
+      in
       let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
       (sigma, ans)
@@ -849,12 +853,13 @@ let change_on_subterm ~check cv_pb deep t where env sigma c =
             change_and_check Reduction.CONV mayneedglobalcheck true (t subst)
           else
             fun env sigma _c -> t subst env sigma) env sigma c in
-  if !mayneedglobalcheck then
+  let sigma = if !mayneedglobalcheck then
     begin
-      try ignore (Typing.unsafe_type_of env sigma c)
+      try fst (Typing.type_of env sigma c)
       with e when catchable_exception e ->
         error "Replacement would lead to an ill-typed term."
-    end;
+    end else sigma
+  in
   (sigma, c)
 
 let change_in_concl ~check occl t =
@@ -1308,30 +1313,23 @@ let cut c =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
-    let relevance =
-      try
-        (* Backward compat: ensure that [c] is well-typed. Plus we
-           need to know the relevance *)
-        let typ = Typing.unsafe_type_of env sigma c in
-        let typ = whd_all env sigma typ in
-        match EConstr.kind sigma typ with
-        | Sort s -> Some (Sorts.relevance_of_sort (ESorts.kind sigma s))
-        | _ -> None
-      with e when Pretype_errors.precatchable_exception e -> None
-    in
-    match relevance with
-    | Some r ->
+    (* Backward compat: ensure that [c] is well-typed. Plus we need to
+       know the relevance *)
+    match Typing.sort_of env sigma c with
+    | exception e when Pretype_errors.precatchable_exception e ->
+      Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
+    | sigma, s ->
+      let r = Sorts.relevance_of_sort s in
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
       (* Backward compat: normalize [c]. *)
       let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
-      Refine.refine ~typecheck:false begin fun h ->
-        let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
-        let (h, x) = Evarutil.new_evar env h c in
-        let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
-        (h, f)
-      end
-    | None ->
-      Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (Refine.refine ~typecheck:false begin fun h ->
+            let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
+            let (h, x) = Evarutil.new_evar env h c in
+            let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
+            (h, f)
+          end)
   end
 
 let error_uninstantiated_metas t clenv =
@@ -1533,16 +1531,19 @@ exception IsNonrec
 
 let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite
 
-let find_ind_eliminator ind s gl =
-  let env = Proofview.Goal.env gl in
+let find_ind_eliminator env sigma ind s =
   let gr = lookup_eliminator env ind s in
-  Tacmach.New.pf_apply Evd.fresh_global gl gr
+  Evd.fresh_global env sigma gr
 
 let find_eliminator c gl =
-  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  let sigma, t = Typing.type_of env sigma c in
+  let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
   if is_nonrec ind then raise IsNonrec;
-  let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
-    evd, { elimindex = None; elimbody = (c,NoBindings) }
+  let sigma, c = find_ind_eliminator env sigma ind (Retyping.get_sort_family_of env sigma concl) in
+    sigma, { elimindex = None; elimbody = (c,NoBindings) }
 
 let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
@@ -1928,18 +1929,20 @@ let apply_in_delayed_once ?(respect_opaque = false) with_delta
 
 let cut_and_apply c =
   Proofview.Goal.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 ->
-        let concl = Proofview.Goal.concl gl in
-        let env = Tacmach.New.pf_env gl in
-        Refine.refine ~typecheck:false begin fun sigma ->
-          let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in
-          let (sigma, f) = Evarutil.new_evar env sigma typ in
-          let (sigma, x) = Evarutil.new_evar env sigma c1 in
-          (sigma, mkApp (f, [|mkApp (c, [|x|])|]))
-        end
-      | _ -> error "lapply needs a non-dependent product."
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let concl = Proofview.Goal.concl gl in
+    let sigma, t = Typing.type_of env sigma c in
+    match EConstr.kind sigma (hnf_constr env sigma t) with
+    | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (Refine.refine ~typecheck:false begin fun sigma ->
+            let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in
+            let (sigma, f) = Evarutil.new_evar env sigma typ in
+            let (sigma, x) = Evarutil.new_evar env sigma c1 in
+            (sigma, mkApp (f, [|mkApp (c, [|x|])|]))
+          end)
+    | _ -> error "lapply needs a non-dependent product."
   end
 
 (********************************************************************)
@@ -2285,8 +2288,8 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented")
 
 let declare_intro_decomp_eq f = intro_decomp_eq_function := f
 
-let my_find_eq_data_decompose gl t =
-  try Some (find_eq_data_decompose gl t)
+let my_find_eq_data_decompose env sigma t =
+  try Some (find_eq_data_decompose env sigma t)
   with e when is_anomaly e
     (* Hack in case equality is not yet defined... one day, maybe,
        known equalities will be dynamically registered *)
@@ -2296,13 +2299,15 @@ let my_find_eq_data_decompose gl t =
 let intro_decomp_eq ?loc l thin tac id =
   Proofview.Goal.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
-  match my_find_eq_data_decompose gl t with
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma, t = Typing.type_of env sigma c in
+  let _,t = reduce_to_quantified_ind env sigma t in
+  match my_find_eq_data_decompose env sigma t with
   | Some (eq,u,eq_args) ->
     !intro_decomp_eq_function
-    (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
-    (eq,t,eq_args) (c, t)
+      (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
+      (eq,t,eq_args) (c, t)
   | None ->
     Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
   end
@@ -2310,16 +2315,19 @@ let intro_decomp_eq ?loc l thin tac id =
 let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
   Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_unsafe_type_of gl c in
-  let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma, t = Typing.type_of env sigma c in
+  let (ind,t) = reduce_to_quantified_ind env sigma t in
   let branchsigns = compute_constructor_signatures ~rec_flag:false ind in
   let nv_with_let = Array.map List.length branchsigns in
   let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
   let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
-  Tacticals.New.tclTHENLASTn
-    (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
-    (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
-       nv_with_let ll)
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (Tacticals.New.tclTHENLASTn
+       (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
+       (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
+          nv_with_let ll))
   end
 
 let rewrite_hyp_then assert_style with_evars thin l2r id tac =
@@ -2333,9 +2341,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
-    let type_of = Tacmach.New.pf_unsafe_type_of gl in
-    let whd_all = Tacmach.New.pf_apply whd_all gl in
-    let t = whd_all (type_of (mkVar id)) in
+    let sigma, t = Typing.type_of env sigma (mkVar id) in
+    let t = whd_all env sigma t in
     let eqtac, thin = match match_with_equality_type env sigma t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then
@@ -2361,7 +2368,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
         Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
         thin in
     (* Skip the side conditions of the rewriting step *)
-    Tacticals.New.tclTHENFIRST eqtac (tac thin)
+    tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin))
   end
 
 let prepare_naming ?loc = function
@@ -3392,8 +3399,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             let id = match EConstr.kind sigma c with
             | Var id -> id
             | _ ->
-            let type_of = Tacmach.New.pf_unsafe_type_of gl in
-            id_of_name_using_hdchar env sigma (type_of c) Anonymous in
+              let type_of = Tacmach.New.pf_get_type_of gl in
+              id_of_name_using_hdchar env sigma (type_of c) Anonymous
+            in
             let x = fresh_id_in_env avoid id env in
             Tacticals.New.tclTHEN
               (letin_tac None (Name x) c None allHypsAndConcl)
@@ -3794,15 +3802,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.New.project gl) in
   let env = Tacmach.New.pf_env gl in
   let concl = Tacmach.New.pf_concl gl in
+  let hyps = Proofview.Goal.hyps gl in
   let dep = dep || local_occur_var !sigma id concl in
   let avoid = ref Id.Set.empty in
   let get_id name =
-    let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
+    let id = fresh_id_in_env !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") env in
       avoid := Id.Set.add id !avoid; id
   in
     (* Build application generalized w.r.t. the argument plus the necessary eqs.
@@ -3811,14 +3819,14 @@ let abstract_args gl generalize_vars dep id defined f args =
 
        eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
     *)
-  let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
+  let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars) arg =
     let name, ty_relevance, ty, arity =
       let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
       let decl = List.hd rel in
       RelDecl.get_name decl, RelDecl.get_relevance decl, RelDecl.get_type decl, c
     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', argty = Typing.type_of env !sigma arg in
+    let sigma', ty = Evarsolve.refresh_universes (Some true) env sigma' ty in
     let () = sigma := sigma' in
     let lenctx = List.length ctx in
     let liftargty = lift lenctx argty in
@@ -3826,7 +3834,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       match EConstr.kind !sigma arg with
       | Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) ->
           (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls,
-          Id.Set.add id nongenvars, Id.Set.remove id vars, env)
+          Id.Set.add id nongenvars, Id.Set.remove id vars)
       | _ ->
           let name = get_id name in
           let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in
@@ -3848,7 +3856,7 @@ let abstract_args gl generalize_vars dep id defined f args =
           let refls = refl :: refls in
           let argvars = ids_of_constr !sigma vars arg in
             (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls,
-            nongenvars, Id.Set.union argvars vars, env)
+            nongenvars, Id.Set.union argvars vars)
   in
   let f', args' = decompose_indapp !sigma f args in
   let dogen, f', args' =
@@ -3862,15 +3870,16 @@ let abstract_args gl generalize_vars dep id defined f args =
               true, mkApp (f', before), after
   in
     if dogen then
-      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'
+      let sigma', tyf' = Typing.type_of env !sigma f' in
+      sigma := sigma';
+      let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars =
+        Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty) args'
       in
       let args, refls = List.rev args, List.rev refls in
       let vars =
         if generalize_vars then
           let nogen = Id.Set.add id nogen in
-            hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars
+            hyps_of_vars env !sigma hyps nogen vars
         else []
       in
       let body, c' =
@@ -3878,7 +3887,7 @@ let abstract_args gl generalize_vars dep id defined f args =
         else None, c'
       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 = make_abstract_generalize env 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)
     else None
@@ -4222,15 +4231,15 @@ let guess_elim isrec dep s hyp0 gl =
         let ind = EConstr.of_constr ind in
         (sigma, ind)
   in
-  let elimt = Typing.unsafe_type_of env sigma elimc in
-    sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
+  let sigma, elimt = Typing.type_of env sigma elimc in
+  sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let sigma = Tacmach.New.project gl in
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in
-  let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
-  Tacmach.New.project gl, (e, elimt), ind_type_guess
+  let sigma, elimt = Tacmach.New.pf_type_of gl elimc in
+  sigma, (e, elimt), ind_type_guess
 
 type scheme_signature =
     (Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array
@@ -4240,33 +4249,32 @@ type eliminator_source =
   | ElimOver of bool * Id.t
 
 let find_induction_type isrec elim hyp0 gl =
-  let sigma = Tacmach.New.project gl in
-  let scheme,elim =
+  let sigma, scheme,elim =
     match elim with
     | None ->
        let sort = Tacticals.New.elimination_sort_of_goal gl in
-       let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
+       let sigma, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
        let scheme = compute_elim_sig sigma ~elimc elimt in
        (* We drop the scheme waiting to know if it is dependent *)
-       scheme, ElimOver (isrec,hyp0)
+       sigma, scheme, ElimOver (isrec,hyp0)
     | Some e ->
-        let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
+        let sigma, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
         let scheme = compute_elim_sig sigma ~elimc elimt in
         if Option.is_empty scheme.indarg then error "Cannot find induction type";
-        let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
+        let indsign = compute_scheme_signature sigma scheme hyp0 ind_guess in
         let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
-        scheme, ElimUsing (elim,indsign)
+        sigma, scheme, ElimUsing (elim,indsign)
   in
   match scheme.indref with
   | None -> error_ind_scheme ""
-  | Some ref -> ref, scheme.nparams, elim
+  | Some ref -> sigma, (ref, scheme.nparams, elim)
 
 let get_elim_signature elim hyp0 gl =
   compute_elim_signature (given_elim hyp0 elim gl) hyp0
 
 let is_functional_induction elimc gl =
   let sigma = Tacmach.New.project gl in
-  let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
+  let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_get_type_of gl (fst elimc)) in
   (* The test is not safe: with non-functional induction on non-standard
      induction scheme, this may fail *)
   Option.is_empty scheme.indarg
@@ -4380,10 +4388,11 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
 
 let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps =
   Proofview.Goal.enter begin fun gl ->
-  let elim_info = find_induction_type isrec elim hyp0 gl in
-  atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
-    apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
-      (fun elim -> induction_tac with_evars [] [hyp0] elim))
+  let sigma, elim_info = find_induction_type isrec elim hyp0 gl in
+  tclEVARSTHEN sigma
+    (atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
+         apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
+           (fun elim -> induction_tac with_evars [] [hyp0] elim)))
   end
 
 let msg_not_right_number_induction_arguments scheme =
@@ -4658,18 +4667,16 @@ let induction_gen_l isrec with_evars elim names lc =
 
             | _ ->
                 Proofview.Goal.enter begin fun gl ->
-                let type_of = Tacmach.New.pf_unsafe_type_of gl in
-                let sigma = Tacmach.New.project gl in
-                Proofview.tclENV >>= fun env ->
-                let x =
-                  id_of_name_using_hdchar env sigma (type_of c) Anonymous in
-
+                let sigma, t = pf_apply Typing.type_of gl c in
+                let x = id_of_name_using_hdchar (Proofview.Goal.env gl) sigma t Anonymous in
                 let id = new_fresh_id Id.Set.empty x gl in
                 let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
                 let () = newlc:=id::!newlc in
-                Tacticals.New.tclTHEN
-                  (letin_tac None (Name id) c None allHypsAndConcl)
-                  (atomize_list newl')
+                Tacticals.New.tclTHENLIST [
+                  tclEVARS sigma;
+                  letin_tac None (Name id) c None allHypsAndConcl;
+                  atomize_list newl';
+                ]
                 end in
   Tacticals.New.tclTHENLIST
     [
@@ -4765,7 +4772,10 @@ let destruct ev clr c l e =
 
 let elim_scheme_type elim t =
   Proofview.Goal.enter begin fun gl ->
-  let clause = mk_clenv_type_of gl elim in
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma, elimt = Typing.type_of env sigma elim in
+  let clause = mk_clenv_from_env env sigma None (elim,elimt) in
   match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with
     | Meta mv ->
         let clause' =
@@ -4779,7 +4789,9 @@ let elim_scheme_type elim t =
 let elim_type t =
   Proofview.Goal.enter begin fun gl ->
   let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
-  let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
+  let evd, elimc = Tacmach.New.pf_apply find_ind_eliminator gl (fst ind)
+      (Tacticals.New.elimination_sort_of_goal gl)
+  in
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t)
   end
 
@@ -4857,7 +4869,8 @@ let prove_symmetry hdcncl eq_kind =
         Tacticals.New.onLastHyp simplest_case;
         one_constructor 1 NoBindings ])
 
-let match_with_equation sigma c =
+let match_with_equation c =
+  Proofview.tclEVARMAP >>= fun sigma ->
   Proofview.tclENV >>= fun env ->
   try
     let res = match_with_equation env sigma c in
@@ -4870,9 +4883,8 @@ let symmetry_red allowred =
   (* PL: usual symmetry don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let sigma = Tacmach.New.project gl in
   let concl = maybe_betadeltaiota_concl allowred gl in
-  match_with_equation sigma concl >>= fun with_eqn ->
+  match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
@@ -4894,25 +4906,25 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   Proofview.Goal.enter begin fun gl ->
-  let sigma = Tacmach.New.project gl in
-  let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
-  let sign,t = decompose_prod_assum sigma ctype in
-  Proofview.tclORELSE
-    begin
-      match_with_equation sigma t >>= fun (_,hdcncl,eq) ->
-        let symccl =
-          match eq with
-          | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
-          | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
-          | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
-        Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign))
-          [ intro_replacing id;
-            Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
-    end
-    begin function (e, info) -> match e with
-      | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
-      | e -> Proofview.tclZERO ~info e
-    end
+    let sigma, ctype = Tacmach.New.pf_type_of gl (mkVar id) in
+    let sign,t = decompose_prod_assum sigma ctype in
+    tclEVARSTHEN sigma
+      (Proofview.tclORELSE
+         begin
+           match_with_equation t >>= fun (_,hdcncl,eq) ->
+           let symccl =
+             match eq with
+             | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
+             | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
+             | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
+           Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign))
+             [ intro_replacing id;
+               Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
+         end
+         begin function (e, info) -> match e with
+           | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
+           | e -> Proofview.tclZERO ~info e
+         end)
   end
 
 let intros_symmetry =
@@ -4939,25 +4951,26 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
 (* This is probably not very useful any longer *)
 let prove_transitivity hdcncl eq_kind t =
   Proofview.Goal.enter begin fun gl ->
-  let (eq1,eq2) = match eq_kind with
-  | MonomorphicLeibnizEq (c1,c2) ->
-      mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
-  | PolymorphicLeibnizEq (typ,c1,c2) ->
-      mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])
-  | HeterogenousEq (typ1,c1,typ2,c2) ->
-      let env = Proofview.Goal.env gl in
-      let sigma = Tacmach.New.project gl in
-      let type_of = Typing.unsafe_type_of env sigma in
-      let typt = type_of t in
-        (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
-         mkApp(hdcncl, [| typt; t; typ2; c2 |]))
-  in
-  Tacticals.New.tclTHENFIRST (cut eq2)
-    (Tacticals.New.tclTHENFIRST (cut eq1)
-       (Tacticals.New.tclTHENLIST
-          [ Tacticals.New.tclDO 2 intro;
-            Tacticals.New.onLastHyp simplest_case;
-            assumption ]))
+    let sigma = Tacmach.New.project gl in
+    let sigma, eq1, eq2 = match eq_kind with
+      | MonomorphicLeibnizEq (c1,c2) ->
+        sigma, mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
+      | PolymorphicLeibnizEq (typ,c1,c2) ->
+        sigma, mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])
+      | HeterogenousEq (typ1,c1,typ2,c2) ->
+        let env = Proofview.Goal.env gl in
+        let sigma, typt = Typing.type_of env sigma t in
+        sigma,
+        mkApp(hdcncl, [| typ1; c1; typt ;t |]),
+        mkApp(hdcncl, [| typt; t; typ2; c2 |])
+    in
+    tclEVARSTHEN sigma
+      (Tacticals.New.tclTHENFIRST (cut eq2)
+         (Tacticals.New.tclTHENFIRST (cut eq1)
+            (Tacticals.New.tclTHENLIST
+               [ Tacticals.New.tclDO 2 intro;
+                 Tacticals.New.onLastHyp simplest_case;
+                 assumption ])))
   end
 
 let transitivity_red allowred t =
@@ -4965,9 +4978,8 @@ let transitivity_red allowred t =
   (* PL: usual transitivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let sigma = Tacmach.New.project gl in
   let concl = maybe_betadeltaiota_concl allowred gl in
-  match_with_equation sigma concl >>= fun with_eqn ->
+  match_with_equation concl >>= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f954915cf8..6bdb3159cf 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -395,7 +395,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
 
   in
   Proofview.Goal.enter begin fun gl ->
-    let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
+    let type_of_pq = Tacmach.New.pf_get_type_of gl p in
     let sigma = Tacmach.New.project gl in
     let env = Tacmach.New.pf_env gl in
     let u,v = destruct_ind env sigma type_of_pq
@@ -458,11 +458,11 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
         Proofview.Goal.enter begin fun gl ->
-        let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         let sigma = Tacmach.New.project gl in
         let env = Tacmach.New.pf_env gl in
         if EConstr.eq_constr sigma t1 t2 then aux q1 q2
         else (
+          let tt1 = Tacmach.New.pf_get_type_of gl t1 in
           let u,v = try destruct_ind env sigma tt1
           (* trick so that the good sequence is returned*)
                 with e when CErrors.noncritical e -> indu,[||]
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 56ab6f289d..2c582da495 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -198,10 +198,9 @@ let build_id_coercion idf_opt source poly =
       lams
   in
   (* juste pour verification *)
-  let _ =
-    if not
-      (Reductionops.is_conv_leq env sigma
-        (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f))
+  let sigma, val_t = Typing.type_of env sigma (EConstr.of_constr val_f) in
+  let () =
+    if not (Reductionops.is_conv_leq env sigma val_t (EConstr.of_constr typ_f))
     then
       user_err  (strbrk
         "Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index d48e2139d1..84f8578ad4 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -127,7 +127,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in
-  let relty = Typing.unsafe_type_of env sigma rel in
+  let relty = Retyping.get_type_of env sigma rel in
   let relargty =
     let error () =
       user_err ?loc:(constr_loc r)