Merge PR #7419: Remove 100 occurrences of Evd.empty

11 files changed, 44 insertions, 25 deletions

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 0c752d4a4..2a527da9b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -229,7 +229,9 @@ let extend_with_auto_hints env sigma l seq =
 
 let print_cmap map=
   let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5e0d3e8ee..83fe1fc2f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -230,7 +230,7 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
   with Not_found -> false
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
-  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
+  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env @@ Evd.from_env Environ.empty_env
 
 
 exception NoChange
@@ -1099,10 +1099,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     let get_body const =
       match Global.body_of_constant const with
 	| Some (body, _) ->
+          let env = Global.env () in
+          let sigma = Evd.from_env env in
 	     Tacred.cbv_norm_flags
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-	       (Global.env ())
-	       (Evd.empty)
+               env
+               sigma
 	       (EConstr.of_constr body)
 	| None -> user_err Pp.(str "Cannot define a principle over an axiom ")
     in
@@ -1340,7 +1342,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-                       Reductionops.nf_betaiota (pf_env g) Evd.empty
+                       Reductionops.nf_betaiota (pf_env g) (project g)
 			 (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90af20b4c..d193e1144 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -38,7 +38,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
     | Some b ->
-      let (_, b) = b (Global.env ()) Evd.empty in
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      let (_, b) = b env evd in
       spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b9d5ebf57..cc92a73f0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -67,7 +67,7 @@ let observe_tac s tac g =
 let nf_zeta =
   Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
     Environ.empty_env
-    Evd.empty
+    (Evd.from_env Environ.empty_env)
 
 let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ab03f1831..72bb8253d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -106,12 +106,12 @@ let const_of_ref = function
 
 let nf_zeta env =
   Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-    env
-    Evd.empty
+    env (Evd.from_env env)
 
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
-  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
+  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env
+    (Evd.from_env Environ.empty_env)
 
 
 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 797dfbe23..c21921513 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -613,10 +613,12 @@ END
 
 VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
  | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
-           [ let tc,_ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in
-             let tb,_ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in
-             let tc = EConstr.to_constr Evd.empty tc in
-             let tb = EConstr.to_constr Evd.empty tb in
+           [ let env = Global.env () in
+             let evd = Evd.from_env env in
+             let tc,_ctx = Constrintern.interp_constr env evd c in
+             let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
+             let tc = EConstr.to_constr evd tc in
+             let tb = EConstr.to_constr evd tb in
              Global.register f tc tb ]
 END
 
@@ -779,7 +781,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
-            let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in
+            let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
 	    change_concl c
           end;
 	  simplest_case a]
@@ -1106,7 +1108,9 @@ END
 VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
 | [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
   let get_key c =
-    let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in
+    let env = Global.env () in
+    let evd = Evd.from_env env in
+    let (evd, c) = Constrintern.interp_open_constr env evd c in
     let kind c = EConstr.kind evd c in
     Keys.constr_key kind c
   in
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bd02d85d5..3dfe308a5 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -149,9 +149,12 @@ let string_of_genarg_arg (ArgumentType arg) =
              let open Genprint in
              match generic_top_print (in_gen (Topwit wit) x) with
              | TopPrinterBasic pr -> pr ()
-             | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+             | TopPrinterNeedsContext pr ->
+               let env = Global.env() in
+               pr env (Evd.from_env env)
              | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
-                printer (Global.env()) Evd.empty default_ensure_surrounded
+               let env = Global.env() in
+               printer env (Evd.from_env env) default_ensure_surrounded
           end
         | _ -> default
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1b86583da..b91315aca 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m =
   let evd = solve_constraints env !evd in
   let evd = Evd.minimize_universes evd in
   let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
-  Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m);
+  Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m);
   Evd.evar_universe_context evd, m
 
 let default_morphism sign m =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e455ebb28..3594c8765 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -369,8 +369,11 @@ let coq_True = lazy (init_constant "True")
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
 (* For unfold *)
-let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with
-  | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+let evaluable_ref_of_constr s c =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  match EConstr.kind evd (Lazy.force c) with
+  | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) ->
       EvalConstRef kn
   | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 05dbf0a86..7ac9ea89d 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -377,7 +377,10 @@ let interp_head_pat hpat =
   | Cast (c', _, _) -> loop c'
   | Prod (_, _, c') -> loop c'
   | LetIn (_, _, _, c') -> loop c'
-  | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in
+  | _ ->
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
   filter_head, loop
 
 let all_true _ = true
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 0dd3625ba..93c63d522 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -708,9 +708,9 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
 ;;
 
 
-let fixed_upat = function
+let fixed_upat evd = function
 | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false 
-| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *)
+| {up_t = t} -> not (occur_existential evd (EConstr.of_constr t)) (** FIXME *)
 
 let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
 
@@ -769,7 +769,7 @@ let mk_tpattern_matcher ?(all_instances=false)
 let p2t p = mkApp(p.up_f,p.up_a) in 
 let source () = match upats_origin, upats with
   | None, [p] -> 
-      (if fixed_upat p then str"term " else str"partial term ") ++ 
+      (if fixed_upat ise p then str"term " else str"partial term ") ++
       pr_constr_pat (p2t p) ++ spc()
   | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
       pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl()