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).
|
