blob: 0994b6fb23fc5801f5abe035afbf507c5d5734f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* Checking that let-in's hiding evars are expanded when enforcing
"occur-check" *)
Require Import List.
Definition foo x y :=
let xy := (x, y) in
let bar xys :=
match xys with
| nil => xy :: nil
| xy' :: xys' => xy' :: xys'
end in bar (nil : list (nat * nat)).
|
