From 15e43996b342f2eddf0c6c0bd4166e757589337e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Apr 2018 14:59:00 +0200 Subject: 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. --- test-suite/bugs/closed/7195.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 test-suite/bugs/closed/7195.v (limited to 'test-suite/bugs') 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. -- cgit v1.2.3