From 53cabaf1e26bfc13e5a45dfeb90ad6a858344c32 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:11:07 +0100
Subject: unsafe_type_of -> get_type_of in Equality.build_injrec

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0eb0a30486..de7e755e5a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1311,7 +1311,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
+  | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
-- 
cgit v1.2.3