aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml4
-rw-r--r--plugins/ltac/rewrite.ml7
-rw-r--r--plugins/ltac/tacinterp.ml6
3 files changed, 6 insertions, 11 deletions
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"