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(-)

(limited to 'vernac')

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


From 702b4e1cc3e93f26a5215e6018bd744ec25fdb55 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:32:16 +0100
Subject: unsafe_type_of -> get_type_of in Auto_ind_decl.do_replace_bl

---
 vernac/auto_ind_decl.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f954915cf8..6bdb3159cf 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -395,7 +395,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
 
   in
   Proofview.Goal.enter begin fun gl ->
-    let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
+    let type_of_pq = Tacmach.New.pf_get_type_of gl p in
     let sigma = Tacmach.New.project gl in
     let env = Tacmach.New.pf_env gl in
     let u,v = destruct_ind env sigma type_of_pq
@@ -458,11 +458,11 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
         Proofview.Goal.enter begin fun gl ->
-        let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         let sigma = Tacmach.New.project gl in
         let env = Tacmach.New.pf_env gl in
         if EConstr.eq_constr sigma t1 t2 then aux q1 q2
         else (
+          let tt1 = Tacmach.New.pf_get_type_of gl t1 in
           let u,v = try destruct_ind env sigma tt1
           (* trick so that the good sequence is returned*)
                 with e when CErrors.noncritical e -> indu,[||]
-- 
cgit v1.2.3


From 15387f4e32d7eac580b53b3c6424aace4796c363 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:35:47 +0100
Subject: unsafe_type_of -> type_of in ComCoercion.build_id_coercion

---
 vernac/comCoercion.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 56ab6f289d..2c582da495 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -198,10 +198,9 @@ let build_id_coercion idf_opt source poly =
       lams
   in
   (* juste pour verification *)
-  let _ =
-    if not
-      (Reductionops.is_conv_leq env sigma
-        (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f))
+  let sigma, val_t = Typing.type_of env sigma (EConstr.of_constr val_f) in
+  let () =
+    if not (Reductionops.is_conv_leq env sigma val_t (EConstr.of_constr typ_f))
     then
       user_err  (strbrk
         "Cannot be defined as coercion (maybe a bad number of arguments).")
-- 
cgit v1.2.3