Use maintainer mode in configure

This will automatically rebuild Makefile and configure if needed,
preventing problems like the missing targets in
https://github.com/HoTT/HoTT/pull/286#issuecomment-30749614.  This means
that we now depend on having autobuild around to run ./configure and
make, though I think that systems without them will simply get warnings,
and not errors.
Remove support for ssreflect

The ssreflect support has been inactive for a long time now. It would
take some effort to make it work, and it is unlikely this will happen.
So I am ripping it out. If in the future anyone wants to put it back
in, they can have a look at the history and go from there.
Remove further traces of ssreflect.
Update a reference in a comment that was renamed

Closes #297.
Split off HoTTBookExercises.v from HoTTBook.v.

Since exercise formalizations tend to be a lot wordier than mere
backreferences to theorems in the library (as discussed in PR #302),
this patch splits HoTTBook.v into a separate exercises file, which
contains formalizations for the exercises in the HoTT book.  etc/Book.v
now takes a new flag, '--exercises', which instructs it to extract out
only exercises from the book; its default setting now no longer inserts
markers for exercises.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>
Merge pull request #303 from ezyang/split-exercises

Split off HoTTBookExercises.v from HoTTBook.v.
Add HoTTBookExercises.v to Makefile_targets.mk

This was forgotten in #303.
Merge pull request #292 from andrejbauer/master

Remove ssreflect "support" which isn't working anyhow.
Merge pull request #290 from JasonGross/enable-maintainer-mode

Use maintainer mode in configure
Move developer note to non-rendered section.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>
Solutions for 1.2-3, expand 1.1 solution.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>
Merge pull request #302 from ezyang/exercises

Solutions for 1.2-3, expand 1.1 solution.
Remove spaces
Squash a bunch of Matthieu's code improvements

From polyproj branch
Fix up some transparency issues

Opacity is respected by the kernel in polyproj Coq, and we really wanted
[simpl never] for most things, anyway.

After    | File Name                                                | Before
------------------------------------------------------------------------------
8m20.22s | Total                                                    | 8m18.24s
------------------------------------------------------------------------------
1m45.56s | categories/Comma/ProjectionFunctors                      | 1m44.65s
0m32.67s | categories/Adjoint/Composition/AssociativityLaw          | 0m32.79s
0m25.24s | categories/Grothendieck/PseudofunctorToCat               | 0m24.74s
0m17.10s | categories/ExponentialLaws/Law4/Functors                 | 0m17.80s
0m16.96s | categories/Adjoint/UnitCounitCoercions                   | 0m16.84s
0m16.31s | categories/Comma/InducedFunctors                         | 0m16.40s
0m16.10s | categories/FunctorCategory/Dual                          | 0m16.22s
0m13.00s | categories/Functor/Pointwise/Properties                  | 0m12.44s
0m12.99s | hit/Flattening                                           | 0m13.43s
0m12.79s | categories/Pseudofunctor/Core                            | 0m12.71s
0m12.16s | categories/Adjoint/Composition/Core                      | 0m11.84s
0m11.79s | categories/Adjoint/Dual                                  | 0m11.86s
0m11.70s | categories/Adjoint/Composition/IdentityLaws              | 0m11.10s
0m11.10s | categories/Pseudofunctor/FromFunctor                     | 0m10.29s
0m08.75s | categories/ExponentialLaws/Law1/Law                      | 0m08.24s
0m08.72s | categories/Functor/Prod/Universal                        | 0m08.55s
0m08.09s | categories/GroupoidCategory/Morphisms                    | 0m08.44s
0m07.42s | categories/UniversalProperties                           | 0m06.95s
0m07.07s | hit/Connectedness                                        | 0m07.37s
0m06.79s | categories/Comma/Dual                                    | 0m06.58s
0m06.36s | categories/Adjoint/Paths                                 | 0m06.38s
0m05.80s | categories/Adjoint/UnitCounit                            | 0m05.90s
0m05.78s | categories/Functor/Sum                                   | 0m05.67s
0m05.69s | categories/Functor/Paths                                 | 0m06.16s
0m05.64s | categories/Category/Morphisms                            | 0m05.89s
0m05.18s | EquivalenceVarieties                                     | 0m05.18s
0m04.88s | categories/ExponentialLaws/Law2/Functors                 | 0m05.05s
0m04.64s | categories/DualFunctor                                   | 0m05.46s
0m04.59s | categories/Category/Sigma/OnMorphisms                    | 0m04.16s
0m03.60s | categories/ProductLaws                                   | 0m03.66s
0m03.51s | types/ObjectClassifier                                   | 0m03.50s
0m03.28s | categories/Grothendieck/ToSet                            | 0m02.51s
0m03.11s | categories/Functor/Prod/Functorial                       | 0m02.88s
0m03.01s | types/Sigma                                              | 0m03.07s
0m02.78s | categories/Adjoint/UniversalMorphisms                    | 0m02.79s
0m02.62s | categories/FunctorCategory/Functorial                    | 0m02.70s
0m02.58s | Equivalences                                             | 0m02.62s
0m02.34s | categories/Functor/Attributes                            | 0m02.27s
0m02.19s | categories/Category/Sum                                  | 0m02.24s
0m02.10s | categories/Comma/Core                                    | 0m02.08s
0m02.06s | categories/Category/Sigma/Core                           | 0m02.04s
0m01.93s | categories/NaturalTransformation/Dual                    | 0m01.96s
0m01.89s | PathGroupoids                                            | 0m02.01s
0m01.84s | categories/HomFunctor                                    | 0m01.85s
0m01.79s | categories/NaturalTransformation/Isomorphisms            | 0m01.79s
0m01.67s | categories/NaturalTransformation/Paths                   | 0m01.60s
0m01.64s | categories/FunctorCategory/Morphisms                     | 0m01.71s
0m01.33s | categories/Category/Prod                                 | 0m01.31s
0m01.32s | categories/Category/Sigma/OnObjects                      | 0m01.34s
0m01.26s | categories/NaturalTransformation/Pointwise               | 0m01.31s
0m01.26s | types/Prod                                               | 0m01.30s
0m01.22s | categories/NaturalTransformation/Composition/Laws        | 0m01.25s
0m01.10s | categories/Limits/Core                                   | 0m01.23s
0m01.09s | categories/Functor/Pointwise                             | 0m01.05s
0m01.05s | categories/CategoryOfSections/Core                       | 0m01.05s
0m01.00s | categories/NaturalTransformation/Prod                    | 0m00.92s
0m00.98s | categories/ExponentialLaws/Law  N/A                      | 0m01.04s
0m00.96s | categories/ExponentialLaws/Law1/Functors                 | 0m00.98s
0m00.93s | hit/epi                                                  | 0m00.94s
0m00.93s | hit/Spheres                                              | 0m01.10s
0m00.92s | categories/Functor/Prod                                  | 0m00.95s
0m00.88s | categories/Functor/Composition/Functorial                | 0m00.84s
0m00.82s | types/Paths                                              | 0m00.79s
0m00.79s | Trunc                                                    | 0m00.84s
0m00.74s | categories/InitialTerminalCategory                       | 0m00.62s
0m00.68s | types/Universe                                           | 0m00.64s
0m00.66s | categories/NaturalTransformation/Composition/Core        | 0m00.64s
0m00.63s | types/Sum                                                | 0m00.59s
0m00.56s | hit/Circle                                               | 0m00.53s
0m00.56s | categories/Comma/Projection                              | 0m00.60s
0m00.54s | Functorish                                               | 0m00.62s
0m00.53s | categories/NaturalTransformation/Sum                     | 0m00.55s
0m00.53s | categories/Functor/Composition/Laws                      | 0m00.51s
0m00.52s | categories/categories                                    | 0m00.53s
0m00.52s | hit/quotient                                             | 0m00.54s
0m00.50s | hit/Suspension                                           | 0m00.53s
0m00.50s | types/Record                                             | 0m00.49s
0m00.45s | categories/Limits/Functors                               | 0m00.46s
0m00.44s | categories/KanExtensions/Functors                        | 0m00.41s
0m00.43s | HSet                                                     | 0m00.41s
0m00.43s | Tactics                                                  | 0m00.41s
0m00.43s | types/Forall                                             | 0m00.44s
0m00.41s | HProp                                                    | 0m00.44s
0m00.40s | categories/ExponentialLaws/Law3/Functors                 | 0m00.41s
0m00.39s | Fibrations                                               | 0m00.33s
0m00.38s | categories/Functor/Functor                               | 0m00.36s
0m00.37s | categories/Cat/Core                                      | 0m00.39s
0m00.36s | categories/NaturalTransformation/Identity                | 0m00.41s
0m00.33s | categories/IndiscreteCategory                            | 0m00.35s
0m00.32s | TruncType                                                | 0m00.39s
0m00.31s | categories/KanExtensions/Core                            | 0m00.26s
0m00.30s | categories/Functor/Dual                                  | 0m00.31s
0m00.29s | Misc                                                     | 0m00.28s
0m00.29s | categories/Cat/Morphisms                                 | 0m00.27s
0m00.28s | hit/minus1Trunc                                          | 0m00.36s
0m00.27s | categories/NaturalTransformation/Composition/Functorial  | 0m00.32s
0m00.26s | types/Arrow                                              | 0m00.27s
0m00.26s | categories/Grothendieck/Grothendieck                     | 0m00.22s
0m00.24s | categories/ExponentialLaws/ExponentialLaws               | 0m00.26s
0m00.24s | categories/Category/Objects                              | 0m00.23s
0m00.24s | categories/Notations                                     | 0m00.22s
0m00.22s | categories/NaturalTransformation/NaturalTransformation   | 0m00.20s
0m00.22s | categories/SetCategory/Functors/Functors                 | 0m00.24s
0m00.22s | categories/Functor/Composition/Core                      | 0m00.24s
0m00.22s | categories/Adjoint/Adjoint                               | 0m00.23s
0m00.21s | categories/Grothendieck/ToCat                            | 0m00.20s
0m00.20s | categories/Functor/Prod/Prod                             | 0m00.20s
0m00.20s | categories/Comma/Comma                                   | 0m00.18s
0m00.20s | categories/Utf8                                          | 0m00.22s
0m00.20s | categories/Pseudofunctor/Pseudofunctor                   | 0m00.17s
0m00.20s | categories/NaturalTransformation/Notations               | 0m00.16s
0m00.19s | categories/DependentProduct                              | 0m00.20s
0m00.19s | hit/iso                                                  | 0m00.20s
0m00.19s | categories/Category/Core                                 | 0m00.16s
0m00.19s | FunextVarieties                                          | 0m00.17s
0m00.18s | categories/FunctorCategory/FunctorCategory               | 0m00.21s
0m00.18s | categories/Profunctor/Representable                      | 0m00.16s
0m00.18s | categories/ExponentialLaws/Law1/Law1                     | 0m00.14s
0m00.17s | Conjugation                                              | 0m00.18s
0m00.17s | contrib/HoTTBook                                         | 0m00.16s
0m00.17s | categories/Category/Category                             | 0m00.16s
0m00.17s | categories/NatCategory                                   | 0m00.20s
0m00.17s | categories/ExponentialLaws/Law2/Law2                     | 0m00.16s
0m00.17s | categories/FunctorCategory/Core                          | 0m00.21s
0m00.16s | categories/Limits/Limits                                 | 0m00.16s
0m00.16s | HoTT                                                     | 0m00.15s
0m00.16s | categories/GroupoidCategory/Core                         | 0m00.18s
0m00.16s | categories/Adjoint/Composition/Composition               | 0m00.16s
0m00.15s | categories/Adjoint/Utf8                                  | 0m00.16s
0m00.15s | categories/KanExtensions/KanExtensions                   | 0m00.15s
0m00.15s | categories/SetCategory/Core                              | 0m00.12s
0m00.15s | categories/Category/Dual                                 | 0m00.16s
0m00.15s | categories/Adjoint/Identity                              | 0m00.13s
0m00.15s | hit/unique_choice                                        | 0m00.14s
0m00.15s | categories/Functor/Notations                             | 0m00.13s
0m00.15s | categories/Adjoint/Notations                             | 0m00.13s
0m00.15s | categories/Comma/Notations                               | 0m00.15s
0m00.15s | Overture                                                 | 0m00.14s
0m00.14s | categories/Comma/Utf8                                    | 0m00.16s
0m00.14s | categories/ExponentialLaws/Law3/Law3                     | 0m00.16s
0m00.14s | categories/Cat/Cat                                       | 0m00.16s
0m00.14s | categories/FunctorCategory/Utf8                          | 0m00.17s
0m00.14s | categories/Functor/Utf8                                  | 0m00.12s
0m00.14s | categories/Functor/Composition/Composition               | 0m00.11s
0m00.14s | categories/NaturalTransformation/Utf8                    | 0m00.16s
0m00.13s | categories/Adjoint/Core                                  | 0m00.13s
0m00.13s | categories/Profunctor/Notations                          | 0m00.12s
0m00.13s | categories/Profunctor/Identity                           | 0m00.12s
0m00.13s | categories/Functor/Pointwise/Pointwise                   | 0m00.10s
0m00.13s | categories/Adjoint/Composition/LawsTactic                | 0m00.14s
0m00.13s | categories/Profunctor/Utf8                               | 0m00.11s
0m00.12s | categories/Profunctor/Core                               | 0m00.09s
0m00.12s | categories/ExponentialLaws/Law4/Law4                     | 0m00.10s
0m00.12s | categories/Category/Univalent                            | 0m00.12s
0m00.12s | categories/Profunctor/Profunctor                         | 0m00.12s
0m00.12s | categories/NaturalTransformation/Core                    | 0m00.15s
0m00.12s | categories/Category/Subcategory/Subcategory              | 0m00.13s
0m00.12s | types/Unit                                               | 0m00.14s
0m00.12s | categories/Category/Sigma/Sigma                          | 0m00.12s
0m00.12s | hit/Truncations                                          | 0m00.14s
0m00.11s | categories/DiscreteCategory                              | 0m00.10s
0m00.11s | categories/GroupoidCategory/GroupoidCategory             | 0m00.08s
0m00.11s | hit/Interval                                             | 0m00.16s
0m00.11s | coq/Init/Peano                                           | 0m00.12s
0m00.11s | types/Bool                                               | 0m00.12s
0m00.11s | categories/SetCategory/SetCategory                       | 0m00.13s
0m00.11s | categories/NaturalTransformation/Composition/Composition | 0m00.11s
0m00.11s | categories/FunctorCategory/Notations                     | 0m00.12s
0m00.10s | categories/Category/Utf8                                 | 0m00.11s
0m00.10s | categories/Functor/Identity                              | 0m00.07s
0m00.10s | Contractible                                             | 0m00.11s
0m00.10s | categories/Category/Notations                            | 0m00.12s
0m00.10s | UnivalenceAxiom                                          | 0m00.10s
0m00.10s | categories/Category/Subcategory/Full                     | 0m00.11s
0m00.10s | categories/CategoryOfSections/CategoryOfSections         | 0m00.13s
0m00.09s | categories/Functor/Core                                  | 0m00.10s
0m00.09s | categories/Category/Subcategory/Wide                     | 0m00.13s
0m00.09s | contrib/HoTTBookExercises                                | 0m00.14s
0m00.08s | coq/Init/Specif                                          | 0m00.07s
0m00.08s | Pointed                                                  | 0m00.08s
0m00.07s | coq/Init/Datatypes                                       | 0m00.06s
0m00.07s | categories/Category/Strict                               | 0m00.07s
0m00.07s | types/Empty                                              | 0m00.08s
0m00.06s | coq/Init/Prelude                                         | 0m00.02s
0m00.06s | coq/Init/Logic_Type                                      | 0m00.06s
0m00.06s | FunextAxiom                                              | 0m00.08s
0m00.05s | coq/Init/Notations                                       | 0m00.03s
0m00.04s | coq/Init/Logic                                           | 0m00.02s
0m00.04s | coq/Bool/Bool                                            | 0m00.03s
0m00.04s | coq/Program/Tactics                                      | 0m00.07s
0m00.03s | coq/Init/Tactics                                         | 0m00.02s
Add some spaces to try to get coqdoc working

The preformatted output looks wrong.
Change case on pseduofunctor section name

Now the tags/links in the html files point to the right places.
Try even more spaces to get coqdoc working
Even more spaces for coqdoc?

I'm not sure what's going wrong
Fix missing coqdoc character

It was a missing ']', and not spaces, after all.