From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Mar 2017 02:18:53 +0100
Subject: 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".
---
 intf/glob_term.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'intf')

diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 5da20c9d1c..a35dae4aae 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 *)
+}
-- 
cgit v1.2.3