From b6f372dd4eba2a63791aae899fbae7b8aa3aa499 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:18:36 +0100
Subject: unsafe_type_of -> get_type_of in ComProgramFixpoint.build_wellfounded

We typecheck it literally the previous line...
---
 vernac/comProgramFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index d48e2139d1..84f8578ad4 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -127,7 +127,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in
-  let relty = Typing.unsafe_type_of env sigma rel in
+  let relty = Retyping.get_type_of env sigma rel in
   let relargty =
     let error () =
       user_err ?loc:(constr_loc r)
-- 
cgit v1.2.3