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.

3 files changed, 5 insertions, 5 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 96bb89e2a..f90508090 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -355,7 +355,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
       )
   in
   Proofview.Goal.nf_enter begin fun gl ->
-    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in
+    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
@@ -417,7 +417,7 @@ 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_type_of gl t1 in
+        let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind tt1
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6a485d52c..0e270f960 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly =
   let _ =
     if not
       (Reductionops.is_conv_leq env Evd.empty
-	(Typing.type_of env Evd.empty val_f) typ_f)
+	(Typing.unsafe_type_of env Evd.empty val_f) typ_f)
     then
       errorlabstrm "" (strbrk
 	"Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1249581ee..7cf0477f9 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -847,7 +847,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
   let () = check_evars_are_solved env !evdref (Evd.empty,!evdref)  in
-  let relty = Typing.type_of env !evdref rel in
+  let relty = Typing.unsafe_type_of env !evdref rel in
   let relargty =
     let error () =
       user_err_loc (constr_loc r,
@@ -988,7 +988,7 @@ let interp_recursive isfix fixl notations =
     List.fold_left2
       (fun env' id t ->
 	 if Flags.is_program_mode () then
-	   let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in
+	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
 	   let fixprot =
 	     try 
 	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in