Remove some occurrences of Evd.empty

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

3 files changed, 10 insertions, 6 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 2db67c299..8aa1e6250 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -237,11 +237,11 @@ let is_rigid env sigma t =
      is_rigid_head sigma t
   | _ -> true
 
-let find_displayed_name_in all avoid na (env, b) =
+let find_displayed_name_in sigma all avoid na (env, b) =
   let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
-  else compute_displayed_name_in Evd.empty flag avoid na b
+  if all then compute_and_force_displayed_name_in sigma flag avoid na b
+  else compute_displayed_name_in sigma flag avoid na b
 
 let compute_implicits_names_gen all env sigma t =
   let open Context.Rel.Declaration in
@@ -249,7 +249,7 @@ let compute_implicits_names_gen all env sigma t =
     let t = whd_all env sigma t in
     match kind sigma t with
     | Prod (na,a,b) ->
-       let na',avoid' = find_displayed_name_in all avoid na (names,b) in
+       let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in
        aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
     | _ -> List.rev names
   in aux env Id.Set.empty [] t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index e51c69136..448881dcf 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -509,7 +509,9 @@ let notation_constr_of_glob_constr nenv a =
 
 let notation_constr_of_constr avoiding t =
   let t = EConstr.of_constr t in
-  let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let t = Detyping.detype Detyping.Now false avoiding env evd t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index b57103cf2..071248f01 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -112,7 +112,9 @@ let revert_reserved_type t =
     let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
     let t = EConstr.of_constr t in
-    let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
+    let env = Global.env () in
+    let evd = Evd.from_env env in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =