aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Cases-bug1834.v
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 *)