diff options
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_027.v (renamed from test-suite/bugs/opened/HoTT_coq_027.v) | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/closed/HoTT_coq_027.v index 7f283237a1..27834cc486 100644 --- a/test-suite/bugs/opened/HoTT_coq_027.v +++ b/test-suite/bugs/closed/HoTT_coq_027.v @@ -20,7 +20,7 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor. Set Printing Universes. Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C) -: FunctorToType@{Type Type Type Set} C. +: FunctorToType C. refine (@Build_Functor _ C _ TypeCat (fun x => F.(ObjectOf) x) (fun s d m => F.(MorphismOf) _ _ m)). |