Merge PR #11538: Remove many unsafe_type_of uses

Reviewed-by: Matafou
Reviewed-by: gares
Reviewed-by: ppedrot

6 files changed, 15 insertions, 7 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index cbd04a76ad..29d6726262 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2164,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid =
         let IndType (indf, _) =
           try find_rectype env sigma (lift (-(List.length realargs)) ty)
           with Not_found -> error_case_not_inductive env sigma
-            {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty}
+            {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty}
         in
         let (ind,u), params = dest_ind_family indf in
         let params = List.map EConstr.of_constr params in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bf61d44a10..cb0c4868b5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -446,7 +446,7 @@ let pretype_ref ?loc sigma env ref us =
          Pretype_errors.error_var_not_found ?loc !!env sigma id)
   | ref ->
     let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
-    let ty = unsafe_type_of !!env sigma c in
+    let sigma, ty = type_of !!env sigma c in
     sigma, make_judge c ty
 
 let interp_sort ?loc evd : glob_sort -> _ = function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 10e8cf7e0f..f87c50b5e4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
 let pattern_occs loccs_trm = begin fun env sigma c ->
   let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
   try
-    let _ = Typing.unsafe_type_of env sigma abstr_trm in
+    let sigma, _ = Typing.type_of env sigma abstr_trm in
     (sigma, applist(abstr_trm, List.map snd loccs_trm))
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index a15134f58d..4582844b71 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -253,6 +253,9 @@ let judge_of_type u =
 let judge_of_relative env v =
   Environ.on_judgment EConstr.of_constr (judge_of_relative env v)
 
+let type_of_variable env id =
+  EConstr.of_constr (type_of_variable env id)
+
 let judge_of_variable env id =
   Environ.on_judgment EConstr.of_constr (judge_of_variable env id)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1b07b2bb78..fd2dc7c2fc 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -30,6 +30,9 @@ val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
 (** Typecheck a term has a given type (assuming the type is OK) *)
 val check : env -> evar_map -> constr -> types -> evar_map
 
+(** Type of a variable. *)
+val type_of_variable : env -> variable -> types
+
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6486435ca2..2157c4ef6a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1274,12 +1274,14 @@ let applyHead env evd n c  =
     else
       match EConstr.kind evd (whd_all env evd cty) with
       | Prod (_,c1,c2) ->
-        let (evd',evar) =
-      Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
-      apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
+        let (evd,evar) =
+          Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1
+        in
+        apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd
       | _ -> user_err Pp.(str "Apply_Head_Then")
   in
-    apprec n c (Typing.unsafe_type_of env evd c) evd
+  let evd, t = Typing.type_of env evd c in
+  apprec n c t evd
 
 let is_mimick_head sigma ts f =
   match EConstr.kind sigma f with