blob: 543ca0c9244d73b103b8eb45580caeefd5b091c7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Bug in the computation of generalization *)
(* The following bug, elaborated by Bruno Barras, is solved from r11083 *)
Parameter P : unit -> Prop.
Definition T := sig P.
Parameter Q : T -> Prop.
Definition U := sig Q.
Parameter a : U.
Check (match a with exist (exist tt e2) e3 => e3=e3 end).
(* There is still a form submitted by Pierre Corbineau (#1834) which fails *)
|
