blob: d9268dbe2fe68a6145c4020bb858f340ac155b90 (
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).
|
