blob: 6f1030a438f70efbee6aee3bfda48cb93eb41f3e (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* Test régression bug #1041 *)
Goal Prop.
pose (P:= fun x y :Prop => y).
evar (Q: forall X Y,P X Y -> Prop) .
instantiate (1:= fun _ => _ ) in (Value of Q).
instantiate (1:= fun _ => _ ) in (Value of Q).
instantiate (1:= fun _ => _ ) in (Value of Q).
instantiate (1:= H) in (Value of Q).
|
