Fix grammar

As per
http://www.quickanddirtytips.com/education/grammar/which-versus?page=all
Use AS_IF rather than 'if', uniformize more things
Check for usr/bin/time in configure
./autogen.sh
Autobuild documentation with travis

Now that we have a `make html` target, we can make the html
automatically on travis.  If travis builds something which is the same
as origin's master, then we autocommit updated documentation and push to
the gh-pages branch, where documentation is accessible at
http://hott.github.io/HoTT/coqdoc-html/.

Generating the files was a pain.  I record the process here, so that if
we need to update the keys, there will be a reference.

First, generate the keys that will be used
```bash
$ ROOT="$(git rev-parse --show-toplevel)"
$ ssh-keygen -t rsa -C "Travis-CI-bot@travis.fake" -f "$(readlink -f "$ROOT"/etc/ci/id_rsa)"
```
When it prompts you for a passphrase, you must leave it blank.

Then add the contents of "$ROOT"/etc/ci/id_rsa.pub as a deploy key to
the HoTT repository at https://github.com/HoTT/HoTT/settings/keys.

Now, following a modified version of
http://about.travis-ci.org/docs/user/travis-pro/#How-can-I-encrypt-files-that-include-sensitive-data%3F,
encrypt the id_rsa file:
```bash
$ password=`cat /dev/urandom | head -c 10000 | openssl sha1`
$ openssl aes-256-cbc -k "$password" -in "$ROOT"/etc/ci/id_rsa -out "$ROOT"/etc/ci/id_rsa.enc -a
```
Now, the hard part (at least if you don't have sudo). Hope that you
either have ruby and gem installed, or a version of ssh-keygen which
supports the `-e -m` flag combination (check with `ssh-keygen -\?`).  If
you have ruby and gem, then you can follow
http://about.travis-ci.org/docs/user/encryption-keys/, and run
```bash
$ gem install travis
$ travis encrypt -r HoTT/HoTT "SSHKEY_PASSWORD=$password"
```
and update the `secure:` part of the `.travis.yml` file with the resulting
secret.  Otherwise, you can follow
http://about.travis-ci.org/docs/user/travis-pro/#How-can-I-encrypt-files-that-include-sensitive-data%3F
and run
```bash
$ \curl https://api.travis-ci.org/repos/HoTT/HoTT/key | perl -pe 's/^{"key"://; s/^"//; s/"}$//' | sed s'/\\n/\n/g' > id_travis.pub
$ ssh-keygen -e -m PKCS8 -f id_travis.pub > id_travis.pub.pem
$ echo "SSHKEY_PASSWORD='$password'" | openssl rsautl -encrypt -pubin -inkey id_travis.pub.pem
```
However, if `ssh-keygen` fails, complaining about `-m` being
unrecognized, then you must clone or copy
https://gist.github.com/thwarted/1024558
(https://gist.github.com/1024558.git), install the required python
dependencies (for me, pyasn1), and then run that on `id_travis.pub` to
get the `id_travis.pub.pem` file, and then run the `openssl rsautl`
commmand.  Either way, the output of that third command should be placed
in the `.travis.yml` file, replacing the existing secret.

Perhaps we should include these instructions somewhere in the
repository?
Use OAuth instead of ssh to autogen doc on travis

This is a much simpler way of doing things.

Now that we have a `make html` target, we can make the html
automatically on travis.  If travis builds something which is the same
as origin's master, then we autocommit updated documentation and push to
the gh-pages branch, where documentation is accessible at
http://hott.github.io/HoTT/coqdoc-html/.

Generating the files was much less of a pain.  I record the process
here, so that if we need to update the keys, there will be a reference.

First, generate the OAuth token that will be used, replacing
'<username>' with your username.  You must have permission to push to
HoTT/HoTT.
```bash
$ TOKEN="$(curl -u '<username>' -d '{"scopes":["repo"],"note":"For Travis-CI Bot"}' https://api.github.com/authorizations | grep -o 'token": "[^"]*' | sed s'/token": "//g')"
```
It will prompt you for your password.

Now, the hard part (at least if you don't have sudo). Hope that you
either have ruby and gem installed, or a version of ssh-keygen which
supports the `-e -m` flag combination (check with `ssh-keygen -\?`).  If
you have ruby and gem, then you can follow
http://about.travis-ci.org/docs/user/encryption-keys/, and run
```bash
$ gem install travis
$ travis encrypt -r HoTT/HoTT "OAUTH_TOKEN=$TOKEN"
```
and update the `secure:` part of the `.travis.yml` file with the resulting
secret.  Otherwise, you can follow
http://about.travis-ci.org/docs/user/travis-pro/#How-can-I-encrypt-files-that-include-sensitive-data%3F
and run
```bash
$ \curl https://api.travis-ci.org/repos/HoTT/HoTT/key | perl -pe 's/^{"key"://; s/^"//; s/"}$//' | sed s'/\\n/\n/g' > id_travis.pub
$ ssh-keygen -e -m PKCS8 -f id_travis.pub > id_travis.pub.pem
$ echo "OAUTH_TOKEN=$TOKEN" | openssl rsautl -encrypt -pubin -inkey id_travis.pub.pem
```
However, if `ssh-keygen` fails, complaining about `-m` being
unrecognized, then you must clone or copy
https://gist.github.com/thwarted/1024558
(https://gist.github.com/1024558.git), install the required python
dependencies (for me, pyasn1), and then run that on `id_travis.pub` to
get the `id_travis.pub.pem` file, and then run the `openssl rsautl`
commmand.  Either way, the output of that third command should be placed
in the `.travis.yml` file, replacing the existing secret.

Perhaps we should include these instructions somewhere in the
repository?
Auto-push autoreconf stuff

Now travis will run autoreconf -fvi for us, and push it to
master-with-autoreconf-files.
Also build without autoreconf

We don't want the build to fail on a machine without autoreconf.
Update autogen.sh to get files from git

But only if we don't have autoreconf.
Update INSTALL.txt to mention autogen.sh
Update CREDITS.txt
Merge pull request #198 from JasonGross/autogen-without-autogoo

Autogen without autogoo.
With Dan's blessing, I dare to push the button.
Don't push if autoreconf fails

Also, don't have travis build the master-with-autoreconf-files branch.
Merge pull request #199 from andrejbauer/master

Update CREDITS.txt
Get rid of temporary file usage.

Hopefully I got the quoting right.
Silence travis on push

This fixes https://github.com/HoTT/HoTT/pull/199#issuecomment-23296261
Removing admits, one left due to universe inconsistency.
No axioms left (apart from Funext).

More documentation on the use of canonical structures.
Moving between records and sigmas should now be easier.
However, I am not sure whether this is the most optimal way of expressing this.
There is still quite a bit of boiler plate code.
Removing one last admit.
Remove use of funext-axiom