Add LaxComma to categories.v

I had forgotten to export it when I originally ported it.
Merge pull request #639 from JasonGross/fix-lax-cat-deps

Add LaxComma to categories.v
Work around bugs 3773 and (probably) 3772

These are https://coq.inria.fr/bugs/show_bug.cgi?id=3773, open_constr no
longer does typeclass resolution, sometime within the past month, and
https://coq.inria.fr/bugs/show_bug.cgi?id=3772, [rewrite] is
inconsistent about unfolding and evar instantiation.

If we're actually going to merge this, we might want to put `simpl
rewrite` back to using `constr`, and make `simpl erewrite` variants that
use `open_constr` and `erewrite`.
Work around bug 3848

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3848, [refine]
sometimes incorrectly leaves over trivially solvable typeclass goals.
work around bug 3811 in extendable_const_isconnected_inO
Work around bug 3854

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3854, Typeclass
resolution fails where it used to succeed (change in the order of
unification in [refine] or in the order of canonical structure
resolution?)
dummy universe parameter for O_ind_internal, needed by Nullification
Work around bug(?) 3703

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3703, [rewrite] with
Keyed Unification fails to unfold some things that [rewrite] with
unkeyed unification unfolds

N.B. This commit does not compile with the pinned version of Coq.  In a
few commits, we'll bump the submodule.
Set Keyed Unification and bump Coq submodule

Bumping the submodule gives us some keyed unification, primitive
projection, and universe polymorphism fixes.

This closes #531 and #557 and #593.

The comment on the [Set Keyed Unification] directive was written by Mike
Shulman.

Note that we get a host of errors if we bump the submodule without
setting keyed unification; the current version of Coq doesn't attempt to
make [rewrite] work correctly in the presence of primitive projections
without [Set Keyed Unification].

A few files got slightly slower, but I think this is an acceptable diff
stat.

After    | File Name                                                 | Before   || Change
--------------------------------------------------------------------------------------------
3m55.20s | Total                                                     | 3m43.81s || +0m11.38s
--------------------------------------------------------------------------------------------
0m06.32s | categories/Adjoint/Composition/AssociativityLaw           | 0m01.33s || +0m04.99s
0m48.30s | categories/Adjoint/Pointwise                              | 0m45.14s || +0m03.15s
0m07.33s | categories/LaxComma/CoreLaws                              | 0m03.61s || +0m03.72s
0m05.22s | Factorization                                             | 0m07.68s || -0m02.46s
0m19.84s | hit/V                                                     | 0m20.84s || -0m01.00s
0m06.87s | categories/ExponentialLaws/Law3/Law                       | 0m08.26s || -0m01.38s
0m05.81s | Modalities/Modality                                       | 0m04.63s || +0m01.17s
0m02.29s | categories/Functor/Sum                                    | 0m01.14s || +0m01.15s
0m00.78s | Types/Equiv                                               | 0m01.78s || -0m01.00s
0m25.83s | Idempotents                                               | 0m25.73s || +0m00.09s
0m10.90s | categories/Adjoint/UniversalMorphisms/FunctorialLaws      | 0m10.07s || +0m00.83s
0m10.01s | contrib/Freudenthal                                       | 0m10.61s || -0m00.59s
0m07.37s | categories/ExponentialLaws/Law2/Law                       | 0m08.02s || -0m00.64s
0m06.68s | categories/ExponentialLaws/Law4/Law                       | 0m07.25s || -0m00.57s
0m04.28s | categories/Comma/ProjectionFunctors                       | 0m03.86s || +0m00.42s
0m02.74s | categories/Comma/Functorial                               | 0m02.74s || +0m00.00s
0m02.38s | categories/ExponentialLaws/Law1/Law                       | 0m01.50s || +0m00.87s
0m01.74s | categories/GroupoidCategory/Morphisms                     | 0m02.04s || -0m00.30s
0m01.68s | categories/Grothendieck/PseudofunctorToCat                | 0m01.17s || +0m00.51s
0m01.66s | hit/Flattening                                            | 0m01.97s || -0m00.31s
0m01.62s | contrib/HoTTBook                                          | 0m01.95s || -0m00.32s
0m01.58s | Modalities/ReflectiveSubuniverse                          | 0m01.53s || +0m00.05s
0m01.55s | hit/epi                                                   | 0m01.52s || +0m00.03s
0m01.50s | Modalities/Localization                                   | 0m01.86s || -0m00.36s
0m01.45s | categories/Category/Morphisms                             | 0m01.18s || +0m00.27s
0m01.35s | categories/Functor/Paths                                  | 0m00.94s || +0m00.41s
0m01.32s | categories/ExponentialLaws/Law4/Functors                  | 0m01.20s || +0m00.12s
0m01.28s | categories/Pseudofunctor/RewriteLaws                      | 0m00.80s || +0m00.48s
0m01.05s | contrib/HoTTBookExercises                                 | 0m01.01s || +0m00.04s
0m01.03s | categories/Adjoint/HomCoercions                           | 0m00.94s || +0m00.09s
0m00.99s | categories/Category/Sigma/OnMorphisms                     | 0m00.67s || +0m00.31s
0m00.97s | categories/Adjoint/Composition/IdentityLaws               | 0m00.74s || +0m00.23s
0m00.95s | categories/Adjoint/Composition/Core                       | 0m00.50s || +0m00.44s
0m00.88s | categories/Functor/Composition/Functorial/Attributes      | 0m00.63s || +0m00.25s
0m00.87s | categories/Yoneda                                         | 0m00.86s || +0m00.01s
0m00.87s | categories/Functor/Pointwise/Properties                   | 0m00.85s || +0m00.02s
0m00.86s | Types/Paths                                               | 0m00.86s || +0m00.00s
0m00.82s | hit/quotient                                              | 0m00.68s || +0m00.13s
0m00.80s | Basics/PathGroupoids                                      | 0m00.75s || +0m00.05s
0m00.78s | categories/Adjoint/UnitCounitCoercions                    | 0m00.71s || +0m00.07s
0m00.71s | categories/Comma/InducedFunctors                          | 0m00.72s || -0m00.01s
0m00.70s | categories/Comma/Core                                     | 0m00.45s || +0m00.24s
0m00.69s | categories/Pseudofunctor/FromFunctor                      | 0m00.73s || -0m00.04s
0m00.68s | Types/Sigma                                               | 0m00.64s || +0m00.04s
0m00.64s | categories/Pseudofunctor/Identity                         | 0m00.63s || +0m00.01s
0m00.64s | Basics/Equivalences                                       | 0m00.88s || -0m00.24s
0m00.63s | categories/LaxComma/CoreParts                             | 0m00.42s || +0m00.21s
0m00.63s | categories/Comma/Dual                                     | 0m00.42s || +0m00.21s
0m00.57s | EquivalenceVarieties                                      | 0m00.50s || +0m00.06s
0m00.56s | categories/Functor/Composition/Laws                       | 0m01.03s || -0m00.47s
0m00.54s | categories/Adjoint/UniversalMorphisms/FunctorialParts     | 0m00.53s || +0m00.01s
0m00.48s | categories/UniversalProperties                            | 0m01.07s || -0m00.59s
0m00.48s | categories/ExponentialLaws/Law0                           | 0m00.26s || +0m00.21s
0m00.46s | Extensions                                                | 0m00.51s || -0m00.04s
0m00.44s | categories/Category/Sum                                   | 0m00.45s || -0m00.01s
0m00.43s | categories/LaxComma/Core                                  | 0m00.40s || +0m00.02s
0m00.43s | categories/Structure/IdentityPrinciple                    | 0m00.41s || +0m00.02s
0m00.43s | categories/Functor/Prod/Universal                         | 0m00.35s || +0m00.08s
0m00.40s | categories/Functor/Attributes                             | 0m00.45s || -0m00.04s
0m00.39s | categories/ProductLaws                                    | 0m00.34s || +0m00.04s
0m00.36s | hit/Spheres                                               | 0m00.39s || -0m00.03s
0m00.34s | categories                                                | 0m00.34s || +0m00.00s
0m00.34s | categories/SetCategory/Morphisms                          | 0m00.32s || +0m00.02s
0m00.34s | categories/NaturalTransformation/Paths                    | 0m00.23s || +0m00.11s
0m00.34s | categories/Adjoint/Paths                                  | 0m00.32s || +0m00.02s
0m00.34s | categories/InitialTerminalCategory/Pseudofunctors         | 0m00.32s || +0m00.02s
0m00.34s | categories/NaturalTransformation/Isomorphisms             | 0m00.29s || +0m00.05s
0m00.34s | categories/DualFunctor                                    | 0m00.31s || +0m00.03s
0m00.31s | Modalities/Closed                                         | 0m00.32s || -0m00.01s
0m00.29s | categories/Category/Sigma/Core                            | 0m00.59s || -0m00.30s
0m00.29s | categories/Adjoint/UniversalMorphisms/Core                | 0m00.26s || +0m00.02s
0m00.26s | categories/Limits/Core                                    | 0m00.22s || +0m00.04s
0m00.26s | categories/HomotopyPreCategory                            | 0m00.26s || +0m00.00s
0m00.26s | categories/ExponentialLaws/Law1/Functors                  | 0m00.21s || +0m00.05s
0m00.25s | categories/FundamentalPreGroupoidCategory                 | 0m00.27s || -0m00.02s
0m00.24s | Types/Universe                                            | 0m00.27s || -0m00.03s
0m00.24s | Types/Prod                                                | 0m00.26s || -0m00.02s
0m00.24s | Fibrations                                                | 0m00.20s || +0m00.03s
0m00.24s | hit/Join                                                  | 0m00.26s || -0m00.02s
0m00.23s | TruncType                                                 | 0m00.23s || +0m00.00s
0m00.23s | hit/Connectedness                                         | 0m00.22s || +0m00.01s
0m00.22s | Types/Sum                                                 | 0m00.20s || +0m00.01s
0m00.22s | Modalities/Accessible                                     | 0m00.22s || +0m00.00s
0m00.22s | categories/Functor/Composition/Functorial/Core            | 0m00.24s || -0m00.01s
0m00.21s | Modalities/Nullification                                  | 0m00.18s || +0m00.03s
0m00.21s | categories/NaturalTransformation/Prod                     | 0m00.19s || +0m00.01s
0m00.21s | categories/Functor/Pointwise/Core                         | 0m00.24s || -0m00.03s
0m00.20s | Modalities/Open                                           | 0m00.20s || +0m00.00s
0m00.20s | categories/FunctorCategory/Morphisms                      | 0m00.19s || +0m00.01s
0m00.20s | ObjectClassifier                                          | 0m00.16s || +0m00.04s
0m00.20s | categories/Structure/Core                                 | 0m00.17s || +0m00.03s
0m00.20s | Tests                                                     | 0m00.22s || -0m00.01s
0m00.19s | categories/NaturalTransformation/Pointwise                | 0m00.18s || +0m00.01s
0m00.19s | categories/ExponentialLaws/Law2/Functors                  | 0m00.20s || -0m00.01s
0m00.19s | categories/HomFunctor                                     | 0m00.18s || +0m00.01s
0m00.19s | hit/Truncations                                           | 0m00.17s || +0m00.01s
0m00.19s | categories/Notations                                      | 0m00.16s || +0m00.03s
0m00.19s | categories/Grothendieck/ToSet                             | 0m00.19s || +0m00.00s
0m00.18s | categories/Pseudofunctor/Core                             | 0m00.13s || +0m00.04s
0m00.18s | hit/Pushout                                               | 0m00.21s || -0m00.03s
0m00.18s | categories/Functor/Prod/Core                              | 0m00.20s || -0m00.02s
0m00.17s | categories/Functor/Prod/Functorial                        | 0m00.17s || +0m00.00s
0m00.17s | HoTT                                                      | 0m00.18s || -0m00.00s
0m00.17s | categories/Category/Sigma/OnObjects                       | 0m00.15s || +0m00.02s
0m00.17s | categories/CategoryOfSections/Core                        | 0m00.13s || +0m00.04s
0m00.17s | hit/Circle                                                | 0m00.19s || -0m00.01s
0m00.16s | categories/Utf8                                           | 0m00.19s || -0m00.03s
0m00.16s | categories/FunctorCategory/Utf8                           | 0m00.15s || +0m00.01s
0m00.16s | categories/IndiscreteCategory                             | 0m00.14s || +0m00.01s
0m00.16s | categories/Limits/Functors                                | 0m00.19s || -0m00.03s
0m00.16s | categories/Category/Prod                                  | 0m00.10s || +0m00.06s
0m00.16s | categories/PseudonaturalTransformation/Core               | 0m00.15s || +0m00.01s
0m00.16s | categories/Functor/Utf8                                   | 0m00.12s || +0m00.04s
0m00.16s | categories/Functor                                        | 0m00.12s || +0m00.04s
0m00.16s | Types/Forall                                              | 0m00.15s || +0m00.01s
0m00.16s | categories/Functor/Composition                            | 0m00.16s || +0m00.00s
0m00.15s | categories/NaturalTransformation/Composition/Laws         | 0m00.16s || -0m00.01s
0m00.15s | categories/InitialTerminalCategory/Functors               | 0m00.14s || +0m00.00s
0m00.15s | HProp                                                     | 0m00.14s || +0m00.00s
0m00.15s | categories/FunctorCategory/Dual                           | 0m00.16s || -0m00.01s
0m00.15s | Modalities/Identity                                       | 0m00.15s || +0m00.00s
0m00.14s | Modalities/Notnot                                         | 0m00.14s || +0m00.00s
0m00.14s | UnivalenceImpliesFunext                                   | 0m00.12s || +0m00.02s
0m00.14s | hit/iso                                                   | 0m00.12s || +0m00.02s
0m00.14s | HSet                                                      | 0m00.14s || +0m00.00s
0m00.14s | hit/Suspension                                            | 0m00.12s || +0m00.02s
0m00.14s | categories/FunctorCategory/Functorial                     | 0m00.13s || +0m00.01s
0m00.14s | Tactics                                                   | 0m00.18s || -0m00.03s
0m00.14s | Types/Arrow                                               | 0m00.12s || +0m00.02s
0m00.14s | Utf8                                                      | 0m00.11s || +0m00.03s
0m00.14s | categories/KanExtensions/Functors                         | 0m00.14s || +0m00.00s
0m00.14s | categories/Adjoint/UnitCounit                             | 0m00.11s || +0m00.03s
0m00.13s | categories/Cat/Core                                       | 0m00.10s || +0m00.03s
0m00.13s | categories/ExponentialLaws/Law3/Functors                  | 0m00.12s || +0m00.01s
0m00.13s | Basics/Trunc                                              | 0m00.16s || -0m00.03s
0m00.13s | categories/Adjoint/Hom                                    | 0m00.14s || -0m00.01s
0m00.12s | categories/Functor/Composition/Functorial                 | 0m00.13s || -0m00.01s
0m00.12s | categories/Grothendieck/ToCat                             | 0m00.10s || +0m00.01s
0m00.12s | categories/Pseudofunctor                                  | 0m00.08s || +0m00.03s
0m00.12s | categories/Functor/Notations                              | 0m00.14s || -0m00.02s
0m00.12s | categories/NaturalTransformation/Utf8                     | 0m00.15s || -0m00.03s
0m00.11s | Types/Bool                                                | 0m00.09s || +0m00.02s
0m00.11s | categories/NatCategory                                    | 0m00.14s || -0m00.03s
0m00.11s | Tactics/RewriteModuloAssociativity                        | 0m00.10s || +0m00.00s
0m00.11s | categories/KanExtensions/Core                             | 0m00.11s || +0m00.00s
0m00.11s | categories/NaturalTransformation/Composition/Core         | 0m00.10s || +0m00.00s
0m00.11s | categories/Comma/Projection                               | 0m00.13s || -0m00.02s
0m00.10s | Basics/Overture                                           | 0m00.12s || -0m00.01s
0m00.10s | categories/LaxComma                                       | 0m00.11s || -0m00.00s
0m00.10s | categories/NaturalTransformation/Sum                      | 0m00.12s || -0m00.01s
0m00.10s | categories/InitialTerminalCategory/Core                   | 0m00.06s || +0m00.04s
0m00.10s | hit/unique_choice                                         | 0m00.12s || -0m00.01s
0m00.10s | categories/GroupoidCategory/Core                          | 0m00.10s || +0m00.00s
0m00.10s | categories/LaxComma/Utf8                                  | 0m00.06s || +0m00.04s
0m00.10s | categories/Adjoint                                        | 0m00.07s || +0m00.03s
0m00.10s | categories/Cat/Morphisms                                  | 0m00.10s || +0m00.00s
0m00.09s | categories/Adjoint/Dual                                   | 0m00.06s || +0m00.03s
0m00.09s | categories/LaxComma/Notations                             | 0m00.10s || -0m00.01s
0m00.09s | hit/Interval                                              | 0m00.06s || +0m00.03s
0m00.09s | categories/ExponentialLaws                                | 0m00.06s || +0m00.03s
0m00.09s | categories/Comma                                          | 0m00.11s || -0m00.02s
0m00.09s | categories/Adjoint/Notations                              | 0m00.06s || +0m00.03s
0m00.09s | categories/NaturalTransformation/Identity                 | 0m00.09s || +0m00.00s
0m00.09s | Types/Record                                              | 0m00.07s || +0m00.01s
0m00.09s | categories/NaturalTransformation/Composition/Functorial   | 0m00.09s || +0m00.00s
0m00.09s | categories/SetCategory/Core                               | 0m00.06s || +0m00.03s
0m00.09s | categories/Limits                                         | 0m00.09s || +0m00.00s
0m00.09s | categories/Adjoint/Composition/LawsTactic                 | 0m00.06s || +0m00.03s
0m00.09s | categories/Adjoint/Composition                            | 0m00.05s || +0m00.03s
0m00.08s | categories/Profunctor/Representable                       | 0m00.05s || +0m00.03s
0m00.08s | Conjugation                                               | 0m00.04s || +0m00.04s
0m00.08s | categories/Comma/Utf8                                     | 0m00.05s || +0m00.03s
0m00.08s | categories/DependentProduct                               | 0m00.08s || +0m00.00s
0m00.08s | categories/Category/Pi                                    | 0m00.06s || +0m00.02s
0m00.08s | categories/Category                                       | 0m00.08s || +0m00.00s
0m00.08s | categories/Profunctor/Core                                | 0m00.07s || +0m00.00s
0m00.08s | categories/PseudonaturalTransformation                    | 0m00.08s || +0m00.00s
0m00.08s | Functorish                                                | 0m00.08s || +0m00.00s
0m00.08s | coq/Init/Peano                                            | 0m00.06s || +0m00.02s
0m00.08s | categories/Grothendieck                                   | 0m00.09s || -0m00.00s
0m00.08s | categories/NaturalTransformation/Dual                     | 0m00.06s || +0m00.02s
0m00.08s | categories/Category/Objects                               | 0m00.09s || -0m00.00s
0m00.08s | Basics/FunextVarieties                                    | 0m00.06s || +0m00.02s
0m00.08s | categories/FunctorCategory                                | 0m00.08s || +0m00.00s
0m00.08s | categories/InitialTerminalCategory/NaturalTransformations | 0m00.09s || -0m00.00s
0m00.08s | categories/NaturalTransformation                          | 0m00.08s || +0m00.00s
0m00.08s | categories/FunctorCategory/Core                           | 0m00.07s || +0m00.00s
0m00.07s | categories/Adjoint/Utf8                                   | 0m00.06s || +0m00.01s
0m00.07s | categories/Category/Sigma                                 | 0m00.07s || +0m00.00s
0m00.07s | categories/Cat                                            | 0m00.06s || +0m00.01s
0m00.07s | categories/SetCategory/Functors                           | 0m00.05s || +0m00.02s
0m00.07s | categories/Functor/Dual                                   | 0m00.04s || +0m00.03s
0m00.07s | Basics/Contractible                                       | 0m00.06s || +0m00.01s
0m00.07s | categories/InitialTerminalCategory                        | 0m00.08s || -0m00.00s
0m00.07s | categories/ExponentialLaws/Law2                           | 0m00.08s || -0m00.00s
0m00.07s | categories/Category/Subcategory                           | 0m00.05s || +0m00.02s
0m00.07s | categories/SetCategory                                    | 0m00.06s || +0m00.01s
0m00.07s | categories/KanExtensions                                  | 0m00.07s || +0m00.00s
0m00.07s | categories/SetCategory/Functors/SetProp                   | 0m00.10s || -0m00.03s
0m00.07s | categories/FunctorCategory/Notations                      | 0m00.05s || +0m00.02s
0m00.07s | categories/Adjoint/UniversalMorphisms                     | 0m00.06s || +0m00.01s
0m00.06s | categories/Category/Utf8                                  | 0m00.05s || +0m00.00s
0m00.06s | categories/NaturalTransformation/Notations                | 0m00.06s || +0m00.00s
0m00.06s | categories/ExponentialLaws/Tactics                        | 0m00.07s || -0m00.01s
0m00.06s | categories/Profunctor/Notations                           | 0m00.06s || +0m00.00s
0m00.06s | categories/ExponentialLaws/Law1                           | 0m00.08s || -0m00.02s
0m00.06s | Types/Unit                                                | 0m00.08s || -0m00.02s
0m00.06s | categories/CategoryOfGroupoids                            | 0m00.09s || -0m00.03s
0m00.06s | categories/CategoryOfSections                             | 0m00.06s || +0m00.00s
0m00.06s | categories/Comma/Notations                                | 0m00.06s || +0m00.00s
0m00.06s | categories/InitialTerminalCategory/Notations              | 0m00.05s || +0m00.00s
0m00.06s | categories/Category/Core                                  | 0m00.07s || -0m00.01s
0m00.06s | hit/TwoSphere                                             | 0m00.05s || +0m00.00s
0m00.06s | NullHomotopy                                              | 0m00.04s || +0m00.01s
0m00.06s | categories/Profunctor/Identity                            | 0m00.06s || +0m00.00s
0m00.05s | coq/Init/Specif                                           | 0m00.04s || +0m00.01s
0m00.05s | categories/Category/Dual                                  | 0m00.06s || -0m00.00s
0m00.05s | categories/ExponentialLaws/Law3                           | 0m00.07s || -0m00.02s
0m00.05s | categories/ExponentialLaws/Law4                           | 0m00.03s || +0m00.02s
0m00.05s | hit/IntervalImpliesFunext                                 | 0m00.05s || +0m00.00s
0m00.05s | categories/Functor/Core                                   | 0m00.05s || +0m00.00s
0m00.05s | categories/Category/Univalent                             | 0m00.06s || -0m00.00s
0m00.05s | categories/Functor/Composition/Core                       | 0m00.04s || +0m00.01s
0m00.05s | categories/Structure                                      | 0m00.05s || +0m00.00s
0m00.05s | Tactics/BinderApply                                       | 0m00.03s || +0m00.02s
0m00.05s | categories/Category/Notations                             | 0m00.04s || +0m00.01s
0m00.05s | Types/Nat                                                 | 0m00.03s || +0m00.02s
0m00.05s | categories/Category/Subcategory/Full                      | 0m00.04s || +0m00.01s
0m00.05s | categories/Structure/Utf8                                 | 0m00.04s || +0m00.01s
0m00.05s | categories/Profunctor/Utf8                                | 0m00.07s || -0m00.02s
0m00.05s | categories/NaturalTransformation/Core                     | 0m00.06s || -0m00.00s
0m00.04s | categories/DiscreteCategory                               | 0m00.06s || -0m00.01s
0m00.04s | categories/Functor/Identity                               | 0m00.05s || -0m00.01s
0m00.04s | coq/Init/Datatypes                                        | 0m00.02s || +0m00.02s
0m00.04s | Basics/UniverseLevel                                      | 0m00.04s || +0m00.00s
0m00.04s | categories/Profunctor                                     | 0m00.05s || -0m00.01s
0m00.04s | Misc                                                      | 0m00.04s || +0m00.00s
0m00.04s | categories/Adjoint/Identity                               | 0m00.09s || -0m00.05s
0m00.04s | Types/Empty                                               | 0m00.03s || +0m00.01s
0m00.04s | categories/Functor/Pointwise                              | 0m00.08s || -0m00.04s
0m00.04s | Types                                                     | 0m00.04s || +0m00.00s
0m00.04s | categories/Functor/Prod                                   | 0m00.07s || -0m00.03s
0m00.04s | categories/Category/Subcategory/Wide                      | 0m00.06s || -0m00.01s
0m00.04s | categories/Structure/Notations                            | 0m00.04s || +0m00.00s
0m00.04s | Basics/Pointed                                            | 0m00.04s || +0m00.00s
0m00.04s | coq/Init/Logic_Type                                       | 0m00.04s || +0m00.00s
0m00.04s | UnivalenceAxiom                                           | 0m00.06s || -0m00.01s
0m00.04s | Basics                                                    | 0m00.04s || +0m00.00s
0m00.04s | categories/GroupoidCategory                               | 0m00.04s || +0m00.00s
0m00.03s | categories/Adjoint/Core                                   | 0m00.06s || -0m00.03s
0m00.03s | categories/Category/Strict                                | 0m00.04s || -0m00.01s
0m00.03s | coq/Init/Logic                                            | 0m00.02s || +0m00.00s
0m00.03s | categories/NaturalTransformation/Composition              | 0m00.07s || -0m00.04s
0m00.03s | coq/Unicode/Utf8_core                                     | 0m00.03s || +0m00.00s
0m00.03s | coq/Program/Tactics                                       | 0m00.05s || -0m00.02s
0m00.03s | FunextAxiom                                               | 0m00.02s || +0m00.00s
0m00.02s | coq/Init/Notations                                        | 0m00.02s || +0m00.00s
0m00.02s | coq/Unicode/Utf8                                          | 0m00.02s || +0m00.00s
0m00.02s | coq/Init/Prelude                                          | 0m00.02s || +0m00.00s
0m00.02s | coq/Init/Tactics                                          | 0m00.02s || +0m00.00s
0m00.01s | coq/Bool/Bool                                             | 0m00.02s || -0m00.01s
Revert "remove max(a,i) from Localize"

This reverts commit ed2dd379baa40fe48f633899e8cff7d03d50c6ab, which was
squished into a previous commit to make "dummy universe parameter for
O_ind_internal, needed by Nullification" compile with the pinned version
of Coq.

Because it's nicer to actually have the right universe in Localize
Global Set Primitive Projections

Idempotents got waay faster, though Factorization got somewhat slower.
Not quite sure what's up with that.

After    | File Name                                                 | Before   || Change
--------------------------------------------------------------------------------------------
3m47.71s | Total                                                     | 4m20.05s || -0m32.33s
--------------------------------------------------------------------------------------------
0m01.88s | Idempotents                                               | 0m30.73s || -0m28.85s
0m16.40s | Factorization                                             | 0m05.88s || +0m10.51s
0m17.75s | hit/V                                                     | 0m21.02s || -0m03.26s
0m02.78s | Modalities/Modality                                       | 0m06.33s || -0m03.55s
0m50.97s | categories/Adjoint/Pointwise                              | 0m53.29s || -0m02.32s
0m02.58s | Basics/Equivalences                                       | 0m00.66s || +0m01.92s
0m01.71s | categories/ExponentialLaws/Law1/Law                       | 0m02.71s || -0m01.00s
0m11.11s | categories/Adjoint/UniversalMorphisms/FunctorialLaws      | 0m12.02s || -0m00.91s
0m10.93s | contrib/Freudenthal                                       | 0m11.88s || -0m00.95s
0m07.92s | categories/ExponentialLaws/Law2/Law                       | 0m08.05s || -0m00.13s
0m07.39s | categories/ExponentialLaws/Law3/Law                       | 0m07.69s || -0m00.30s
0m07.28s | categories/ExponentialLaws/Law4/Law                       | 0m07.24s || +0m00.04s
0m07.24s | categories/LaxComma/CoreLaws                              | 0m07.99s || -0m00.75s
0m06.93s | categories/Adjoint/Composition/AssociativityLaw           | 0m06.67s || +0m00.25s
0m04.67s | categories/Comma/ProjectionFunctors                       | 0m04.92s || -0m00.25s
0m02.92s | categories/Comma/Functorial                               | 0m02.98s || -0m00.06s
0m02.50s | categories/Functor/Sum                                    | 0m02.48s || +0m00.02s
0m02.06s | hit/epi                                                   | 0m01.96s || +0m00.10s
0m01.88s | categories/GroupoidCategory/Morphisms                     | 0m01.96s || -0m00.08s
0m01.67s | contrib/HoTTBook                                          | 0m01.62s || +0m00.04s
0m01.60s | Modalities/ReflectiveSubuniverse                          | 0m01.79s || -0m00.18s
0m01.60s | Modalities/Localization                                   | 0m01.59s || +0m00.01s
0m01.58s | categories/Grothendieck/PseudofunctorToCat                | 0m01.82s || -0m00.24s
0m01.57s | categories/Category/Morphisms                             | 0m01.58s || -0m00.01s
0m01.50s | hit/Flattening                                            | 0m01.82s || -0m00.32s
0m01.47s | categories/ExponentialLaws/Law4/Functors                  | 0m01.47s || +0m00.00s
0m01.15s | categories/Pseudofunctor/RewriteLaws                      | 0m01.38s || -0m00.23s
0m01.10s | categories/Functor/Paths                                  | 0m01.42s || -0m00.31s
0m01.08s | categories/Adjoint/Composition/IdentityLaws               | 0m00.96s || +0m00.12s
0m01.08s | categories/Category/Sigma/OnMorphisms                     | 0m01.09s || -0m00.01s
0m00.99s | categories/Adjoint/HomCoercions                           | 0m01.08s || -0m00.09s
0m00.99s | categories/Adjoint/Composition/Core                       | 0m01.02s || -0m00.03s
0m00.92s | categories/Functor/Composition/Functorial/Attributes      | 0m00.89s || +0m00.03s
0m00.91s | categories/Functor/Pointwise/Properties                   | 0m00.98s || -0m00.06s
0m00.90s | hit/quotient                                              | 0m00.97s || -0m00.06s
0m00.87s | contrib/HoTTBookExercises                                 | 0m01.08s || -0m00.21s
0m00.86s | categories/Yoneda                                         | 0m00.98s || -0m00.12s
0m00.86s | Basics/PathGroupoids                                      | 0m00.87s || -0m00.01s
0m00.82s | categories/Comma/InducedFunctors                          | 0m00.86s || -0m00.04s
0m00.73s | categories/Comma/Core                                     | 0m00.71s || +0m00.02s
0m00.71s | categories/Pseudofunctor/FromFunctor                      | 0m00.74s || -0m00.03s
0m00.70s | categories/Pseudofunctor/Identity                         | 0m00.66s || +0m00.03s
0m00.70s | categories/Adjoint/UniversalMorphisms/FunctorialParts     | 0m00.66s || +0m00.03s
0m00.68s | Types/Sigma                                               | 0m00.67s || +0m00.01s
0m00.66s | Types/Paths                                               | 0m00.90s || -0m00.24s
0m00.64s | categories/Comma/Dual                                     | 0m00.69s || -0m00.04s
0m00.64s | categories/Adjoint/UnitCounitCoercions                    | 0m00.86s || -0m00.21s
0m00.63s | categories/LaxComma/CoreParts                             | 0m00.60s || +0m00.03s
0m00.60s | EquivalenceVarieties                                      | 0m00.56s || +0m00.03s
0m00.60s | categories/Functor/Composition/Laws                       | 0m00.60s || +0m00.00s
0m00.57s | Types/Equiv                                               | 0m00.76s || -0m00.19s
0m00.52s | categories/UniversalProperties                            | 0m00.50s || +0m00.02s
0m00.50s | categories/ExponentialLaws/Law0                           | 0m00.52s || -0m00.02s
0m00.48s | categories/Category/Sum                                   | 0m00.51s || -0m00.03s
0m00.47s | categories/Functor/Attributes                             | 0m00.47s || +0m00.00s
0m00.46s | categories/Functor/Prod/Universal                         | 0m00.47s || -0m00.00s
0m00.44s | Extensions                                                | 0m00.55s || -0m00.11s
0m00.42s | categories/Adjoint/Paths                                  | 0m00.36s || +0m00.06s
0m00.41s | categories/LaxComma/Core                                  | 0m00.43s || -0m00.02s
0m00.39s | categories/ProductLaws                                    | 0m00.40s || -0m00.01s
0m00.37s | categories                                                | 0m00.40s || -0m00.03s
0m00.37s | categories/InitialTerminalCategory/Pseudofunctors         | 0m00.36s || +0m00.01s
0m00.35s | Modalities/Closed                                         | 0m00.32s || +0m00.02s
0m00.34s | categories/Category/Sigma/Core                            | 0m00.32s || +0m00.02s
0m00.34s | hit/Spheres                                               | 0m00.36s || -0m00.01s
0m00.33s | categories/Limits/Core                                    | 0m00.31s || +0m00.02s
0m00.33s | categories/Structure/IdentityPrinciple                    | 0m00.44s || -0m00.10s
0m00.32s | categories/DualFunctor                                    | 0m00.34s || -0m00.02s
0m00.30s | Modalities/Open                                           | 0m00.23s || +0m00.06s
0m00.30s | categories/FundamentalPreGroupoidCategory                 | 0m00.30s || +0m00.00s
0m00.30s | categories/SetCategory/Morphisms                          | 0m00.40s || -0m00.10s
0m00.30s | categories/NaturalTransformation/Paths                    | 0m00.26s || +0m00.03s
0m00.30s | categories/Functor/Composition/Functorial/Core            | 0m00.30s || +0m00.00s
0m00.30s | categories/NaturalTransformation/Isomorphisms             | 0m00.30s || +0m00.00s
0m00.30s | categories/Adjoint/UniversalMorphisms/Core                | 0m00.30s || +0m00.00s
0m00.30s | hit/Connectedness                                         | 0m00.28s || +0m00.01s
0m00.29s | Types/Universe                                            | 0m00.27s || +0m00.01s
0m00.28s | Types/Prod                                                | 0m00.25s || +0m00.03s
0m00.26s | categories/HomotopyPreCategory                            | 0m00.21s || +0m00.05s
0m00.25s | categories/ExponentialLaws/Law1/Functors                  | 0m00.24s || +0m00.01s
0m00.24s | categories/Functor/Pointwise/Core                         | 0m00.30s || -0m00.06s
0m00.24s | Fibrations                                                | 0m00.25s || -0m00.01s
0m00.24s | hit/Join                                                  | 0m00.27s || -0m00.03s
0m00.23s | categories/FunctorCategory/Morphisms                      | 0m00.21s || +0m00.02s
0m00.23s | hit/Truncations                                           | 0m00.20s || +0m00.03s
0m00.22s | Modalities/Nullification                                  | 0m00.17s || +0m00.04s
0m00.22s | categories/NaturalTransformation/Pointwise                | 0m00.19s || +0m00.03s
0m00.22s | categories/ExponentialLaws/Law2/Functors                  | 0m00.20s || +0m00.01s
0m00.22s | Types/Sum                                                 | 0m00.27s || -0m00.05s
0m00.22s | Modalities/Accessible                                     | 0m00.24s || -0m00.01s
0m00.22s | categories/NaturalTransformation/Composition/Laws         | 0m00.18s || +0m00.04s
0m00.21s | categories/Functor/Prod/Core                              | 0m00.24s || -0m00.03s
0m00.20s | categories/Limits/Functors                                | 0m00.19s || +0m00.01s
0m00.20s | categories/HomFunctor                                     | 0m00.24s || -0m00.03s
0m00.20s | HoTT                                                      | 0m00.22s || -0m00.01s
0m00.20s | hit/Circle                                                | 0m00.18s || +0m00.02s
0m00.20s | categories/InitialTerminalCategory/Functors               | 0m00.19s || +0m00.01s
0m00.20s | categories/FunctorCategory/Dual                           | 0m00.16s || +0m00.04s
0m00.19s | hit/Pushout                                               | 0m00.22s || -0m00.03s
0m00.19s | categories/Functor/Prod/Functorial                        | 0m00.16s || +0m00.03s
0m00.19s | categories/Notations                                      | 0m00.19s || +0m00.00s
0m00.18s | categories/Utf8                                           | 0m00.20s || -0m00.02s
0m00.18s | categories/Category/Sigma/OnObjects                       | 0m00.18s || +0m00.00s
0m00.18s | categories/PseudonaturalTransformation/Core               | 0m00.17s || +0m00.00s
0m00.18s | HSet                                                      | 0m00.14s || +0m00.03s
0m00.18s | ObjectClassifier                                          | 0m00.23s || -0m00.05s
0m00.18s | categories/Functor/Utf8                                   | 0m00.16s || +0m00.01s
0m00.18s | categories/Functor                                        | 0m00.20s || -0m00.02s
0m00.18s | categories/Structure/Core                                 | 0m00.20s || -0m00.02s
0m00.18s | Tests                                                     | 0m00.22s || -0m00.04s
0m00.17s | categories/Grothendieck/ToSet                             | 0m00.21s || -0m00.03s
0m00.17s | categories/FunctorCategory/Utf8                           | 0m00.18s || -0m00.00s
0m00.17s | categories/NaturalTransformation/Prod                     | 0m00.20s || -0m00.03s
0m00.17s | categories/Functor/Notations                              | 0m00.15s || +0m00.02s
0m00.17s | categories/Pseudofunctor/Core                             | 0m00.15s || +0m00.02s
0m00.17s | categories/Adjoint                                        | 0m00.16s || +0m00.01s
0m00.17s | Utf8                                                      | 0m00.13s || +0m00.04s
0m00.17s | categories/KanExtensions/Functors                         | 0m00.16s || +0m00.01s
0m00.16s | categories/Functor/Composition/Functorial                 | 0m00.14s || +0m00.01s
0m00.16s | hit/iso                                                   | 0m00.19s || -0m00.03s
0m00.16s | categories/Functor/Composition                            | 0m00.14s || +0m00.01s
0m00.15s | categories/Cat/Core                                       | 0m00.16s || -0m00.01s
0m00.15s | categories/IndiscreteCategory                             | 0m00.16s || -0m00.01s
0m00.15s | Tactics                                                   | 0m00.14s || +0m00.00s
0m00.15s | categories/KanExtensions/Core                             | 0m00.12s || +0m00.03s
0m00.15s | categories/NaturalTransformation/Utf8                     | 0m00.17s || -0m00.02s
0m00.15s | categories/Comma/Projection                               | 0m00.14s || +0m00.00s
0m00.14s | Modalities/Notnot                                         | 0m00.15s || -0m00.00s
0m00.14s | categories/Category/Prod                                  | 0m00.15s || -0m00.00s
0m00.14s | categories/Adjoint/Hom                                    | 0m00.13s || +0m00.01s
0m00.14s | hit/Suspension                                            | 0m00.16s || -0m00.01s
0m00.14s | TruncType                                                 | 0m00.28s || -0m00.14s
0m00.14s | categories/NatCategory                                    | 0m00.12s || +0m00.02s
0m00.14s | categories/CategoryOfSections/Core                        | 0m00.16s || -0m00.01s
0m00.14s | Types/Forall                                              | 0m00.16s || -0m00.01s
0m00.14s | categories/SetCategory/Functors/SetProp                   | 0m00.10s || +0m00.04s
0m00.14s | HProp                                                     | 0m00.13s || +0m00.01s
0m00.13s | categories/ExponentialLaws/Law3/Functors                  | 0m00.14s || -0m00.01s
0m00.13s | Types/Arrow                                               | 0m00.14s || -0m00.01s
0m00.13s | Tactics/RewriteModuloAssociativity                        | 0m00.12s || +0m00.01s
0m00.13s | categories/Adjoint/UnitCounit                             | 0m00.16s || -0m00.03s
0m00.12s | categories/Category/Pi                                    | 0m00.07s || +0m00.04s
0m00.12s | UnivalenceImpliesFunext                                   | 0m00.13s || -0m00.01s
0m00.12s | categories/Comma                                          | 0m00.13s || -0m00.01s
0m00.12s | categories/NaturalTransformation/Sum                      | 0m00.09s || +0m00.03s
0m00.12s | hit/unique_choice                                         | 0m00.16s || -0m00.04s
0m00.12s | categories/LaxComma/Utf8                                  | 0m00.10s || +0m00.01s
0m00.12s | Modalities/Identity                                       | 0m00.14s || -0m00.02s
0m00.11s | Basics/Overture                                           | 0m00.12s || -0m00.00s
0m00.11s | categories/Category                                       | 0m00.12s || -0m00.00s
0m00.11s | categories/ExponentialLaws                                | 0m00.07s || +0m00.03s
0m00.11s | categories/Grothendieck/ToCat                             | 0m00.12s || -0m00.00s
0m00.11s | categories/FunctorCategory/Functorial                     | 0m00.12s || -0m00.00s
0m00.10s | categories/InitialTerminalCategory/NaturalTransformations | 0m00.10s || +0m00.00s
0m00.10s | categories/DependentProduct                               | 0m00.09s || +0m00.01s
0m00.10s | categories/LaxComma/Notations                             | 0m00.08s || +0m00.02s
0m00.10s | Types/Bool                                                | 0m00.09s || +0m00.01s
0m00.10s | categories/NaturalTransformation/Identity                 | 0m00.09s || +0m00.01s
0m00.10s | categories/NaturalTransformation/Notations                | 0m00.09s || +0m00.01s
0m00.10s | Types/Record                                              | 0m00.11s || -0m00.00s
0m00.09s | categories/PseudonaturalTransformation                    | 0m00.07s || +0m00.01s
0m00.09s | categories/ExponentialLaws/Tactics                        | 0m00.06s || +0m00.03s
0m00.09s | categories/Category/Dual                                  | 0m00.06s || +0m00.03s
0m00.09s | Basics/Trunc                                              | 0m00.15s || -0m00.06s
0m00.09s | Types/Unit                                                | 0m00.10s || -0m00.01s
0m00.09s | categories/Grothendieck                                   | 0m00.09s || +0m00.00s
0m00.09s | categories/CategoryOfGroupoids                            | 0m00.09s || +0m00.00s
0m00.09s | categories/GroupoidCategory/Core                          | 0m00.10s || -0m00.01s
0m00.09s | categories/Category/Objects                               | 0m00.11s || -0m00.02s
0m00.09s | categories/Cat/Morphisms                                  | 0m00.08s || +0m00.00s
0m00.09s | categories/Adjoint/Composition/LawsTactic                 | 0m00.07s || +0m00.01s
0m00.08s | categories/Profunctor/Representable                       | 0m00.09s || -0m00.00s
0m00.08s | categories/Comma/Utf8                                     | 0m00.08s || +0m00.00s
0m00.08s | categories/Adjoint/Dual                                   | 0m00.07s || +0m00.00s
0m00.08s | categories/LaxComma                                       | 0m00.10s || -0m00.02s
0m00.08s | categories/Profunctor                                     | 0m00.07s || +0m00.00s
0m00.08s | categories/Functor/Dual                                   | 0m00.06s || +0m00.02s
0m00.08s | Functorish                                                | 0m00.09s || -0m00.00s
0m00.08s | categories/SetCategory/Core                               | 0m00.07s || +0m00.00s
0m00.08s | categories/ExponentialLaws/Law1                           | 0m00.06s || +0m00.02s
0m00.08s | categories/ExponentialLaws/Law2                           | 0m00.07s || +0m00.00s
0m00.08s | Misc                                                      | 0m00.03s || +0m00.05s
0m00.08s | categories/Pseudofunctor                                  | 0m00.09s || -0m00.00s
0m00.08s | categories/Adjoint/Notations                              | 0m00.08s || +0m00.00s
0m00.08s | categories/Category/Subcategory/Wide                      | 0m00.08s || +0m00.00s
0m00.08s | categories/FunctorCategory                                | 0m00.07s || +0m00.00s
0m00.08s | categories/NaturalTransformation                          | 0m00.10s || -0m00.02s
0m00.08s | hit/TwoSphere                                             | 0m00.08s || +0m00.00s
0m00.08s | categories/Limits                                         | 0m00.09s || -0m00.00s
0m00.08s | categories/Adjoint/UniversalMorphisms                     | 0m00.10s || -0m00.02s
0m00.08s | categories/FunctorCategory/Core                           | 0m00.09s || -0m00.00s
0m00.08s | categories/Profunctor/Utf8                                | 0m00.07s || +0m00.00s
0m00.08s | categories/NaturalTransformation/Composition/Core         | 0m00.12s || -0m00.03s
0m00.07s | categories/Adjoint/Utf8                                   | 0m00.07s || +0m00.00s
0m00.07s | categories/Category/Utf8                                  | 0m00.07s || +0m00.00s
0m00.07s | categories/Cat                                            | 0m00.10s || -0m00.03s
0m00.07s | Basics/Contractible                                       | 0m00.05s || +0m00.02s
0m00.07s | categories/InitialTerminalCategory                        | 0m00.08s || -0m00.00s
0m00.07s | categories/ExponentialLaws/Law3                           | 0m00.07s || +0m00.00s
0m00.07s | categories/ExponentialLaws/Law4                           | 0m00.06s || +0m00.01s
0m00.07s | categories/Category/Subcategory                           | 0m00.04s || +0m00.03s
0m00.07s | coq/Init/Peano                                            | 0m00.07s || +0m00.00s
0m00.07s | categories/InitialTerminalCategory/Core                   | 0m00.08s || -0m00.00s
0m00.07s | categories/Functor/Pointwise                              | 0m00.06s || +0m00.01s
0m00.07s | categories/Functor/Prod                                   | 0m00.06s || +0m00.01s
0m00.07s | categories/NaturalTransformation/Composition              | 0m00.07s || +0m00.00s
0m00.07s | Basics/FunextVarieties                                    | 0m00.07s || +0m00.00s
0m00.07s | categories/KanExtensions                                  | 0m00.09s || -0m00.01s
0m00.07s | categories/Structure                                      | 0m00.07s || +0m00.00s
0m00.07s | categories/NaturalTransformation/Composition/Functorial   | 0m00.10s || -0m00.03s
0m00.07s | categories/Category/Subcategory/Full                      | 0m00.04s || +0m00.03s
0m00.07s | categories/NaturalTransformation/Core                     | 0m00.07s || +0m00.00s
0m00.06s | categories/DiscreteCategory                               | 0m00.07s || -0m00.01s
0m00.06s | categories/Adjoint/Core                                   | 0m00.03s || +0m00.03s
0m00.06s | categories/Category/Sigma                                 | 0m00.08s || -0m00.02s
0m00.06s | categories/Profunctor/Core                                | 0m00.07s || -0m00.01s
0m00.06s | hit/Interval                                              | 0m00.09s || -0m00.03s
0m00.06s | categories/Profunctor/Notations                           | 0m00.07s || -0m00.01s
0m00.06s | categories/Adjoint/Identity                               | 0m00.06s || +0m00.00s
0m00.06s | Types/Empty                                               | 0m00.04s || +0m00.01s
0m00.06s | categories/CategoryOfSections                             | 0m00.07s || -0m00.01s
0m00.06s | categories/Category/Univalent                             | 0m00.07s || -0m00.01s
0m00.06s | categories/Comma/Notations                                | 0m00.08s || -0m00.02s
0m00.06s | categories/InitialTerminalCategory/Notations              | 0m00.07s || -0m00.01s
0m00.06s | NullHomotopy                                              | 0m00.06s || +0m00.00s
0m00.06s | categories/Category/Notations                             | 0m00.06s || +0m00.00s
0m00.06s | categories/Profunctor/Identity                            | 0m00.08s || -0m00.02s
0m00.06s | Basics                                                    | 0m00.04s || +0m00.01s
0m00.06s | categories/GroupoidCategory                               | 0m00.06s || +0m00.00s
0m00.06s | categories/Adjoint/Composition                            | 0m00.06s || +0m00.00s
0m00.05s | Conjugation                                               | 0m00.07s || -0m00.02s
0m00.05s | categories/SetCategory/Functors                           | 0m00.06s || -0m00.00s
0m00.05s | hit/IntervalImpliesFunext                                 | 0m00.04s || +0m00.01s
0m00.05s | categories/NaturalTransformation/Dual                     | 0m00.08s || -0m00.03s
0m00.05s | categories/Structure/Notations                            | 0m00.07s || -0m00.02s
0m00.05s | categories/Functor/Composition/Core                       | 0m00.06s || -0m00.00s
0m00.05s | UnivalenceAxiom                                           | 0m00.03s || +0m00.02s
0m00.05s | categories/Structure/Utf8                                 | 0m00.04s || +0m00.01s
0m00.04s | categories/Functor/Identity                               | 0m00.04s || +0m00.00s
0m00.04s | Basics/UniverseLevel                                      | 0m00.04s || +0m00.00s
0m00.04s | categories/Category/Strict                                | 0m00.02s || +0m00.02s
0m00.04s | categories/Functor/Core                                   | 0m00.05s || -0m00.01s
0m00.04s | categories/SetCategory                                    | 0m00.05s || -0m00.01s
0m00.04s | categories/Category/Core                                  | 0m00.08s || -0m00.04s
0m00.04s | coq/Init/Logic_Type                                       | 0m00.04s || +0m00.00s
0m00.04s | Tactics/BinderApply                                       | 0m00.05s || -0m00.01s
0m00.04s | Types/Nat                                                 | 0m00.02s || +0m00.02s
0m00.04s | categories/FunctorCategory/Notations                      | 0m00.06s || -0m00.01s
0m00.04s | FunextAxiom                                               | 0m00.04s || +0m00.00s
0m00.03s | coq/Init/Specif                                           | 0m00.05s || -0m00.02s
0m00.03s | Types                                                     | 0m00.05s || -0m00.02s
0m00.03s | coq/Program/Tactics                                       | 0m00.04s || -0m00.01s
0m00.02s | coq/Init/Datatypes                                        | 0m00.04s || -0m00.02s
0m00.02s | coq/Init/Logic                                            | 0m00.01s || +0m00.01s
0m00.02s | coq/Unicode/Utf8                                          | 0m00.02s || +0m00.00s
0m00.02s | coq/Unicode/Utf8_core                                     | 0m00.02s || +0m00.00s
0m00.02s | coq/Init/Prelude                                          | 0m00.02s || +0m00.00s
0m00.02s | coq/Bool/Bool                                             | 0m00.01s || +0m00.01s
0m00.02s | coq/Init/Tactics                                          | 0m00.03s || -0m00.00s
0m00.02s | Basics/Pointed                                            | 0m00.04s || -0m00.02s
0m00.01s | coq/Init/Notations                                        | 0m00.03s || -0m00.01s