Merge PR #11538: Remove many unsafe_type_of uses

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

16 files changed, 157 insertions, 152 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 [