Allowing to pass arbitrary data in internalization environments.

1 files changed, 4 insertions, 3 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b8c021f18..5f831f326 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -587,6 +587,7 @@ let interp_uconstr ist env sigma = function
       let ltacvars = {
         Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
@@ -614,6 +615,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       let ltacvars = {
         ltac_vars = constr_context;
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       let kind_for_intern =
         match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
@@ -1966,8 +1968,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   let ist = { lfun = lfun; extra = extra } in
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
-    (intern_pure_tactic {
-      ltacvars; genv = env } t)
+    (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
   end }
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -1976,7 +1977,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
 (* [global] means that [t] should be internalized outside of goals. *)
 let hide_interp global t ot =
   let hide_interp env =
-    let ist = { ltacvars = Id.Set.empty; genv = env } in
+    let ist = Genintern.empty_glob_sign env in
     let te = intern_pure_tactic ist t in
     let t = eval_tactic te in
     match ot with