diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1041.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1041.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1041.v b/test-suite/bugs/closed/shouldsucceed/1041.v deleted file mode 100644 index a5de82e0..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1041.v +++ /dev/null @@ -1,13 +0,0 @@ -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). - -Admitted. - |