Remove uses of Global in Evd API.

Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.

4 files changed, 33 insertions, 33 deletions

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