Attempt to slightly improve abusive "Collision between bound

variables" when matching over "{v : _ | _ & _}" which hides twice the
binding "fun v" since it is "sig2 (fun v => _) (fun v => _)".

Computing the bound variables statically at internalisation time
rather than every time at interpretation time. This cannot hurt even
if I don't know how to deal with the "notation" problem of a single
bound variable actually hiding two: at the current time, the notation
is printed only if the two variables are identical (see #4592), so,
with this semantics the warning should not be printed, but we lost the
information that we are coming from a notation; if #4592 were
addressed, then one of the binding should be alpha-renamed if they
differ, so collision should be solved by choosing the variable name
which is not renamed, but the matching algorithm should then be aware
of what the notation printing algorithm is doing... maybe not the most
critical thing at the current time.

5 files changed, 17 insertions, 14 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 875ad3d160..e06436d8a3 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -120,7 +120,7 @@ type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
 
 type binding_bound_vars = Id.Set.t
-type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
+type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
 
 type 'a delayed_open = 'a Pretyping.delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index a75805b4f8..15589d5c4a 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -325,8 +325,9 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
   let metas,pat = Constrintern.intern_constr_pattern
     ist.genv ~as_type ~ltacvars pc
   in
-  let c = intern_constr_gen true false ist pc in
-  metas,(c,pat)
+  let (glob,_ as c) = intern_constr_gen true false ist pc in
+  let bound_names = Glob_ops.bound_glob_vars glob in
+  metas,(bound_names,c,pat)
 
 let dummy_pat = PRel 0
 
@@ -334,7 +335,9 @@ let intern_typed_pattern ist p =
   (* we cannot ensure in non strict mode that the pattern is closed *)
   (* keeping a constr_expr copy is too complicated and we want anyway to *)
   (* type it, so we remember the pattern as a glob_constr only *)
-  (intern_constr_gen true false ist p,dummy_pat)
+  let (glob,_ as c) = intern_constr_gen true false ist p in
+  let bound_names = Glob_ops.bound_glob_vars glob in
+  (bound_names,c,dummy_pat)
 
 let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   let interp_ref r =
@@ -358,7 +361,8 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
           let r = evaluable_of_global_reference ist.genv (VarRef id) in
           Inl (ArgArg (r,None))
       | _ ->
-          Inr ((c,None),dummy_pat) in
+          let bound_names = Glob_ops.bound_glob_vars c in
+          Inr (bound_names,(c,None),dummy_pat) in
   (l, match p with
   | Inl r -> interp_ref r
   | Inr (CAppExpl(_,(None,r,None),[])) ->
@@ -577,7 +581,7 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
 
   | TacMatchGoal (lz,lr,lmr) ->
-      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)
+      ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr))
   | TacMatch (lz,c,lmr) ->
       ist.ltacvars,
       TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 02b03b72c2..9b41a276b9 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -678,7 +678,7 @@ let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
 let interp_pure_open_constr ist =
   interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
 
-let interp_typed_pattern ist env sigma (c,_) =
+let interp_typed_pattern ist env sigma (_,c,_) =
   let sigma, c =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
   pattern_of_constr env sigma c
@@ -1106,12 +1106,11 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt
 (* Reads a pattern by substituting vars of lfun *)
 let use_types = false
 
-let eval_pattern lfun ist env sigma ((glob,_),pat as c) =
-  let bound_names = bound_glob_vars glob in
+let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) =
   if use_types then
-    (bound_names,interp_typed_pattern ist env sigma c)
+    (bvars,interp_typed_pattern ist env sigma c)
   else
-    (bound_names,instantiate_pattern env sigma lfun pat)
+    (bvars,instantiate_pattern env sigma lfun pat)
 
 let read_pattern lfun ist env sigma = function
   | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 4059877b75..438219f5a3 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -107,8 +107,8 @@ let subst_evaluable subst =
 
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
-let subst_glob_constr_or_pattern subst (c,p) =
-  (subst_glob_constr subst c,subst_pattern subst p)
+let subst_glob_constr_or_pattern subst (bvars,c,p) =
+  (bvars,subst_glob_constr subst c,subst_pattern subst p)
 
 let subst_redexp subst =
   Miscops.map_red_expr_gen
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 631cb4c577..7949bafcbb 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1188,7 +1188,7 @@ module Make
 
   let pr_and_constr_expr pr (c,_) = pr c
 
-  let pr_pat_and_constr_expr pr ((c,_),_) = pr c
+  let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c
 
   let pr_glob_tactic_level env n t =
     let glob_printers =