Merge PR #11338: Remove uses of Global in Evd API.

Reviewed-by: ejgallego
Reviewed-by: herbelin

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 085689be0a..ba7ae5069b 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -606,7 +606,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
@@ -623,7 +623,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 04f3e0d7b2..99d74f16cc 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 &&