Remove fully_empty_glob_sign which uses a dummy environment

4 files changed, 3 insertions, 6 deletions

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 16cff420bd..0f88734caf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -353,7 +353,7 @@ let extend_atomic_tactic name entries =
       let default = epsilon_value inj e in
       match default with
       | None -> raise NonEmptyArgument
-      | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
+      | Some def -> Tacintern.intern_tactic_or_tacarg (Genintern.empty_glob_sign Environ.empty_env) def
     in
     try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
   in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index a2b4156f50..fcbcfae115 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -46,7 +46,6 @@ type glob_sign = Genintern.glob_sign = {
   extra : Genintern.Store.t;
 }
 
-let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env
 let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
 
 (* We have identifier <| global_reference <| constr *)
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 9146fced2d..a9f2d76e30 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -23,10 +23,8 @@ type glob_sign = Genintern.glob_sign = {
   extra : Genintern.Store.t;
 }
 
-val fully_empty_glob_sign : glob_sign
-
 val make_empty_glob_sign : unit -> glob_sign
- (** same as [fully_empty_glob_sign], but with [Global.env()] as
+ (** build an empty [glob_sign] using [Global.env()] as
      environment *)
 
 (** Main globalization functions *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b60b77595b..528d7de549 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2024,7 +2024,7 @@ let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k
 
 let interp_redexp env sigma r =
   let ist = default_ist () in
-  let gist = { fully_empty_glob_sign with genv = env; } in
+  let gist = Genintern.empty_glob_sign env in
   interp_red_expr ist env sigma (intern_red_expr gist r)
 
 (***************************************************************************)