Work around bug 3583

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3583, "Error: Ltac
variable x is not bound to an identifier. It cannot be used in a
binder." should not trigger when the binder is shared with one in the
pattern match
Add sig as a primitive record
Work around bug 3584

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3584, pattern matching
should be desugared to primitive projection usage (Error:
Pattern-matching expression on an object of inductive type sigT has
invalid information.).  The workaround requires judgmental eta.
Work around bug 3584 in sigma.v

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3584, pattern matching
should be desugared to primitive projection usage (Error:
Pattern-matching expression on an object of inductive type sigT has
invalid information.).  But these are changes we'll want to make to
sigma.v, anyway.
Work around bug 3584 in record.v

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3584, pattern matching
should be desugared to primitive projection usage (Error:
Pattern-matching expression on an object of inductive type sigT has
invalid information.).  But these are changes we'll want to make to
record.v, anyway.
Work around an as-yet-unspecified bug in theories/hit/Connectedness.v
Work around an as-yet-unspecified bug in theories/categories/ExponentialLaws/Law1/Law.v