Safer typing primitives.

Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.

- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.

All uses of unsafe_* functions should be eventually eliminated.

14 files changed, 72 insertions, 72 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 29bca8622b..d5d6bdf749 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -513,7 +513,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_type_of state.gls trm in
+	  let typ = pf_unsafe_type_of state.gls trm in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -836,7 +836,7 @@ let complete_one_class state i=
 	    let _,etyp,rest= destProd typ in
 	    let id = new_state_var etyp state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
-	let _c = pf_type_of state.gls
+	let _c = pf_unsafe_type_of state.gls
 	  (constr_of_term (term state.uf pac.cnode)) in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 9952cb0807..9c3a0f7299 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -255,13 +255,13 @@ let new_refine c = Proofview.V82.tactic (refine c)
 
 let assert_before n c =
   Proofview.Goal.enter begin fun gl ->
-    let evm, _ = Tacmach.New.pf_apply e_type_of gl c in
+    let evm, _ = Tacmach.New.pf_apply type_of gl c in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end
     
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter begin fun gl ->
-  let type_of t = Tacmach.New.pf_type_of gl t in
+  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 c
@@ -331,7 +331,7 @@ let refute_tac c t1 t2 p =
   Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let intype =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
   in
   let neweq= new_app_global _eq [|intype;tt1;tt2|] in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
@@ -341,14 +341,14 @@ let refute_tac c t1 t2 p =
   end
 
 let refine_exact_check c gl =
-  let evm, _ = pf_apply e_type_of gl c in
+  let evm, _ = pf_apply type_of gl c in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
 let convert_to_goal_tac c t1 t2 p = 
   Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let sort =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
   in
   let neweq= new_app_global _eq [|sort;tt1;tt2|] in
   let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
@@ -373,7 +373,7 @@ let discriminate_tac (cstr,u as cstru) p =
   Proofview.Goal.nf_enter begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
     let intype =
-      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl
+      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
     in
     let concl = Proofview.Goal.concl gl in
     (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
@@ -382,7 +382,7 @@ let discriminate_tac (cstr,u as cstru) p =
     (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
     (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
     let identity = Universes.constr_of_global (Lazy.force _I) in
-    (* let trivial=pf_type_of gls identity in *)
+    (* let trivial=pf_unsafe_type_of gls identity in *)
     let trivial = Universes.constr_of_global (Lazy.force _True) in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
     let outtype = mkSort outtype in
@@ -486,7 +486,7 @@ let congruence_tac depth l =
 let f_equal =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let type_of = Tacmach.New.pf_type_of gl in
+    let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         let ty = (* Termops.refresh_universes *) (type_of c1) in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 36273faae2..714cd86341 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -773,7 +773,7 @@ let rec take_tac wits gls =
   match wits with
       [] -> tclIDTAC gls
     | wit::rest ->
-	let typ = pf_type_of gls wit in
+	let typ = pf_unsafe_type_of gls wit in
 	  tclTHEN (thus_tac wit typ []) (take_tac rest)  gls
 
 
@@ -854,7 +854,7 @@ let start_tree env ind rp =
 let build_per_info etype casee gls =
   let concl=pf_concl gls in
   let env=pf_env gls in
-  let ctyp=pf_type_of gls casee in
+  let ctyp=pf_unsafe_type_of gls casee in
   let is_dep = dependent casee concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
   let (ind,u) =
@@ -869,7 +869,7 @@ let build_per_info etype casee gls =
       | _ -> mind.mind_nparams,None in
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
-    let typ=pf_type_of gls c in
+    let typ=pf_unsafe_type_of gls c in
       lambda_create env (typ,subst_term c body) in
   let pred= List.fold_right abstract_obj
     real_args (lambda_create env (ctyp,subst_term casee concl)) in
@@ -1228,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let nparams = mind.mind_nparams in
 	let concl=pf_concl gls in
 	let env=pf_env gls in
-	let ctyp=pf_type_of gls casee in
+	let ctyp=pf_unsafe_type_of gls casee in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
 	let ind', u = destInd hd in
 	let _ = assert (eq_ind ind' ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
-	  let typ=pf_type_of gls c in
+	  let typ=pf_unsafe_type_of gls c in
 	    lambda_create env (typ,subst_term c body) in
 	let elim_pred = List.fold_right abstract_obj
 	  real_args (lambda_create env (ctyp,subst_term casee concl)) in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 5912f0a0c3..c80a8081a3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -105,7 +105,7 @@ let mk_open_instance id idc gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_type_of gl idc in
+      let typ=pf_unsafe_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
@@ -154,7 +154,7 @@ let left_instance_tac (inst,id) continue seq=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
-		    try Typing.e_type_of (pf_env gl) evmap gt
+		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when Errors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 802af04d06..96c4eb01eb 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl =
   let l = expand_constructor_hints l in
   let f gr (seq,gl) =
     let gl, c = pf_eapply Evd.fresh_global gl gr in
-    let typ=(pf_type_of gl c) in
+    let typ=(pf_unsafe_type_of gl c) in
       (add_formula Hyp gr typ seq gl,gl) in
     List.fold_right f l (seq,gl)
 
@@ -214,7 +214,7 @@ let extend_with_auto_hints l seq gl=
       | Res_pf_THEN_trivial_fail (c,_) ->
 	  (try
 	     let gr = global_of_constr c in
-	     let typ=(pf_type_of gl c) in
+	     let typ=(pf_unsafe_type_of gl c) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4a832435f8..169a706005 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -328,7 +328,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
 	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
-	   let evm, _ = pf_apply Typing.e_type_of g to_refine in
+	   let evm, _ = pf_apply Typing.type_of g to_refine in
 	     tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
 	)
     in
@@ -543,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       tclIDTAC
   in
   try
-    scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id]
+    scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -593,7 +593,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
 	observe_tac "after_introduction" (fun g' ->
 	   (* We get infos on the equations introduced*)
-	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
+	   let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
 	   (* compute the new value of the body *)
 	   let new_term_value =
 	     match kind_of_term new_term_value_eq with
@@ -606,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
-		    pf_type_of g' term,
+		    pf_unsafe_type_of g' term,
 		    Termops.replace_term term (mkRel 1) dyn_infos.info
 		   )
 	 in
@@ -638,7 +638,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  let c = mkApp(mkVar hid,args) in
-	  let evm, _ = pf_apply Typing.e_type_of g c in
+	  let evm, _ = pf_apply Typing.type_of g c in
 	  tclTHENLIST[
             Refiner.tclEVARS evm;
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -699,7 +699,7 @@ let build_proof
 		  let dyn_infos = {dyn_info' with info =
 		      mkCase(ci,ct,t,cb)} in
 		  let g_nb_prod = nb_prod (pf_concl g) in
-		  let type_of_term = pf_type_of g t in
+		  let type_of_term = pf_unsafe_type_of g t in
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
@@ -919,7 +919,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_type_of g (mkVar hyp) in
+  let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
   let to_revert,_ =
     Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
       if Id.List.mem hyp hyps
@@ -964,7 +964,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
   (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let (type_ctxt,type_of_f),evd =
-    let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f
+    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
     in 
     decompose_prod_n_assum
       (nb_params + nb_args) t,evd
@@ -1034,8 +1034,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Global.env ()) !evd
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
-      let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in 
-      evd:=evd';		       
+      evd:=evd';                       
+      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
       res
   in
   let nb_intro_to_do = nb_prod (pf_concl g) in
@@ -1414,7 +1414,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 (pf_type_of gls (mkVar hrec)) in
+    let _,hrec_concl  = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in
     let f_app = Array.last (snd (destApp hrec_concl)) in
     let f =  (fst (destApp f_app)) in
     let rec backtrack : tactic =
@@ -1641,7 +1641,7 @@ let prove_principle_for_gen
 (*       (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 " *) (fix (Some fix_id) (List.length args_ids + 1));
-(*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
+(*       (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); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
       (* observe_tac "finish" *) (fun gl' ->
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a2bbf97ae3..3edc590ccc 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -274,7 +274,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
-  let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in
+  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
@@ -327,7 +327,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	let s = Universes.new_sort_in_family fam_sort in
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
-	let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in
+	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
 	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
 	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in
 	ignore(
@@ -478,7 +478,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
   in
   let _ = evd := sigma in 
   let l_schemes =
-    List.map (Typing.type_of env sigma) schemes
+    List.map (Typing.unsafe_type_of env sigma) schemes
   in
   let i = ref (-1) in
   let sorts =
@@ -608,8 +608,8 @@ let build_scheme fas =
                   (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
-	    let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in 
-	    let _ = evd := evd' in 
+            let _ = evd := evd' in 
+	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in 
 	    (destConst f,sort)
 	 )
 	 fas
@@ -659,7 +659,7 @@ let build_case_scheme fa =
   in
   let sigma, scheme = 
     (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun in
-  let scheme_type =  (Typing.type_of env sigma ) scheme in
+  let scheme_type =  (Typing.unsafe_type_of env sigma ) scheme in
   let sorts =
     (fun (_,_,x) ->
        Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 043d4328c4..61f03d6f22 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -321,7 +321,7 @@ let mkEq typ c1 c2 =
 
 
 let poseq_unsafe idunsafe cstr gl =
-  let typ = Tacmach.pf_type_of gl cstr in
+  let typ = Tacmach.pf_unsafe_type_of gl cstr in
   tclTHEN
     (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl))
     (tclTHENFIRST
@@ -349,7 +349,7 @@ let rec poseq_list_ids_rec lcstr gl =
 	      let _ = prstr "c = " in
 	      let _ = prconstr c in
 	      let _ = prstr "\n" in
-	      let typ = Tacmach.pf_type_of gl c in
+	      let typ = Tacmach.pf_unsafe_type_of gl c in
 	      let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in
 	      let x = Tactics.fresh_id [] cname gl in
 	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
@@ -478,8 +478,8 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
 	 (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
        let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty
 	 (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
-       let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
-       let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
+       let f1type = Typing.unsafe_type_of (Global.env()) Evd.empty f1 in
+       let f2type = Typing.unsafe_type_of (Global.env()) Evd.empty f2 in
        let ar1 = List.length (fst (decompose_prod f1type)) in
        let ar2 = List.length (fst (decompose_prod f2type)) in
        let _ =
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 9e3f398633..065c12a2d7 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -487,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		   The "value" of this branch is then simply [res]
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
-		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
+		let rt_typ = Typing.unsafe_type_of env Evd.empty rt_as_constr in
 		let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
@@ -595,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	*)
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env Evd.empty v in
-	let v_type = Typing.type_of env Evd.empty v_as_constr in
+	let v_type = Typing.unsafe_type_of env Evd.empty v_as_constr in
 	let new_env =
 	  match n with
 	      Anonymous -> env
@@ -611,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
 	let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
-	let b_typ = Typing.type_of env Evd.empty b_as_constr in
+	let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in
 	let (ind,_) =
 	  try Inductiveops.find_inductive env Evd.empty b_typ
 	  with Not_found ->
@@ -643,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	      nal
 	  in
 	  let b_as_constr,ctx = Pretyping.understand env Evd.empty b in
-	  let b_typ = Typing.type_of env Evd.empty b_as_constr in
+	  let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env Evd.empty b_typ
 	    with Not_found ->
@@ -690,7 +690,7 @@ and build_entry_lc_from_case env funname make_discr
 	let types =
 	  List.map (fun (case_arg,_) ->
 		      let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in
-		      Typing.type_of env Evd.empty case_arg_as_constr
+		      Typing.unsafe_type_of env Evd.empty case_arg_as_constr
 		   ) el
 	in
 	(****** The next works only if the match is not dependent ****)
@@ -737,7 +737,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		   List.fold_right
 		     (fun id acc ->
 			let typ_of_id =
-			  Typing.type_of env_with_pat_ids Evd.empty (mkVar id)
+			  Typing.unsafe_type_of env_with_pat_ids Evd.empty (mkVar id)
 			in
 			let raw_typ_of_id =
 			  Detyping.detype false []
@@ -791,7 +791,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		   (fun id  acc ->
 		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
-		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
+		      let typ_of_id = Typing.unsafe_type_of new_env Evd.empty (mkVar id) in
 		      let raw_typ_of_id =
 			Detyping.detype false [] new_env Evd.empty typ_of_id
 		      in
@@ -1105,7 +1105,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let t',ctx = Pretyping.understand env Evd.empty t in
-	  let type_t' = Typing.type_of env Evd.empty t' in
+	  let type_t' = Typing.unsafe_type_of env Evd.empty t' in
 	  let new_env = Environ.push_rel (n,Some t',type_t') env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
@@ -1255,7 +1255,7 @@ let do_build_inductive
   let evd,env =
     Array.fold_right2
       (fun id c (evd,env) ->
-       let evd,t = Typing.e_type_of env evd (mkConstU c) in
+       let evd,t = Typing.type_of env evd (mkConstU c) in
        evd,
        Environ.push_named (id,None,t)
 			   (* try *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e211b68837..5dcb0c0439 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -72,11 +72,11 @@ let functional_induction with_clean c princl pat =
 		    errorlabstrm "" (str "Cannot find induction principle for "
 				     ++Printer.pr_lconstr (mkConst c') )
 	      in
-	      (princ,NoBindings, Tacmach.pf_type_of g' princ,g')
+	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
 	   | _ -> raise (UserError("",str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
-	 princ,binding,Tacmach.pf_type_of g princ,g
+	 princ,binding,Tacmach.pf_unsafe_type_of g princ,g
     in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     let args_as_induction_constr =
@@ -356,8 +356,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	    (fun i x ->
 	     let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
 	     let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in
-	     let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in
-	     let _ = evd := evd' in 
+             let _ = evd := evd' in 
+	     let princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd uprinc in
     	     Functional_principles_types.generate_functional_principle
 	       evd
 		 interactive_proof
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d10924f886..89ceb751a4 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -127,8 +127,8 @@ let generate_type evd g_to_f f graph i =
   let evd',graph =
     Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
   in
-  let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in
   evd:=evd';
+  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -193,7 +193,7 @@ let find_induction_principle evd f =
     | None -> raise Not_found
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
-       let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
        evd:=evd';
        rect_lemma,typ
 
@@ -296,7 +296,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let constructor_args g =
 	List.fold_right 
 	  (fun hid acc ->
-	     let type_of_hid = pf_type_of g (mkVar hid) in
+	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
 	     match kind_of_term type_of_hid with
 	       | Prod(_,_,t') ->
 		   begin
@@ -440,7 +440,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     "functional_induction" (
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true)  gl term in
+		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
 		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -577,7 +577,7 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match kind_of_term  (pf_type_of g (mkVar id)) with
+	       match kind_of_term  (pf_unsafe_type_of g (mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -642,7 +642,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = nf_zeta schemes.(i)  in
-    let princ_type = pf_type_of g graph_principle in
+    let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
@@ -772,7 +772,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in 
+	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
 	   let type_of_lemma = nf_zeta type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
@@ -900,7 +900,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
 let revert_graph kn post_tac hid g =
-    let typ = pf_type_of g (mkVar hid) in
+    let typ = pf_unsafe_type_of g (mkVar hid) in
     match kind_of_term typ with
       | App(i,args) when isInd i ->
 	  let ((kn',num) as ind'),u = destInd i in
@@ -951,7 +951,7 @@ let revert_graph kn post_tac hid g =
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let type_of_h = pf_type_of g (mkVar hid) in
+    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
     match kind_of_term type_of_h with
       | App(eq,args) when eq_constr eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
@@ -1003,7 +1003,7 @@ let invfun qhyp f g =
        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
-	     let hyp_typ = pf_type_of g (mkVar hid)  in
+	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
 	     match kind_of_term hyp_typ with
 	       | App(eq,args) when eq_constr eq (make_eq ()) ->
 		   begin
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b9902a9fc7..d3979748e1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -115,7 +115,7 @@ let pf_get_new_ids idl g =
 
 let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (pf_type_of gls c)
+    (pf_unsafe_type_of gls c)
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -400,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    thin to_intros;
 	    h_intros to_intros;
 	    (fun g' -> 
-	      let ty_teq = pf_type_of g' (mkVar heq) in
+	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
 	      let teq_lhs,teq_rhs =
 		let _,args = try destApp ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
@@ -514,13 +514,13 @@ let rec prove_lt hyple g =
       in
       let h =
 	List.find (fun id ->
-          match decompose_app (pf_type_of g (mkVar id)) with
+          match decompose_app (pf_unsafe_type_of g (mkVar id)) with
             | _, t::_ -> eq_constr t varx
             | _ -> false
 	) hyple
       in
       let y =
-	List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
+	List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in
       observe_tclTHENLIST (str "prove_lt1")[
 	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
 	observe_tac (str "prove_lt") (prove_lt hyple)
@@ -655,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} 
 
 let pf_type c tac gl = 
-  let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in
+  let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
     tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
 
 let pf_typel l tac =
@@ -680,7 +680,7 @@ let mkDestructEq :
         if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let type_of_expr = pf_type_of g expr 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
     pf_typel new_hyps (fun _ ->
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4e2696dfdb..710a2394d3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1689,7 +1689,7 @@ let onClearedName2 id tac =
 
 let destructure_hyps =
   Proofview.Goal.nf_enter begin fun gl ->
-  let type_of = Tacmach.New.pf_type_of gl in
+  let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let decidability = Tacmach.New.of_old decidability gl in
   let pf_nf = Tacmach.New.of_old pf_nf gl in
     let rec loop = function
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2f9e8509c2..e590958ccf 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -162,7 +162,7 @@ let ic_unsafe c = (*FIXME remove *)
   let env = Global.env() and sigma = Evd.empty in
     fst (Constrintern.interp_constr env sigma c)
 
-let ty c = Typing.type_of (Global.env()) Evd.empty c
+let ty c = Typing.unsafe_type_of (Global.env()) Evd.empty c
 
 let decl_constant na ctx c =
   let vars = Universes.universes_of_constr c in