diff options
| author | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
| commit | 414890675cb72fd9286e19521a746677c06e784e (patch) | |
| tree | 14599a23215356ac472ac483ad564c11eb53c1fc /test-suite/bugs | |
| parent | 396c77feb0cced3965f90f65c681e48c528636d5 (diff) | |
| parent | 15b1856edd593b39d63d23584a4f5acec0eeb592 (diff) | |
Merge PR#613: Cumulativity for inductive types
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/3330.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index e3b5e94356..672fb3f131 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,7 +1072,7 @@ Section Adjunction. Variable F : Functor C D. Variable G : Functor D C. - Let Adjunction_Type := + Let Adjunction_Type := Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). Record AdjunctionHom := |