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