Remove some occurrences of Evd.empty

We address the easy ones, but they should probably be all removed.

3 files changed, 16 insertions, 9 deletions

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 =