1 files changed, 0 insertions, 56 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v
deleted file mode 100644
index 6377a8b7..00000000
--- a/test-suite/bugs/closed/shouldsucceed/2117.v
+++ /dev/null
@@ -1,56 +0,0 @@
-(* Check pattern-unification on evars in apply unification *)
-
-Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'.
-
-Axiom copy : forall tau:Type, tau -> tau -> Prop.
-Axiom copyr : forall tau:Type, tau -> tau -> Prop.
-Axiom copyf : forall tau:Type, tau -> tau -> Prop.
-Axiom eq : forall tau:Type, tau -> tau -> Prop.
-Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop.
-
-Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'.
-Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'),
-(forall x:tau, copyr tau x x->copy tau' (t x) (t' x))
-->copy (tau->tau') t t'.
-
-Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'.
-Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'),
-copyr (tau->tau') t t'
-->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)).
-
-Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'.
-Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'),
-copyr (tau->tau') t t'
-->(forall x y:tau, forall z1 z2:tau',
-(copy tau x y)->
-(subst tau tau' t x z1)->
-(subst tau tau' t' y z2)->
-copyf tau' z1 z2).
-
-Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau',
-( ((subst tau tau' t q t') /\ (eq tau' t' r))
-->eq tau' (app tau tau' t q) r).
-
-Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
-forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t'))
-->eq tau' r (app tau tau' t q).
-
-Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
-(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r))
-->subst tau tau' t q r.
-
-Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.
-Ltac Subst := apply substcopy;intros;EtaLong.
-Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A).
-Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A.
-
-Theorem church0: forall i:Type, exists X:(i->i)->i->i,
-copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)).
-intros.
-esplit.
-EtaLong.
-eapply eqappd;split.
-Subst.
-apply copyf_atom.
-Show Existentials.
-apply H1.