blob: cb30aa5d1fa29961e2776ae2bc1b96c15b5082cc (
plain)
1
2
3
4
5
6
7
8
|
(* Regression wrt v8.4 related to the change of order of resolution of evar-evar unification problems. *)
Goal exists x, x=1 -> True.
eexists. intro H.
pose proof (f_equal (fun k => k) H).
Undo.
pose (@f_equal _ _ S _ _ H).
Abort.
|
