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.

4 files changed, 11 insertions, 5 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 2c9c695bfd..a2cccc0e0b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -28,7 +28,7 @@ open Misctypes
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
+let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 898588d9e4..5c48995fc7 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 =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fa0d03623c..4238d1e372 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -84,6 +84,7 @@ let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_unsafe_type_of            = pf_reduce unsafe_type_of
 let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
@@ -172,6 +173,9 @@ module New = struct
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
 
+  let pf_unsafe_type_of gl t =
+    pf_apply unsafe_type_of gl t
+
   let pf_type_of gl t =
     pf_apply type_of gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f7fc6b54f1..a0e1a01577 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,7 +41,8 @@ val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
-val pf_type_of            : goal sigma -> constr -> types
+val pf_unsafe_type_of            : goal sigma -> constr -> types
+val pf_type_of            : goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
 val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
@@ -112,7 +113,8 @@ module New : sig
   val pf_env : 'a Proofview.Goal.t -> Environ.env
   val pf_concl : [ `NF ] Proofview.Goal.t -> types
 
-  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types
   val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
   val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier