diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_020.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_020.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 73da464bbe..babd180209 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -26,6 +26,7 @@ Ltac present_obj from to := | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * end. +#[universes(polymorphic)] Section NaturalTransformationComposition. Set Universe Polymorphism. Context `(C : @Category objC). @@ -58,6 +59,7 @@ Polymorphic Definition Cat0 : Category Empty_set Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C := Build_Functor Cat0 C (fun x => match x with end). +#[universes(polymorphic)] Section Law0. Polymorphic Variable objC : Type. Polymorphic Variable C : Category objC. |