Better structure for Ltac pretyping environments.

3 files changed, 21 insertions, 5 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 27986eab6..478019b41 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -44,7 +44,12 @@ let instantiate_tac n (ist,rawc) ido =
     let evi = Evd.find sigma evk in
     let filtered = Evd.evar_filtered_env evi in
     let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
-    let sigma' = w_refine (evk,evi) ((constrvars,Names.Id.Map.empty, ist.Geninterp.lfun),rawc) sigma in
+    let lvar = {
+      Pretyping.ltac_constrs = constrvars;
+      ltac_uconstrs = Names.Id.Map.empty;
+      ltac_genargs = ist.Geninterp.lfun;
+    } in
+    let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in
     tclEVARS sigma' gl
   end
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 214db580a..af28f5145 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -364,8 +364,11 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Goal.bind Goal.concl (fun concl ->
         let flags = Pretyping.all_no_fail_flags in
         let tycon = Pretyping.OfType concl in
-        Goal.Refinable.constr_of_raw h tycon flags
-          Glob_term.(closure.typed,closure.untyped,Id.Map.empty) term
+        let lvar = { Pretyping.empty_lvar with
+          Pretyping.ltac_constrs = closure.Glob_term.typed;
+          Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
+        } in
+        Goal.Refinable.constr_of_raw h tycon flags lvar term
       )
     end in
     Proofview.Goal.lift c begin fun c ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4372f87a4..35f36f008 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -485,7 +485,11 @@ let interp_uconstr ist env = function
 
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_values ist env in
-  let vars = (constrvars, Id.Map.empty, ist.lfun) in
+  let vars = {
+    Pretyping.ltac_constrs = constrvars;
+    Pretyping.ltac_uconstrs = Id.Map.empty;
+    Pretyping.ltac_genargs = ist.lfun;
+  } in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -1185,7 +1189,11 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t =
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let {closure;term} = interp_uconstr ist env c in
-        let vars = closure.typed , closure.untyped , ist.lfun in
+        let vars = {
+          Pretyping.ltac_constrs = closure.typed;
+          Pretyping.ltac_uconstrs = closure.untyped;
+          Pretyping.ltac_genargs = ist.lfun;
+        } in
         let (sigma,c_interp) =
           Pretyping.understand_ltac constr_flags sigma env vars WithoutTypeConstraint term
         in