Make sig/sigT a primitive record

We have less funext in sigma.v, and the issig tactics are significantly simpler (to the point of having practically no ltac at all).  There's not much speedup here, but we don't use nested sigmas much.

Next up, categories, functors, natural transformations, and adjunctions.

Our proofs about sigma types now use less functional extensionality.

Arnaud said that he'd fix [bug 3583](https://coq.inria.fr/bugs/show_bug.cgi?id=3583) on Monday, so we probably want to wait until then to actually merge this.  The work-arounds for 3587 and 2588 are very simple, and it's likely that if/when the crop up elsewhere, people will just chalk it up to peculiarities of `apply` or `rewrite`.  So I'd prefer not to wait for those two to be fixed to merge this.

Since the work-arounds for the bugs are all extremely trivial, I'd like to open this up to feedback now