diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 18:09:02 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 18:12:28 -0500 |
| commit | 7c102bb3a3798a234701fdc28a8e8ec28ee2549c (patch) | |
| tree | b75f8353b7a0ab3db161c77feb69636835bfba4a /test-suite/bugs/closed/HoTT_coq_014.v | |
| parent | 209faf81c432c39d4537f8b1dc5c9947d4349d30 (diff) | |
Univs: missing checks in evarsolve with candidates and missing a
whd_evar in refresh_universes.
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 ae3e50d7e..223a98de1 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' |