From 40c2154e369cf1a3434fe34679bb3a186df3199a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Jun 2014 17:03:25 +0200
Subject: Not considering test-suite file #89 as a bug anymore.

---
 test-suite/bugs/closed/HoTT_coq_089.v | 43 +++++++++++++++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_089.v | 43 -----------------------------------
 2 files changed, 43 insertions(+), 43 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_089.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_089.v

diff --git a/test-suite/bugs/closed/HoTT_coq_089.v b/test-suite/bugs/closed/HoTT_coq_089.v
new file mode 100644
index 0000000000..6841d6b279
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_089.v
@@ -0,0 +1,43 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Inductive type_paths (A : Type) : Type -> Prop
+  := idtypepath : type_paths A A.
+Monomorphic Definition comp_type_paths := Eval compute in type_paths@{Type Type}.
+Check comp_type_paths.
+(* comp_type_paths
+     : Type (* Top.12 *) -> Type (* Top.12 *) -> Prop *)
+(* This is terrible. *)
+
+Inductive type_paths' (A : Type) : Type -> Prop
+  := idtypepath' : type_paths' A A
+   | other_type_path : False -> forall B : Type, type_paths' A B.
+Monomorphic Definition comp_type_paths' := Eval compute in type_paths'.
+Check comp_type_paths'.
+(* comp_type_paths'
+     : Type (* Top.24 *) -> Type (* Top.23 *) -> Prop *)
+(* Ok, then ... *)
+
+(** Fail if it's [U0 -> U0 -> _], but not on [U0 -> U1 -> _]. *)
+Goal Type.
+Proof.
+  match type of comp_type_paths' with
+    | ?U0 -> ?U1 -> ?R
+      => exact (@comp_type_paths' nat U0)
+  end.
+Defined.
+
+Goal Type.
+Proof.
+   match type of comp_type_paths with
+    | ?U0 -> ?U1 -> ?R
+      => exact (@comp_type_paths nat U0)
+  end.
+  (* Toplevel input, characters 110-112:
+Error:
+The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)"
+while it is expected to have type "Type (* Top.51 *)"
+(Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51
+= Top.51)). *)
+  
+Defined.
diff --git a/test-suite/bugs/opened/HoTT_coq_089.v b/test-suite/bugs/opened/HoTT_coq_089.v
deleted file mode 100644
index 143f60404e..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_089.v
+++ /dev/null
@@ -1,43 +0,0 @@
-Set Universe Polymorphism.
-Set Printing Universes.
-
-Inductive type_paths (A : Type) : Type -> Prop
-  := idtypepath : type_paths A A.
-Monomorphic Definition comp_type_paths := Eval compute in type_paths.
-Check comp_type_paths.
-(* comp_type_paths
-     : Type (* Top.12 *) -> Type (* Top.12 *) -> Prop *)
-(* This is terrible. *)
-
-Inductive type_paths' (A : Type) : Type -> Prop
-  := idtypepath' : type_paths' A A
-   | other_type_path : False -> forall B : Type, type_paths' A B.
-Monomorphic Definition comp_type_paths' := Eval compute in type_paths'.
-Check comp_type_paths'.
-(* comp_type_paths'
-     : Type (* Top.24 *) -> Type (* Top.23 *) -> Prop *)
-(* Ok, then ... *)
-
-(** Fail if it's [U0 -> U0 -> _], but not on [U0 -> U1 -> _]. *)
-Goal Type.
-Proof.
-  match type of comp_type_paths' with
-    | ?U0 -> ?U1 -> ?R
-      => exact (@comp_type_paths' nat U0)
-  end.
-Defined.
-
-Goal Type.
-Proof.
-  Fail match type of comp_type_paths with
-    | ?U0 -> ?U1 -> ?R
-      => exact (@comp_type_paths nat U0)
-  end.
-  (* Toplevel input, characters 110-112:
-Error:
-The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)"
-while it is expected to have type "Type (* Top.51 *)"
-(Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51
-= Top.51)). *)
-  admit.
-Defined.
-- 
cgit v1.2.3