Pass Ltac2 variables in a dedicated environment for generic arguments.

This is a way to hack around the fact that various interpretation functions
rely wrongly on the values of the environment to do nasty tricks. Typically,
the interpretation of terms is broken, as it will fail when there is a bound
variable with the same name as a hypothesis, instead of producing the
hypothesis itself.

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