aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh9
-rw-r--r--engine/evd.ml9
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/proofview.ml7
-rw-r--r--plugins/ltac/evar_tactics.ml12
-rw-r--r--pretyping/evarconv.ml30
-rw-r--r--pretyping/evardefine.ml6
-rw-r--r--pretyping/evarsolve.ml26
-rw-r--r--pretyping/evarsolve.mli4
-rw-r--r--printing/printer.ml7
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/goal.ml3
-rw-r--r--proofs/proof.ml4
-rw-r--r--vernac/himsg.ml4
-rw-r--r--vernac/vernacentries.ml2
16 files changed, 74 insertions, 59 deletions
diff --git a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
new file mode 100644
index 0000000000..f41271804a
--- /dev/null
+++ b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11338" ] || [ "$CI_BRANCH" = "rm-global-uses-evd" ]; then
+
+ unicoq_CI_REF=rm-global-uses-evd
+ unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+ equations_CI_REF=rm-global-uses-evd
+ equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/engine/evd.ml b/engine/evd.ml
index 94868d9bdd..8e7d942c37 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -200,13 +200,14 @@ let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
in
make_hyps filter (evar_context evi)
-let evar_env evi = Global.env_of_context evi.evar_hyps
+let evar_env env evi =
+ Environ.reset_with_named_context evi.evar_hyps env
-let evar_filtered_env evi = match Filter.repr (evar_filter evi) with
-| None -> evar_env evi
+let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with
+| None -> evar_env env evi
| Some filter ->
let rec make_env filter ctxt = match filter, ctxt with
- | [], [] -> reset_context (Global.env ())
+ | [], [] -> reset_context env
| false :: filter, _ :: ctxt -> make_env filter ctxt
| true :: filter, decl :: ctxt ->
let env = make_env filter ctxt in
diff --git a/engine/evd.mli b/engine/evd.mli
index 7876e9a48f..8843adc853 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -125,8 +125,8 @@ val evar_filtered_hyps : evar_info -> named_context_val
val evar_body : evar_info -> evar_body
val evar_candidates : evar_info -> constr list option
val evar_filter : evar_info -> Filter.t
-val evar_env : evar_info -> env
-val evar_filtered_env : evar_info -> env
+val evar_env : env -> evar_info -> env
+val evar_filtered_env : env -> evar_info -> env
val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 6f8e668e4e..16be96454e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1039,9 +1039,9 @@ let (>>=) = tclBIND
(** {6 Goal-dependent tactics} *)
-let goal_env evars gl =
+let goal_env env evars gl =
let evi = Evd.find evars gl in
- Evd.evar_filtered_env evi
+ Evd.evar_filtered_env env evi
let goal_nf_evar sigma gl =
let evi = Evd.find sigma gl in
@@ -1256,9 +1256,10 @@ module V82 = struct
let of_tactic t gls =
try
+ let env = Global.env () in
let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
let name, poly = Names.Id.of_string "legacy_pe", false in
- let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in
+ let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
with Logic_monad.TacticFailure e as src ->
let (_, info) = CErrors.push src in
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index c87eb7c3c9..3ea4974a87 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -26,9 +26,9 @@ module NamedDecl = Context.Named.Declaration
(* The instantiate tactic *)
-let instantiate_evar evk (ist,rawc) sigma =
+let instantiate_evar evk (ist,rawc) env sigma =
let evi = Evd.find sigma evk in
- let filtered = Evd.evar_filtered_env evi in
+ let filtered = Evd.evar_filtered_env env evi in
let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
let lvar = {
ltac_constrs = constrvars;
@@ -36,7 +36,7 @@ let instantiate_evar evk (ist,rawc) sigma =
ltac_idents = Names.Id.Map.empty;
ltac_genargs = ist.Geninterp.lfun;
} in
- let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in
+ let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in
tclEVARS sigma'
let evar_list sigma c =
@@ -48,6 +48,7 @@ let evar_list sigma c =
let instantiate_tac n c ido =
Proofview.V82.tactic begin fun gl ->
+ let env = Global.env () in
let sigma = gl.sigma in
let evl =
match ido with
@@ -69,16 +70,17 @@ let instantiate_tac n c ido =
user_err Pp.(str "Not enough uninstantiated existential variables.");
if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let evk,_ = List.nth evl (n-1) in
- instantiate_evar evk c sigma gl
+ instantiate_evar evk c env sigma gl
end
let instantiate_tac_by_name id c =
Proofview.V82.tactic begin fun gl ->
+ let env = Global.env () in
let sigma = gl.sigma in
let evk =
try Evd.evar_key id sigma
with Not_found -> user_err Pp.(str "Unknown existential variable.") in
- instantiate_evar evk c sigma gl
+ instantiate_evar evk c env sigma gl
end
let let_evar name typ =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2130d4ce90..3bd52088c7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1337,8 +1337,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
try
let evi = Evd.find_undefined evd evk in
let evi = nf_evar_info evd evi in
- let env_evar_unf = evar_env evi in
- let env_evar = evar_filtered_env evi in
+ let env_evar_unf = evar_env env_rhs evi in
+ let env_evar = evar_filtered_env env_rhs evi in
let sign = named_context_val env_evar in
let ctxt = evar_filtered_context evi in
if !debug_ho_unification then
@@ -1473,16 +1473,16 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
| Some [t] ->
if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then
raise (TypingFailed evd);
- instantiate_evar evar_unify flags evd ev (EConstr.of_constr t)
+ instantiate_evar evar_unify flags env_rhs evd ev (EConstr.of_constr t)
| Some l when abstract = Abstraction.Abstract &&
List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l ->
- instantiate_evar evar_unify flags evd ev vid
+ instantiate_evar evar_unify flags env_rhs evd ev vid
| _ -> evd)
with e -> user_err (Pp.str "Cannot find an instance")
else
((if !debug_ho_unification then
let evi = Evd.find evd evk in
- let env = Evd.evar_env evi in
+ let env = Evd.evar_env env_rhs evi in
Feedback.msg_debug Pp.(str"evar is defined: " ++
int (Evar.repr evk) ++ spc () ++
prc env evd (match evar_body evi with Evar_defined c -> c
@@ -1498,7 +1498,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
(if !debug_ho_unification then
begin
let evi = Evd.find evd evk in
- let evenv = evar_env evi in
+ let evenv = evar_env env_rhs evi in
let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in
Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body)
end;
@@ -1506,7 +1506,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
else
try
let evi = Evd.find_undefined evd evk in
- let evenv = evar_env evi in
+ let evenv = evar_env env_rhs evi in
let rhs' = nf_evar evd rhs' in
if !debug_ho_unification then
Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
@@ -1517,7 +1517,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
if !debug_ho_unification then
Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'));
let flags = default_flags_of TransparentState.full in
- Evarsolve.instantiate_evar evar_unify flags evd evk rhs'
+ Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs'
with IllTypedInstance _ -> raise (TypingFailed evd)
in
let evd = abstract_free_holes evd subst in
@@ -1664,7 +1664,7 @@ let max_undefined_with_candidates evd =
with MaxUndefined ans ->
Some ans
-let rec solve_unconstrained_evars_with_candidates flags evd =
+let rec solve_unconstrained_evars_with_candidates flags env evd =
(* max_undefined is supposed to return the most recent, hence
possibly most dependent evar *)
match max_undefined_with_candidates evd with
@@ -1675,9 +1675,9 @@ let rec solve_unconstrained_evars_with_candidates flags evd =
| a::l ->
(* In case of variables, most recent ones come first *)
try
- let evd = instantiate_evar evar_unify flags evd evk a in
+ let evd = instantiate_evar evar_unify flags env evd evk a in
match reconsider_unif_constraints evar_unify flags evd with
- | Success evd -> solve_unconstrained_evars_with_candidates flags evd
+ | Success evd -> solve_unconstrained_evars_with_candidates flags env evd
| UnifFailure _ -> aux l
with
| IllTypedInstance _ -> aux l
@@ -1685,7 +1685,7 @@ let rec solve_unconstrained_evars_with_candidates flags evd =
(* Expected invariant: most dependent solutions come first *)
(* so as to favor progress when used with the refine tactics *)
let evd = aux l in
- solve_unconstrained_evars_with_candidates flags evd
+ solve_unconstrained_evars_with_candidates flags env evd
let solve_unconstrained_impossible_cases env evd =
Evd.fold_undefined (fun evk ev_info evd' ->
@@ -1695,18 +1695,18 @@ let solve_unconstrained_impossible_cases env evd =
let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
let ty = j_type j in
let flags = default_flags env in
- instantiate_evar evar_unify flags evd' evk ty
+ instantiate_evar evar_unify flags env evd' evk ty
| _ -> evd') evd evd
let solve_unif_constraints_with_heuristics env
?(flags=default_flags env) ?(with_ho=false) evd =
- let evd = solve_unconstrained_evars_with_candidates flags evd in
+ let evd = solve_unconstrained_evars_with_candidates flags env evd in
let rec aux evd pbs progress stuck =
match pbs with
| (pbty,env,t1,t2 as pb) :: pbs ->
(match apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 with
| Success evd' ->
- let evd' = solve_unconstrained_evars_with_candidates flags evd' in
+ let evd' = solve_unconstrained_evars_with_candidates flags env evd' in
let (evd', rest) = extract_all_conv_pbs evd' in
begin match rest with
| [] -> aux evd' pbs true stuck
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index aebdd14396..c580d44237 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -76,7 +76,7 @@ let idx = Namegen.default_dependent_ident
let define_pure_evar_as_product env evd evk =
let open Context.Named.Declaration in
let evi = Evd.find_undefined evd evk in
- let evenv = evar_env evi in
+ let evenv = evar_env env evi in
let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in
let concl = Reductionops.whd_all evenv evd evi.evar_concl in
let s = destSort evd concl in
@@ -129,7 +129,7 @@ let define_evar_as_product env evd (evk,args) =
let define_pure_evar_as_lambda env evd evk =
let open Context.Named.Declaration in
let evi = Evd.find_undefined evd evk in
- let evenv = evar_env evi in
+ let evenv = evar_env env evi in
let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
let evd1,(na,dom,rng) = match EConstr.kind evd typ with
| Prod (na,dom,rng) -> (evd,(na,dom,rng))
@@ -170,7 +170,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function
let define_evar_as_sort env evd (ev,args) =
let evd, s = new_sort_variable univ_rigid evd in
let evi = Evd.find_undefined evd ev in
- let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in
+ let concl = Reductionops.whd_all (evar_env env evi) evd evi.evar_concl in
let sort = destSort evd concl in
let evd' = Evd.define ev (mkSort s) evd in
Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 5a23525fb0..b54a713a16 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -764,9 +764,9 @@ let restrict_upon_filter evd evk p args =
let len = Array.length args in
Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i))
-let check_evar_instance unify flags evd evk1 body =
+let check_evar_instance unify flags env evd evk1 body =
let evi = Evd.find evd evk1 in
- let evenv = evar_env evi in
+ let evenv = evar_env env evi in
(* FIXME: The body might be ill-typed when this is called from w_merge *)
(* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
let ty =
@@ -915,7 +915,7 @@ let rec find_solution_type evarenv = function
let rec do_projection_effects unify flags define_fun env ty evd = function
| ProjectVar -> evd
| ProjectEvar ((evk,argsv),evi,id,p) ->
- let evd = check_evar_instance unify flags evd evk (mkVar id) in
+ let evd = check_evar_instance unify flags env evd evk (mkVar id) in
let evd = Evd.define evk (EConstr.mkVar id) evd in
(* TODO: simplify constraints involving evk *)
let evd = do_projection_effects unify flags define_fun env ty evd p in
@@ -1284,7 +1284,7 @@ let solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 (evk2,_ as
update_evar_info evk2 (fst (destEvar evd' body)) evd'
else evd'
in
- check_evar_instance unify flags evd' evk2 body
+ check_evar_instance unify flags env evd' evk2 body
with EvarSolvedOnTheFly (evd,c) ->
f env evd pbty ev2 c
@@ -1329,12 +1329,12 @@ let solve_evar_evar ?(force=false) f unify flags env evd pbty (evk1,args1 as ev1
try
(* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j.
The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *)
- let evienv = Evd.evar_env evi in
+ let evienv = Evd.evar_env env evi in
let concl1 = EConstr.Unsafe.to_constr evi.evar_concl in
let ctx1, i = Reduction.dest_arity evienv concl1 in
let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in
let evi2 = Evd.find evd evk2 in
- let evi2env = Evd.evar_env evi2 in
+ let evi2env = Evd.evar_env env evi2 in
let concl2 = EConstr.Unsafe.to_constr evi2.evar_concl in
let ctx2, j = Reduction.dest_arity evi2env concl2 in
let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in
@@ -1418,7 +1418,7 @@ let solve_candidates unify flags env evd (evk,argsv) rhs =
(* time and the evar been solved by the filtering process *)
if Evd.is_undefined evd evk then
let evd' = Evd.define evk c evd in
- check_evar_instance unify flags evd' evk c
+ check_evar_instance unify flags env evd' evk c
else evd
| l when List.length l < List.length l' ->
let candidates = List.map fst l in
@@ -1442,11 +1442,11 @@ let occur_evar_upto_types sigma n c =
in
try occur_rec c; false with Occur -> true
-let instantiate_evar unify flags evd evk body =
+let instantiate_evar unify flags env evd evk body =
(* Check instance freezing the evar to be defined, as
checking could involve the same evar definition problem again otherwise *)
let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in
- let evd' = check_evar_instance unify flags evd evk body in
+ let evd' = check_evar_instance unify flags env evd evk body in
Evd.define evk body evd'
(* We try to instantiate the evar assuming the body won't depend
@@ -1508,7 +1508,7 @@ let rec invert_definition unify flags choose imitate_defs
raise (NotEnoughInformationToProgress sols);
(* No unique projection but still restrict to where it is possible *)
(* materializing is necessary, but is restricting useful? *)
- let ty = find_solution_type (evar_filtered_env evi) sols in
+ let ty = find_solution_type (evar_filtered_env env evi) sols in
let ty' = instantiate_evar_array evi ty argsv in
let (evd,evar,(evk',argsv' as ev')) =
materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in
@@ -1571,7 +1571,7 @@ let rec invert_definition unify flags choose imitate_defs
try
let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in
let evd = Evd.define evk' body evd in
- check_evar_instance unify flags evd evk' body
+ check_evar_instance unify flags env' evd evk' body
with
| EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
| CannotProject (evd,ev'') ->
@@ -1638,7 +1638,7 @@ let rec invert_definition unify flags choose imitate_defs
else
let t' = imitate (env,0) rhs in
if !progress then
- (recheck_applications unify flags (evar_env evi) evdref t'; t')
+ (recheck_applications unify flags (evar_env env evi) evdref t'; t')
else t'
in (!evdref,body)
@@ -1670,7 +1670,7 @@ and evar_define unify flags ?(choose=false) ?(imitate_defs=true) env evd pbty (e
if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
(* needed only if an inferred type *)
let evd', body = refresh_universes pbty env evd' body in
- instantiate_evar unify flags evd' evk body
+ instantiate_evar unify flags env evd' evk body
with
| NotEnoughInformationToProgress sols ->
postpone_non_unique_projection env evd pbty ev sols rhs
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 908adac7e4..74aee9da59 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -77,7 +77,7 @@ type conversion_check = unify_flags -> unification_kind ->
- [c] does not contain any Meta(_)
*)
-val instantiate_evar : unifier -> unify_flags -> evar_map ->
+val instantiate_evar : unifier -> unify_flags -> env -> evar_map ->
Evar.t -> constr -> evar_map
(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
@@ -125,7 +125,7 @@ exception IllTypedInstance of env * types * types
(* May raise IllTypedInstance if types are not convertible *)
val check_evar_instance : unifier -> unify_flags ->
- evar_map -> Evar.t -> constr -> evar_map
+ env -> evar_map -> Evar.t -> constr -> evar_map
val remove_instance_local_defs :
evar_map -> Evar.t -> 'a array -> 'a list
diff --git a/printing/printer.ml b/printing/printer.ml
index bb54f587fd..97e0528939 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -490,8 +490,8 @@ let pr_concl n ?(diffs=false) ?og_s sigma g =
header ++ str " is:" ++ cut () ++ str" " ++ pc
(* display evar type: a context and a type *)
-let pr_evgl_sign sigma evi =
- let env = evar_env evi in
+let pr_evgl_sign env sigma evi =
+ let env = evar_env env evi in
let ps = pr_named_context_of env sigma in
let _, l = match Filter.repr (evar_filter evi) with
| None -> [], []
@@ -517,7 +517,8 @@ let pr_evgl_sign sigma evi =
(* Print an existential variable *)
let pr_evar sigma (evk, evi) =
- let pegl = pr_evgl_sign sigma evi in
+ let env = Global.env () in
+ let pegl = pr_evgl_sign env sigma evi in
hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl)
(* Print an enumerated list of existential variables *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 59918ab2f9..8297b11585 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -44,10 +44,10 @@ let define_and_solve_constraints evk c env evd =
| Success evd -> evd
| UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.")
-let w_refine (evk,evi) (ltac_var,rawc) sigma =
+let w_refine (evk,evi) (ltac_var,rawc) env sigma =
if Evd.is_defined sigma evk then
user_err Pp.(str "Instantiate called on already-defined evar");
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
let sigma',typed_c =
let flags = {
Pretyping.use_typeclasses = true;
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 8f3ac7ed25..a618bf1c94 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -17,4 +17,4 @@ open Ltac_pretype
type glob_constr_ltac_closure = ltac_var_map * glob_constr
val w_refine : Evar.t * evar_info ->
- glob_constr_ltac_closure -> evar_map -> evar_map
+ glob_constr_ltac_closure -> Environ.env -> evar_map -> evar_map
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 426fba7f63..4759c0860f 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -31,8 +31,9 @@ module V82 = struct
(* Old style env primitive *)
let env evars gl =
+ let env = Global.env () in
let evi = Evd.find evars gl in
- Evd.evar_filtered_env evi
+ Evd.evar_filtered_env env evi
(* Old style hyps primitive *)
let hyps evars gl =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e9f93d0c8f..5ab4409f8b 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -434,10 +434,10 @@ module V82 = struct
else
CList.nth evl (n-1)
in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
let rawc = intern env sigma in
let ltac_vars = Glob_ops.empty_lvar in
- let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
+ let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) env sigma in
Proofview.Unsafe.tclEVARS sigma
end in
let { name; poly } = pr in
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 19ec0a3642..c8e308cb9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -605,7 +605,7 @@ let rec explain_evar_kind env sigma evk ty =
let explain_typeclass_resolution env sigma evi k =
match Typeclasses.class_of_constr env sigma evi.evar_concl with
| Some _ ->
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
fnl () ++ str "Could not find an instance for " ++
pr_leconstr_env env sigma evi.evar_concl ++
pr_trailing_ne_context_of env sigma
@@ -622,7 +622,7 @@ let explain_placeholder_kind env sigma c e =
let explain_unsolvable_implicit env sigma evk explain =
let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in
let pe = pr_trailing_ne_context_of env sigma in
strbrk "Cannot infer " ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 604d1b28ff..d3bc06cd6c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -474,7 +474,7 @@ let program_inference_hook env sigma ev =
let tac = !Obligations.default_tactic in
let evi = Evd.find sigma ev in
let evi = Evarutil.nf_evar_info sigma evi in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
try
let concl = evi.Evd.evar_concl in
if not (Evarutil.is_ground_env sigma env &&
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:47:45 +0000