Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.

1 files changed, 4 insertions, 29 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
index fc15a88f7..fc99daab6 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.