blob: ea97747ac921868c5032bfcb481a279dbb5f7f4a (
plain)
1
2
3
4
5
6
7
8
9
10
11
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.
|
