From 29de26213adaa8b75320bee6897218d5e8d54663 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Thu, 10 Apr 2014 15:59:45 +0200
Subject: By resolution of the CoqWG, instantiate must not be used now that
 refine works

---
 test-suite/bugs/closed/1041.v | 13 -------------
 1 file changed, 13 deletions(-)
 delete mode 100644 test-suite/bugs/closed/1041.v

diff --git a/test-suite/bugs/closed/1041.v b/test-suite/bugs/closed/1041.v
deleted file mode 100644
index a5de82e0d8..0000000000
--- a/test-suite/bugs/closed/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.
-
-- 
cgit v1.2.3