Add a .travis.yml file for continuous integration
Add a build-status logo

Perhaps we should test on multiple versions of OCaml, a la
http://anil.recoil.org/2013/09/30/travis-and-ocaml.html
Exact pattern-matching up to standard equivalence
Also, slightly better debugging output
Prove sigma_eta and sigma_eta' (renamed to id_sigma)

Renamed sigma_eta' because it's classifying the strict identity type
of sigmas.

Unfortunately, sigma_eta is rather slow; on my machine:
$ time ./brazil.native examples/sigma.br
...
real    0m14.380s
user    0m14.281s
sys     0m0.047s
Add sigma.br to the brazil smoketest
Equivalence alg uses rewrites on recursing
Also more debugging print output
Also a #verbose directive
Record types (forgot projections)
Working on records, added projections
Record types almost implemented, at least compile
Merge pull request #24 from JasonGross/travis

Travis
Merge pull request #25 from JasonGross/more-sigma

Prove sigma_eta and sigma_eta' (renamed to id_sigma)
Temporarily disable `sigma.br` in smoke test

Also add `record.br` to smoke test.
Example of how to use records.
Bug fixes for record types.
Change travis target to `all`
Towards propositional truncation.

This version exposes a bug with records.
Allow numerals in projections.
Coq-style printing of products.
Bug in synthesizing the type of a projection.
Example: propositional truncation and interval.

It’s kind of surprising that once the computation rules for truncation
and booleans are installed as rewrites we don’t need any equality hints
or new rewrite hints.