Imported Upstream version 8.8.2upstream/8.8.2

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 00000000..ea97747a
--- /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.