From 44d70e3e7d1101018dee45008b949c91d337438f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 14:33:11 +0100
Subject: unsafe_type_of -> type_of in Unification.applyHead

We already thread the evar map
---
 pretyping/unification.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3