Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of)

3 files changed, 4 insertions, 8 deletions

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 *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 827f44ec1e..609b752716 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4772,7 +4772,10 @@ let destruct ev clr c l e =
 
 let elim_scheme_type elim t =
   Proofview.Goal.enter begin fun gl ->
-  let clause = mk_clenv_type_of gl elim in
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma, elimt = Typing.type_of env sigma elim in
+  let clause = mk_clenv_from_env env sigma None (elim,elimt) in
   match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with
     | Meta mv ->
         let clause' =