Tacinterp: fewer use of old-style goals.

There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics.

I've changed some of them to explicitely take an environment and an evar_map instead.
Factoring: is_section_variable.

In 0c7a77, I inadvertantly re-defined an is_section_variable function.
Remove the Hiddentac module.

Since the new proof engine, Hiddentac has been essentially trivial.
Here is what happened to the functions defined there
- Aliases, or tactics that were trivial to inline were systematically inlined
- Tactics used only in tacinterp have been moved to tacinterp
- Other tactics have been moved to a new module Tactics.Simple.