Better struture for Ltac internalization environments in Constrintern.

2 files changed, 27 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 04e9fceff..203d78bd2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -66,6 +66,12 @@ type internalization_env =
 
 type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
 
+type ltac_sign = {
+  ltac_vars : Id.Set.t;
+  ltac_bound : Id.Set.t;
+  ltac_subst : glob_constr Lazy.t Id.Map.t;
+}
+
 let interning_grammar = ref false
 
 (* Historically for parsing grammar rules, but in fact used only for
@@ -638,7 +644,6 @@ let string_of_ty = function
   | Variable -> "var"
 
 let intern_var genv (ltacvars,ntnvars) namedctx loc id =
-  let (ltacvars,unbndltacvars,ltacsubst) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
@@ -649,12 +654,12 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
     GVar (loc,id), make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
-  if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars
+  if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
   then
     GVar (loc,id), [], [], []
   (* Is [id] bound to a glob_constr in the the ltac context *)
-  else if Id.Map.mem id ltacsubst then
-    Lazy.force (Id.Map.find id ltacsubst), [], [], []
+  else if Id.Map.mem id ltacvars.ltac_subst then
+    Lazy.force (Id.Map.find id ltacvars.ltac_subst), [], [], []
   (* Is [id] a notation variable *)
   else if Id.Map.mem id ntnvars
   then
@@ -664,7 +669,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   then if Id.Map.is_empty ntnvars
     then error_ldots_var loc
     else GVar (loc,id), [], [], []
-  else if Id.Set.mem id unbndltacvars then
+  else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
     user_err_loc (loc,"intern_var",
       str "variable " ++ pr_id id ++ str " should be bound to a term.")
@@ -1549,9 +1554,9 @@ let internalize globalenv env allow_patvar lvar c =
         let solve = match solve with
         | None -> None
         | Some gen ->
-          let ((cvars, lvars,_), ntnvars) = lvar in
+          let (ltacvars, ntnvars) = lvar in
           let ntnvars = Id.Map.domain ntnvars in
-          let lvars = Id.Set.union lvars cvars in
+          let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
           let lvars = Id.Set.union lvars ntnvars in
           let lvars = Id.Set.union lvars env.ids in
           let ist = {
@@ -1769,9 +1774,11 @@ let scope_of_type_kind = function
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
-type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t
-
-let empty_ltac_sign = (Id.Set.empty, Id.Set.empty, Id.Map.empty)
+let empty_ltac_sign = {
+  ltac_vars = Id.Set.empty;
+  ltac_bound = Id.Set.empty;
+  ltac_subst = Id.Map.empty;
+}
 
 let intern_gen kind env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 46697253b..b6cae349d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -67,7 +67,16 @@ val compute_internalization_env : env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = Id.Set.t * Id.Set.t * glob_constr Lazy.t Id.Map.t
+type ltac_sign = {
+  ltac_vars : Id.Set.t;
+  (** Variables of Ltac which may be bound to a term *)
+  ltac_bound : Id.Set.t;
+  (** Other variables of Ltac *)
+  ltac_subst : glob_constr Lazy.t Id.Map.t;
+  (** Substitution for untyped terms *)
+}
+
+val empty_ltac_sign : ltac_sign
 
 type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)