Add the -dont-load-proofs-argument
Add the -dont-load-proofs-argument

It speeds some things up a little bit.  The build times, from a csail cagnode
machine, are:
After     | File Name                         | Before
---------------------------------------------------------
7m49.957s | CommaCategoryFunctors             | 9m02.115s
2m34.311s | InducedLimitFunctors              | 2m33.737s
1m38.402s | SpecializedLaxCommaCategory       | 2m22.471s
0m51.757s | CommaCategoryFunctorProperties    | 0m51.607s
0m37.810s | UniversalProperties               | 0m37.566s
0m29.214s | Pullback                          | 0m29.528s
0m21.419s | Adjoint                           | 0m21.472s
0m19.976s | Examples                          | 0m19.788s
0m19.149s | ExponentialLaws                   | 0m25.199s
0m14.972s | AdjointPointwise                  | 0m14.985s
0m13.879s | DecidableDiscreteCategoryFunctors | 0m13.836s
0m13.800s | AdjointComposition                | 0m13.774s
0m13.649s | LaxCommaCategory                  | 0m15.833s
0m08.496s | MonoidalCategory                  | 0m13.263s
0m07.485s | AdjointUniversalMorphisms         | 0m07.484s
0m07.321s | CoendFunctor                      | 0m07.565s
0m07.086s | SpecializedCommaCategory          | 0m10.095s
0m05.941s | FunctorCategoryFunctorial         | 0m06.088s
0m05.032s | Correspondences                   | 0m04.931s
0m04.663s | SetColimits                       | 0m04.733s
0m04.070s | CommaCategory                     | 0m06.817s
0m03.777s | NaturalTransformation             | 0m04.788s
0m01.944s | LimitFunctorTheorems              | 0m01.929s
0m01.933s | SmallTranslation                  | 0m01.929s
0m01.905s | SemiSimplicialSets                | 0m01.907s
0m01.899s | NaturalEquivalence                | 0m02.581s
0m01.784s | SimplicialSets                    | 0m01.790s
0m01.750s | MetaEquivalence                   | 0m01.779s
0m01.707s | ChainCategory                     | 0m09.035s
0m01.692s | Coend                             | 0m01.703s
0m01.664s | Schema                            | 0m01.663s
0m01.596s | NatFacts                          | 0m07.336s
0m01.547s | Translation                       | 0m01.525s
0m01.508s | CanonicalStructureSimplification  | 0m03.385s
0m01.453s | Yoneda                            | 0m01.459s
0m01.444s | TypeclassSimplification           | 0m03.511s
0m01.314s | EnrichedCategory                  | 0m02.910s
0m01.296s | SigSigTCategory                   | 0m01.293s
0m01.286s | Graphs                            | 0m01.312s
0m01.227s | ProductLaws                       | 0m03.729s
0m01.210s | SigTCategory                      | 0m01.219s
0m01.206s | SetLimits                         | 0m01.205s
0m01.154s | SigCategory                       | 0m03.732s
0m01.039s | Duals                             | 0m03.884s
0m00.910s | Functor                           | 0m03.119s
0m00.906s | DiscreteCategoryFunctors          | 0m00.910s
0m00.900s | Limits                            | 0m00.902s
0m00.856s | Grothendieck                      | 0m00.871s
0m00.854s | SigTSigCategory                   | 0m00.840s
0m00.778s | Theorems                          | 0m00.711s
0m00.770s | EquivalenceClass                  | 0m02.137s
0m00.724s | SetCategoryFacts                  | 0m00.720s
0m00.713s | EquivalenceSet                    | 0m02.241s
0m00.710s | MetaTranslation                   | 0m00.709s
0m00.687s | Instance                          | 0m00.690s
0m00.659s | CategoryIsomorphisms              | 0m02.638s
0m00.646s | Hom                               | 0m02.019s
0m00.633s | FunctorialComposition             | 0m03.596s
0m00.629s | SigTInducedFunctors               | 0m00.635s
0m00.613s | ProductFunctors                   | 0m00.613s
0m00.598s | SigTSigInducedFunctors            | 0m00.599s
0m00.595s | PullbackFunctor                   | 0m00.595s
0m00.594s | LimitFunctors                     | 0m00.601s
0m00.591s | Common                            | 0m02.416s
0m00.588s | ProductInducedFunctors            | 0m03.325s
0m00.582s | EqualizerFunctor                  | 0m00.588s
0m00.571s | Groupoid                          | 0m00.567s
0m00.565s | Equalizer                         | 0m00.587s
0m00.561s | CategoryEquality                  | 0m01.012s
0m00.549s | SumCategory                       | 0m03.379s
0m00.549s | FunctorIsomorphisms               | 0m01.465s
0m00.545s | Products                          | 0m00.546s
0m00.537s | DualFunctor                       | 0m00.534s
0m00.500s | SmallCat                          | 0m02.225s
0m00.495s | PathsCategoryFunctors             | 0m00.498s
0m00.489s | SetCategoryProductFunctor         | 0m03.218s
0m00.461s | FunctorAttributes                 | 0m02.030s
0m00.455s | SmallSchema                       | 0m00.460s
0m00.436s | SubobjectClassifier               | 0m00.441s
0m00.406s | SetSchema                         | 0m00.407s
0m00.399s | AdjointUnit                       | 0m00.358s
0m00.392s | SpecializedCategory               | 0m00.558s
0m00.380s | Paths                             | 0m00.663s
0m00.378s | DecidableDiscreteCategory         | 0m01.772s
0m00.367s | FunctorProduct                    | 0m02.656s
0m00.353s | ProductCategory                   | 0m02.097s
0m00.348s | ComputableCategory                | 0m01.163s
0m00.345s | DecidableSmallCat                 | 0m00.341s
0m00.321s | DecidableComputableCategory       | 0m00.322s
0m00.316s | DecidableSetCategory              | 0m00.316s
0m00.314s | SetCategory                       | 0m01.969s
0m00.313s | GetArguments                      | 0m01.329s
0m00.313s | ProductNaturalTransformation      | 0m02.056s
0m00.305s | FEqualDep                         | 0m02.236s
0m00.304s | Subcategory                       | 0m02.861s
0m00.287s | GraphTranslation                  | 0m00.558s
0m00.262s | NaturalNumbersObject              | 0m02.018s
0m00.255s | FunctorCategory                   | 0m01.639s
0m00.247s | GroupCategory                     | 0m00.245s
0m00.242s | BoolCategory                      | 0m01.923s
0m00.235s | ComputableGraphCategory           | 0m02.248s
0m00.226s | EquivalenceRelationGenerator      | 0m00.476s
0m00.216s | PathsCategory                     | 0m01.609s
0m00.216s | InitialTerminalCategory           | 0m02.135s
0m00.202s | DiscreteCategory                  | 0m02.005s
0m00.195s | Category                          | 0m00.440s
0m00.188s | NatCategory                       | 0m01.448s
0m00.182s | StructureEquality                 | 0m01.884s
0m00.168s | DefinitionSimplification          | 0m00.919s
0m00.163s | Group                             | 0m00.163s
0m00.154s | Graph                             | 0m00.639s
0m00.149s | Notations                         | 0m01.373s

CategoricalData/catdb,CategoricalData/catdb,JasonGross/catdb,JasonGross/catdb