Better struture for Ltac internalization environments in Constrintern.

2 files changed, 22 insertions, 10 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 2a66b32bc5..c2f85d5343 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -245,7 +245,11 @@ let intern_binding_name ist x =
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
-  let ltacvars = (lfun, Id.Set.empty,Id.Map.empty) in
+  let ltacvars = {
+    Constrintern.ltac_vars = lfun;
+    ltac_bound = Id.Set.empty;
+    ltac_subst = Id.Map.empty;
+  } in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
   in
@@ -318,7 +322,11 @@ let intern_flag ist red =
 let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 
 let intern_constr_pattern ist ~as_type ~ltacvars pc =
-  let ltacvars = ltacvars, Id.Set.empty,Id.Map.empty in
+  let ltacvars = {
+    Constrintern.ltac_vars = ltacvars;
+    ltac_bound = Id.Set.empty;
+    ltac_subst = Id.Map.empty;
+  } in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.genv ~as_type ~ltacvars pc
   in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 20234d1f2c..cca26bf055 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -471,10 +471,12 @@ let extract_ltac_uconstr_values ist env =
 let interp_uconstr ist env = function
   | (c,None) -> c
   | (_,Some ce) ->
-      let ltacvars = extract_ltac_uconstr_values ist env in
-      let bndvars = Id.Map.domain ist.lfun in
-      let ltacdata = (Id.Set.empty, bndvars , ltacvars) in
-      intern_gen WithoutTypeConstraint ~ltacvars:ltacdata env ce
+      let ltacvars = {
+        Constrintern.ltac_vars = Id.Set.empty;
+        ltac_bound = Id.Map.domain ist.lfun;
+        ltac_subst = extract_ltac_uconstr_values ist env;
+      } in
+      intern_gen WithoutTypeConstraint ~ltacvars env ce
 
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_values ist env in
@@ -485,10 +487,12 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
   | Some c ->
-      let ltacvars = Id.Map.domain constrvars in
-      let bndvars = Id.Map.domain ist.lfun in
-      let ltacdata = (ltacvars, bndvars,Id.Map.empty) in
-      intern_gen kind ~allow_patvar ~ltacvars:ltacdata env c
+      let ltacvars = {
+        ltac_vars = Id.Map.domain constrvars;
+        ltac_bound = Id.Map.domain ist.lfun;
+        ltac_subst = Id.Map.empty;
+      } in
+      intern_gen kind ~allow_patvar ~ltacvars env c
   in
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in