From 45bcb4c7ad7aad8c2c63287870666339fe2ac1f2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 20 Jun 2014 15:45:57 +0200
Subject: Add fixed test-suite file for 3373.

---
 test-suite/bugs/closed/3373.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/3373.v

diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v
new file mode 100644
index 0000000000..16b137091d
--- /dev/null
+++ b/test-suite/bugs/closed/3373.v
@@ -0,0 +1,19 @@
+(* File reduced by coq-bug-finder from original input, then from 5968 lines to
+11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446
+lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then
+from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348
+lines to 320 lines, then from 328 lines to 302 lines, then from 332 lines to 21
+lines *)
+Set Universe Polymorphism.
+Axiom admit : forall {T}, T.
+Definition UU := Set.
+Definition UU' := Type.
+Definition hSet:= sigT (fun X : UU' => admit) .
+Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type.
+Coercion pr1hSet: hSet >-> Sortclass.
+Axiom binop : UU -> Type.
+Axiom setwithbinop : Type.
+Definition pr1setwithbinop : setwithbinop -> hSet.
+Goal True.
+pose (( @projT1 _ ( fun X : hSet@{Set j k} => binop X ) ) : _ -> hSet).
+Admitted.
\ No newline at end of file
-- 
cgit v1.2.3