Fixes #7195 (missing freshness condition in Ltac pattern-matching names).

We ensure that all original names in a spine of matched nested binders
are distinct.

Note: This enforces that two binders with same internal names are kept
disjoint but this does not enforce that we shall respect names exactly
as they are printed. Only the original prefix of the internal names
are preserved, not their "0" or "1" etc. suffix.

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/7195.v b/test-suite/bugs/closed/7195.v
new file mode 100644
index 000000000..ea97747ac
--- /dev/null
+++ b/test-suite/bugs/closed/7195.v
@@ -0,0 +1,12 @@
+(* A disjoint-names condition was missing when matching names in Ltac
+   pattern-matching *)
+
+Goal True.
+  let x := (eval cbv beta zeta in (fun P => let Q := P in fun P => P + Q)) in
+  unify x (fun a b => b + a); (* success *)
+    let x' := lazymatch x with
+              | (fun (a : ?A) (b : ?B) => ?k)
+                => constr:(fun (a : A) (b : B) => k)
+              end in
+    unify x x'.
+Abort.