aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/intros.v
blob: 3599da4dc7371bf8180daf8d2c8ce68b241438b9 (plain)
1
2
3
4
5
6
7
(* Thinning introduction hypothesis must be done after all introductions *)
(* Submitted by Guillaume Melquiond (bug #1000) *)

Goal forall A, A -> True.
intros _ _.