From c22ac10752c12bcb23402ad29a73f2d9699248a6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 15:03:10 +0200
Subject: Deprecate Typing.e_* functions

---
 plugins/ltac/evar_tactics.ml | 4 +---
 plugins/ltac/rewrite.ml      | 7 +++----
 plugins/ltac/tacinterp.ml    | 6 ++----
 3 files changed, 6 insertions(+), 11 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 9382f567b..fb6be430f 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -85,9 +85,7 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    let sigma = ref sigma in
-    let _ = Typing.e_sort_of env sigma typ in
-    let sigma = !sigma in
+    let sigma, _ = Typing.sort_of env sigma typ in
     let id = match name with
     | Name.Anonymous ->
       let id = Namegen.id_of_name_using_hdchar env sigma typ name in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9eb55aa5e..1b86583da 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -104,9 +104,8 @@ let extends_undefined evars evars' =
 
 let app_poly_check env evars f args =
   let (evars, cstrs), fc = f evars in
-  let evdref = ref evars in 
-  let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
-    (!evdref, cstrs), t
+  let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in
+  (evars, cstrs), t
 
 let app_poly_nocheck env evars f args =
   let evars, fc = f evars in 
@@ -1469,8 +1468,8 @@ exception RewriteFailure of Pp.t
 type result = (evar_map * constr option * types) option option
 
 let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
+  let sigma, sort = Typing.sort_of env sigma concl in
   let evdref = ref sigma in
-  let sort = Typing.e_sort_of env evdref concl in
   let evars = (!evdref, Evar.Set.empty) in
   let evars, cstr =
     let prop, (evars, arrow) = 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 84049d4ed..a93cf5ae7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -691,11 +691,9 @@ let interp_may_eval f ist env sigma = function
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
 	let ctxt = EConstr.Unsafe.to_constr ctxt in
-	let evdref = ref sigma in
-	let ic = EConstr.Unsafe.to_constr ic in
+        let ic = EConstr.Unsafe.to_constr ic in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
-	!evdref , c
+        Typing.solve_evars env sigma (EConstr.of_constr c)
       with
 	| Not_found ->
 	    user_err ?loc ~hdr:"interp_may_eval"
-- 
cgit v1.2.3