diff options
| author | Arnaud Spiwack | 2013-12-06 11:11:01 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-06 14:14:56 +0100 |
| commit | 2bbe6a88b840a4857f683fd6ee8cfc37ad7770c7 (patch) | |
| tree | 39370679ba80a2d8ec12639032e95519d5ba44c3 | |
| parent | a6a87649c3e0ea205e0ad9e9536bb881ddc2e73b (diff) | |
Remove duplicate test-suite file.
success/instantiate.v was a duplicate of bugs/closed/1041.v
| -rw-r--r-- | test-suite/success/instantiate.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/test-suite/success/instantiate.v b/test-suite/success/instantiate.v deleted file mode 100644 index 6f1030a438..0000000000 --- a/test-suite/success/instantiate.v +++ /dev/null @@ -1,11 +0,0 @@ -(* 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). |