Better structure for Ltac pretyping environments.

7 files changed, 53 insertions, 17 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f18aa364b..cb3e81efe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -48,7 +48,11 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = constr_under_binders Id.Map.t
 type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
 type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
-type ltac_var_map = var_map * uconstr_var_map * unbound_ltac_var_map
+type ltac_var_map = {
+  ltac_constrs : var_map;
+  ltac_uconstrs : uconstr_var_map;
+  ltac_genargs : unbound_ltac_var_map;
+}
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
@@ -237,7 +241,7 @@ let protected_get_type_of env sigma c =
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
-let pretype_id pretype loc env evdref (lvar,globvar,unbndltacvars) id =
+let pretype_id pretype loc env evdref lvar id =
   let sigma = !evdref in
   (* Look for the binder of [id] *)
   try
@@ -246,21 +250,22 @@ let pretype_id pretype loc env evdref (lvar,globvar,unbndltacvars) id =
   with Not_found ->
     (* Check if [id] is an ltac variable *)
     try
-      let (ids,c) = Id.Map.find id lvar in
+      let (ids,c) = Id.Map.find id lvar.ltac_constrs in
       let subst = List.map (invert_ltac_bound_name env id) ids in
       let c = substl subst c in
 	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found -> try
-       let {closure;term} = Id.Map.find id globvar in
+       let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in
+       let lvar = { lvar with ltac_constrs = closure.typed; ltac_uconstrs = closure.untyped } in
        (* spiwack: I'm catching [Not_found] potentially too eagerly
           here, as the call to the main pretyping function is caught
           inside the try but I want to avoid refactoring this function
           too much for now. *)
-       pretype env evdref (closure.typed,closure.untyped,unbndltacvars) term
+       pretype env evdref lvar term
     with Not_found ->
         (* Check if [id] is a ltac variable not bound to a term *)
 	(* and build a nice error message *)
-      if Id.Map.mem id unbndltacvars then
+      if Id.Map.mem id lvar.ltac_genargs then
 	user_err_loc (loc,"",
           str "Variable " ++ pr_id id ++ str " should be bound to a term.");
       (* Check if [id] is a section or goal variable *)
@@ -362,7 +367,7 @@ let is_GHole = function
   | GHole _ -> true
   | _ -> false
 
-let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
+let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
   let pretype_type = pretype_type resolve_tc in
   let pretype = pretype resolve_tc in
@@ -410,7 +415,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
         | Some ty -> ty
         | None ->
           new_type_evar evdref env loc in
-      let ist = Util.pi3 lvar in
+      let ist = lvar.ltac_genargs in
       let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }
@@ -907,7 +912,11 @@ let no_classes_no_fail_inference_flags = {
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
-let empty_lvar : ltac_var_map = (Id.Map.empty, Id.Map.empty, Id.Map.empty)
+let empty_lvar : ltac_var_map = {
+  ltac_constrs = Id.Map.empty;
+  ltac_uconstrs = Id.Map.empty;
+  ltac_genargs = Id.Map.empty;
+}
 
 let on_judgment f j =
   let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 4a80226bd..33f5e420d 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -30,7 +30,18 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = Pattern.constr_under_binders Id.Map.t
 type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
 type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
-type ltac_var_map = var_map * uconstr_var_map * unbound_ltac_var_map
+
+type ltac_var_map = {
+  ltac_constrs : var_map;
+  (** Ltac variables bound to constrs *)
+  ltac_uconstrs : uconstr_var_map;
+  (** Ltac variables bound to untyped constrs *)
+  ltac_genargs : unbound_ltac_var_map;
+  (** Ltac variables bound to other kinds of arguments *)
+}
+
+val empty_lvar : ltac_var_map
+
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 4746177ac..98a97a91c 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -64,6 +64,6 @@ let instantiate_pf_com evk com sigma =
   let evi = Evd.find sigma evk in
   let env = Evd.evar_filtered_env evi in
   let rawc = Constrintern.intern_constr env com in
-  let ltac_vars = (Id.Map.empty, Id.Map.empty, Id.Map.empty) in
+  let ltac_vars = Pretyping.empty_lvar in
   let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
   sigma'
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
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 7c42d7a8f..7497393e5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1173,7 +1173,7 @@ let explain_ltac_call_trace last trace loc =
   | Proof_type.LtacAtomCall te ->
       quote (Pptactic.pr_glob_tactic (Global.env())
               (Tacexpr.TacAtom (Loc.ghost,te)))
-  | Proof_type.LtacConstrInterp (c,(vars,_,unboundvars)) ->
+  | Proof_type.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
       quote (pr_glob_constr_env (Global.env()) c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++