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, 2 insertions, 2 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 898588d9e..5c48995fc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -83,7 +83,7 @@ let apply_to_hyp sign id f =
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma c in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -317,7 +317,7 @@ let meta_free_prefix a =
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then type_of env sigma c
+  if !check then unsafe_type_of env sigma c
   else Retyping.get_type_of env sigma c
 
 let rec mk_refgoals sigma goal goalacc conclty trm =