Improve presentation of old issig tactics

I found a way to build issig tactics which are two orders of magnitude
faster than the very old ones (which did not adjointify), but which keep
all do not adjust the sections and retractions.  The key is to apply
symmetry, so that we destruct a record rather than a sigma type.
However, the adjointifying versions are still an order of magnitude or
two faster than these versions, so we use the adjointifying ones by
default.