From 0b1507b16da38e883d63802db7c013e2c09665fd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 Jun 2014 12:59:48 +0200
Subject: Proper handling of the polymorphism flag for Context, fixing HoTT bug
 #98.

---
 test-suite/bugs/closed/HoTT_coq_098.v | 33 ++++-----------------------------
 1 file changed, 4 insertions(+), 29 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
index fc15a88f7b..fc99daab68 100644
--- a/test-suite/bugs/closed/HoTT_coq_098.v
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -37,35 +37,10 @@ Module success.
   Admitted.
 End success.
 
-Module failure.
+Module success2.
   Section SpecializedFunctor.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
-
-    Polymorphic Record SpecializedFunctor
-      := {
-          ObjectOf' : objC -> objD;
-          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
-        }.
-  End SpecializedFunctor.
-
-  Set Printing Universes.
-  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
-  (* Toplevel input, characters 73-94:
-Error:
-The term "GraphIndexingCategory (* Top.563 *)" has type
- "SpecializedCategory (* Top.563 Set *) GraphIndex"
-while it is expected to have type
- "SpecializedCategory (* Top.550 Top.551 *) ?7"
-(Universe inconsistency: Cannot enforce Set = Top.551)). *)
-  admit.
-  Defined.
-End failure.
-
-Module polycontext.
-  Section SpecializedFunctor.
-    Context `(C : @SpecializedCategory objC).
-    Context `(D : @SpecializedCategory objD).
+    Polymorphic Context `(C : @SpecializedCategory objC).
+    Polymorphic Context `(D : @SpecializedCategory objD).
 
     Polymorphic Record SpecializedFunctor
       := {
@@ -85,4 +60,4 @@ while it is expected to have type
 (Universe inconsistency: Cannot enforce Set = Top.551)). *)
   admit.
   Defined.
-End polycontext.
+End success2.
-- 
cgit v1.2.3