From b8fb594259f7abaedc4e335cfd8eacd0508fffcf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 20:22:13 +0100
Subject: unsafe_type_of -> type_of in Rewrite.build_morphism_signature

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

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7cb359b8cd..a52d03c57a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1907,7 +1907,7 @@ let declare_projection n instance_id r =
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
   let sigma = Evd.from_ctx ctx in
-  let t = Typing.unsafe_type_of env sigma m in
+  let t = Retyping.get_type_of env sigma m in
   let cstrs =
     let rec aux t =
       match EConstr.kind sigma t with
-- 
cgit v1.2.3