From 6bf68189b74fed332a064257b9f1b7e46b6309b5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:37:18 +0100
Subject: unsafe_type_of -> type_of in Celenv.mk_clenv_type_of

---
 proofs/clenv.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index e466992721..bb660adf4d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -128,7 +128,11 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
+let mk_clenv_type_of gls t =
+  let env = Proofview.Goal.env gls in
+  let sigma = Tacmach.New.project gls in
+  let sigma, tt = Typing.type_of env sigma t in
+  mk_clenv_from_env env sigma None (t,tt)
 
 (******************************************************************)
 
-- 
cgit v1.2.3


From 48b142d0e915e946274c14ab354f174cc5b6df51 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:41:49 +0100
Subject: Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of)

---
 proofs/clenv.ml  | 6 ------
 proofs/clenv.mli | 1 -
 2 files changed, 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index bb660adf4d..b0eb8dc646 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -128,12 +128,6 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t =
-  let env = Proofview.Goal.env gls in
-  let sigma = Tacmach.New.project gls in
-  let sigma, tt = Typing.type_of env sigma t in
-  mk_clenv_from_env env sigma None (t,tt)
-
 (******************************************************************)
 
 (* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 3fca967395..7213c9318c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -46,7 +46,6 @@ val clenv_meta_type : clausenv -> metavariable -> types
 val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
   Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
 (** Refresh the universes in a clenv *)
-- 
cgit v1.2.3


From ebd1c087298a50f85d3f227452b8a3d1fb7a625c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:43:23 +0100
Subject: unsafe_type_of -> type_of in Logic.check_typability

---
 proofs/logic.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index a361c4208e..bac13fcfc3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -79,7 +79,7 @@ let check = ref false
 let with_check = Flags.with_option check
 
 let check_typability env sigma c =
-  if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
+  if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma
 
 (************************************************************************)
 (************************************************************************)
@@ -363,7 +363,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
           gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
-        check_typability env sigma ty;
+        let sigma = check_typability env sigma ty in
         let sigma = check_conv_leq_goal env sigma trm ty conclty in
         let res = mk_refgoals sigma goal goalacc ty t in
         (* we keep the casts (in particular VMcast and NATIVEcast) except
@@ -430,13 +430,13 @@ and mk_hdgoals sigma goal goalacc trm =
     Goal.V82.mk_goal sigma hyps concl in
   match kind trm with
     | Cast (c,_, ty) when isMeta c ->
-        check_typability env sigma ty;
+        let sigma = check_typability env sigma ty in
         let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
         let ev = EConstr.Unsafe.to_constr ev in
         gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
-        check_typability env sigma ty;
+        let sigma = check_typability env sigma ty in
         mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
-- 
cgit v1.2.3