A fix to #5414 (ident bound by ltac names now known for "match").

Also taking into account a name in the return clause and in the
indices.

Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".

1 files changed, 16 insertions, 0 deletions

diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 5da20c9d1..a35dae4aa 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -95,3 +95,19 @@ type closure = {
 and closed_glob_constr = {
   closure: closure;
   term: glob_constr }
+
+(** Ltac variable maps *)
+type var_map = Pattern.constr_under_binders Id.Map.t
+type uconstr_var_map = closed_glob_constr Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
+
+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_idents: Id.t Id.Map.t;
+  (** Ltac variables bound to identifiers *)
+  ltac_genargs : unbound_ltac_var_map;
+  (** Ltac variables bound to other kinds of arguments *)
+}