diff options
| author | Matthieu Sozeau | 2014-06-20 14:15:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-20 14:15:02 +0200 |
| commit | 1e2fa3a3a0ce3c5be93287ee034fc1fddc82d733 (patch) | |
| tree | 4a75e04b5d54c1a53f49db80fd20c04cec0195ae | |
| parent | cbf1315572bdb86dd5fc9102690f3585194bbc30 (diff) | |
Bug 27 closed now that universe contexts can be refined during the proof,
here instantiating a flexible level with Set.
| -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)). |