From ac03db11dd55e1250126b7369e70a2c1fa397271 Mon Sep 17 00:00:00 2001
From: Xavier Clerc
Date: Fri, 26 Sep 2014 13:28:25 +0200
Subject: Bug #3566 is fixed.

---
 test-suite/bugs/opened/3566.v | 21 ---------------------
 1 file changed, 21 deletions(-)
 delete mode 100644 test-suite/bugs/opened/3566.v

(limited to 'test-suite/bugs/opened')

diff --git a/test-suite/bugs/opened/3566.v b/test-suite/bugs/opened/3566.v
deleted file mode 100644
index e0075b8339..0000000000
--- a/test-suite/bugs/opened/3566.v
+++ /dev/null
@@ -1,21 +0,0 @@
-Notation idmap := (fun x => x).
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
-Arguments idpath {A a} , [A] a.
-Notation "x = y :> A" := (@paths A x y) : type_scope.
-Notation "x = y" := (x = y :>_) : type_scope.
-Delimit Scope path_scope with path.
-Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
-Definition inverse {A : Type} {x y : A} (p : x = y) : y = x := match p with idpath => idpath end.
-Notation "p @ q" := (concat p q) (at level 20) : path_scope.
-Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope.
-Class IsEquiv {A B : Type} (f : A -> B) := {}.
-Axiom path_universe : forall {A B : Type} (f : A -> B) {feq : IsEquiv f}, (A = B).
-
-Definition Lift : Type@{i} -> Type@{j}
-  := Eval hnf in let lt := Type@{i} : Type@{j} in fun T => T.
-
-Definition lift {T} : T -> Lift T := fun x => x.
-
-Goal forall x y : Type, x = y.
-  intros.
-  pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''.
-- 
cgit v1.2.3