aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4191.v
blob: 290bb384d96427fcec03cc906cb88a994c7e0c90 (plain)
1
2
3
4
5
(* Test maximal implicit arguments in the presence of let-ins *)
Definition foo (x := 1) {y : nat} (H : y = y) : True := I.
Definition bar {y : nat} (x := 1) (H : y = y) : True := I.
Check bar (eq_refl 1).
Check foo (eq_refl 1).