Use pr1/2 rather than projT1/2
Use pr1/2 rather than proj1/2_sig
Merge pull request #439 from andrejbauer/master

Fix /etc/install_coq.sh for OSX, merging because this is a technicality.
Merge pull request #437 from mikeshulman/pr

Use pr1/2 rather than projT1/2
make contrib/.dir-locals.el the same as the other .dir-locals.el's.
Merge pull request #441 from mikeshulman/dirlocals

make contrib/.dir-locals.el the same as the other .dir-locals.el's.
Add a [transparent assert] tactic

I hope we'll one day have an OCaml version in the stdlib, because this
one has some infelicities
(https://coq.inria.fr/bugs/show_bug.cgi?id=3551).  I think we need an
OCaml version to do [transparent assert (foo : nat = nat)] rather
than [transparent assert (foo : (nat = nat))], and so that we can have
both [transparent assert (foo : bar)] and just [transparent assert
(bar)].  Currently, you must name all the hypotheses that you
[transparent assert].
¹ is now a symbol

Fix in response to the fix to https://coq.inria.fr/bugs/show_bug.cgi?id=3541
More replacement of [projT] with [pr]

The instances of [proj1_sig] in Category/Sigma are intentional and
semantically meaningful (they are about subsets/sigT with an hProp).
Merge pull request #443 from JasonGross/remove-more-projT

More replacement of [projT] with [pr]
Merge pull request #442 from JasonGross/transparent-assert

Add a [transparent assert] tactic
Solution to Exercise 3.1 and two preparing lemmas added.
Merge pull request #445 from marcbezem/master

Solution to Exercise 3.1 and two preparing lemmas added.
Move some [Require]s to the top of a file

It's bad practice to have them in the middle of the file.  Also, it
makes my coq-bug-finder run afoul of
https://coq.inria.fr/bugs/show_bug.cgi?id=3556 when tracking down a bug
in [apply] in the new version of trunk with #440.
Strip out a duplicate [Require Import]
Don't match on pairs where we don't need to

It's slightly better style, I think, to do it this way.  Also, when we
move to primitive projections, this code will break (see
https://coq.inria.fr/bugs/show_bug.cgi?id=3558).
Merge pull request #446 from JasonGross/no-match-pair

Don't match on pairs where we don't need to
Formalize the cumulative hierarchy V (most of §10.5 of the book)
Change the style of the comments
Move the dependent composition to Overture.v