diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/bugs/closed/HoTT_coq_014.v | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_014.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_014.v | 6 |
1 files changed, 3 insertions, 3 deletions
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' |