From c22ac10752c12bcb23402ad29a73f2d9699248a6 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 26 Apr 2018 15:03:10 +0200 Subject: Deprecate Typing.e_* functions --- plugins/ltac/tacinterp.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins/ltac/tacinterp.ml') 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