blob: 6f8631d458d28679a0853fd21c7e5ad08fc96df9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* Fixing missing test for variable shadowing *)
Definition test (x y:bool*bool) :=
match x with
| (e as e1, (true) as e2)
| ((true) as e1, e as e2) =>
let '(e, b) := y in
e
| _ => true
end.
Goal test (true,false) (true,true) = true.
(* used to evaluate to "false = true" in 8.4 *)
reflexivity.
Qed.
|
