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