3 files changed, 26 insertions, 8 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 609dd40587..d14849a2a6 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -656,8 +656,7 @@ let open_constr_no_classes_flags () =
 (** Embed all Ltac2 data into Values *)
 let to_lvar ist =
   let open Glob_ops in
-  let map e = Val.Dyn (val_valexpr, e) in
-  let lfun = Id.Map.map map ist in
+  let lfun = Tac2interp.set_env ist Id.Map.empty in
   { empty_lvar with Glob_term.ltac_genargs = lfun }
 
 let interp_constr flags ist (c, _) =
@@ -728,12 +727,7 @@ let () =
 
 let () =
   let interp ist env sigma concl tac =
-    let fold id (Val.Dyn (tag, v)) (accu : environment) : environment =
-      match Val.eq tag val_valexpr with
-      | None -> accu
-      | Some Refl -> Id.Map.add id v accu
-    in
-    let ist = Id.Map.fold fold ist Id.Map.empty in
+    let ist = Tac2interp.get_env ist in
     let tac = Proofview.tclIGNORE (interp ist tac) in
     let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in
     (EConstr.of_constr c, sigma)
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 3490b1a2a8..691c795502 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -155,3 +155,22 @@ and interp_set ist e p r = match e with
   return (ValInt 0)
 | ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
   anomaly (str "Unexpected value shape")
+
+(** Cross-boundary hacks. *)
+
+open Geninterp
+
+let val_env : environment Val.typ = Val.create "ltac2:env"
+let env_ref = Id.of_string_soft "@@ltac2_env@@"
+
+let extract_env (Val.Dyn (tag, v)) : environment =
+match Val.eq tag val_env with
+| None -> assert false
+| Some Refl -> v
+
+let get_env ist =
+  try extract_env (Id.Map.find env_ref ist)
+  with Not_found -> empty_environment
+
+let set_env env ist =
+  Id.Map.add env_ref (Val.Dyn (val_env, env)) ist
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index 42e9e3adeb..f99008c506 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -17,6 +17,11 @@ val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
 
 val interp_app : valexpr -> valexpr list -> valexpr Proofview.tactic
 
+(** {5 Cross-boundary encodings} *)
+
+val get_env : Glob_term.unbound_ltac_var_map -> environment
+val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound_ltac_var_map
+
 (** {5 Exceptions} *)
 
 exception LtacError of KerName.t * valexpr array