From 791797fce5e11b83b88e6b869678ee7c39703043 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 20:16:37 +0100
Subject: unsafe_type_of -> type_of in Rewrite.resolve_morphism

---
 plugins/ltac/rewrite.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d630e9bd4..7cb359b8cd 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -789,7 +789,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
     let morphargs, morphobjs = Array.chop first args in
     let morphargs', morphobjs' = Array.chop first args' in
     let appm = mkApp(m, morphargs) in
-    let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
+    let evd, appmtype = Typing.type_of env (goalevars evars) appm in
+    let evars = evd, snd evars in
     let cstrs = List.map
       (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
       (Array.to_list morphobjs')
-- 
cgit v1.2.3