diff options
| author | Amin Timany | 2017-04-27 20:16:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:51:16 +0200 |
| commit | 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac (patch) | |
| tree | 916f61f35650966d7a288e8579279b0a3e45afc6 /test-suite/bugs/closed | |
| parent | 7b5fcef8a0fb3b97a3980f10596137234061990f (diff) | |
Fix bugs and add an option for cumulativity
Diffstat (limited to 'test-suite/bugs/closed')
| -rw-r--r-- | test-suite/bugs/closed/3330.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index e3b5e94356..a497e7a987 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function Open Scope function_scope. +Set Printing Universes. Set Printing All. + Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. @@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism. Delimit Scope category_scope with category. Delimit Scope object_scope with object. - +Set Printing Universes. +Set Printing All. Record PreCategory := Build_PreCategory' { object :> Type; @@ -1069,8 +1072,10 @@ Section Adjunction. Variable F : Functor C D. Variable G : Functor D C. - Let Adjunction_Type := - Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). +(* Let Adjunction_Type := + Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).*) + + Set Printing All. Set Printing Universes. Record AdjunctionHom := { |