From 5112af4fd5df24b7272e69affcbb88edf1474b82 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 14:30:08 +0100
Subject: unsafe_type_of -> get_type_of in cases

It goes in an error message so should be fine.
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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