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.

1 files changed, 5 insertions, 5 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 36273faae..714cd8634 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