From c7284415e4bdd3315c84c7d15d140d3fee000bc5 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 9 May 2014 10:13:32 -0400
Subject: Move opened bugs to bugs/opened

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

(limited to 'test-suite/bugs/closed/HoTT_coq_054.v')

diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
deleted file mode 100644
index f79fe1c1e..000000000
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ /dev/null
@@ -1,94 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
-Inductive Empty : Prop := .
-
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-
-Notation "x = y :> A" := (@paths A x y) : type_scope.
-Notation "x = y" := (x = y :>_) : type_scope.
-
-Arguments idpath {A a} , [A] a.
-
-Definition idmap {A : Type} : A -> A := fun x => x.
-
-Definition path_sum {A B : Type} (z z' : A + B)
-           (pq : match z, z' with
-                   | inl z0, inl z'0 => z0 = z'0
-                   | inr z0, inr z'0 => z0 = z'0
-                   | _, _ => Empty
-                 end)
-: z = z'.
-  destruct z, z', pq; exact idpath.
-Defined.
-
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
-  := match p with idpath => idpath end.
-
-Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
-              (* Fortunately, this unifies properly *)
-              (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
-  let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
-  ap f (path_sum x y pq) = path_sum (f x) (f y)
-     (* Coq appears to require *ALL* of the annotations *)
-     ((match x as x return match (x, y) with
-              (inl x', inl y') => x' = y'
-            | (inr x', inr y') => x' = y'
-            | _ => Empty
-          end -> match (f x, f y) with
-               | (inl x', inl y') => x' = y'
-               | (inr x', inr y') => x' = y'
-               | _ => Empty end with
-           | inl x' => match y as y return match y with
-                                               inl y' => x' = y'
-                                             | _ => Empty
-                                           end -> match f y with
-                                                    | inl y' => g x' = y'
-                                                    | _ => Empty end with
-                         | inl y' => ap g
-                         | inr y' => idmap
-                       end
-           | inr x' => match y as y return match y with
-                                               inr y' => x' = y'
-                                             | _ => Empty
-                                           end -> match f y with
-                                                    | inr y' => h x' = y'
-                                                    | _ => Empty end with
-                         | inl y' => idmap
-                         | inr y' => ap h
-                       end
-       end) pq).
-  destruct x; destruct y; destruct pq; reflexivity.
-Qed.
-(* Toplevel input, characters 1367-1374:
-Error:
-In environment
-A : Type
-B : Type
-A' : Type
-B' : Type
-g : A -> A'
-h : B -> B'
-x : A + B
-y : A + B
-pq :
-match x with
-| inl x' => match y with
-            | inl y' => x' = y'
-            | inr _ => Empty
-            end
-| inr x' => match y with
-            | inl _ => Empty
-            | inr y' => x' = y'
-            end
-end
-f :=
-fun z : A + B =>
-match z with
-| inl z' => inl (g z')
-| inr z' => inr (h z')
-end : A + B -> A' + B'
-x' : B
-y0 : A + B
-y' : B
-The term "x' = y'" has type "Type" while it is expected to have type
-"Prop" (Universe inconsistency). *)
-- 
cgit v1.2.3