blob: df6661483a35540b728f4b1aeffb1678c4c43a21 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* Some check of Miller's pattern inference - used to fail in 8.2 due
first to the presence of aliases, secondly due to the absence of
restriction of the potential interesting variables to the subset of
variables effectively occurring in the term to instantiate *)
Set Implicit Arguments.
Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
Variable H : exists x : bool, True.
Definition coef :=
match Some true with
Some _ => @choose _ H |_ => true
end .
|
