From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

---
 test-suite/bugs/closed/HoTT_coq_014.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index ae3e50d7..223a98de 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -3,9 +3,9 @@ Set Implicit Arguments.
 Generalizable All Variables.
 Set Universe Polymorphism.
 
-Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
-  Object :> _ := obj;
-  Morphism' : obj -> obj -> Type;
+Polymorphic Record SpecializedCategory@{l k} (obj : Type@{l}) := Build_SpecializedCategory' {
+  Object :> Type@{l} := obj;
+  Morphism' : obj -> obj -> Type@{k};
 
   Identity' : forall o, Morphism' o o;
   Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d'
-- 
cgit v1.2.3