blob: 32b25ff7262e0ed2670fb3e0e61fc6d87ee43667 (
plain)
1
2
3
4
5
6
7
8
|
Definition a := fun (P:SProp) (p:P) => p.
Lemma foo : (let k := a in let k' := a in fun (x:nat) y => x) = (let k := a in fun x y => y).
Proof.
Fail reflexivity.
match goal with |- ?l = _ => exact_no_check (eq_refl l) end.
Fail Qed.
Abort.
|
