ConstructiveEpsilon: simplify the before_witness type using non-uniform parameters.
Proofview: small optimisation/simplification.
Proofview.Refine: delay the marking of new evars as goals from [new_evar] to [refine].

This makes [new_evar] closer to be a mere wrapper around [Evarutil.new_evars]. Will allow restructuring of the refinement interface.
Evd: remove/update obsolete comments.
Evd: a few comments to document the increasingly wide internal [evar_map] type.
Move the handling a new evars from the [Proofview.Refine] module to [Evd].

That way, everything in the code of pretying is made "refine"-aware. Making the abstraction stonger and integration of pretyping with interactive proof more direct.

It might create goals in a slightly different goal order in the (user level) refine tactic. Because now, the [update] primitive which used to infer an order from an [evar_map] now has the order fixed by the successive declaration with [Evarutil.new_evar] (and similar). It probably coincides, though.

Following a suggestion by Hugo.
Move the handling of the principal evar from refine to evd.

See previous commit for more discussion.

Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway.
Proofview.Refine: remove the handle type, and simplify the API.

Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine.

The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.
Expose Proofview.Refine.with_type in the API.
Goal: remove dead code.
Make [Goal.goal] be exactly [Evar.t].

First step in removing the [Goal] module whose code is now essentially legacy.

Removes the cache attached to a goal, which was used to avoid unnecessary [nf_evar]. May have a performance cost, which is to be fixed later.
Goal: remove most of the API (make [Goal.goal] concrete).

We are left with the compatibility layer and a handful of primitives which require some thought to move.
Goal: remove some functions from the compatibility layer.

The rest will take more work.
Proofview: remove unused [refresh_sigma] compatibility primitive.
Goal: remove [advance] from the API.

Now [Goal] only contains a few helpers.
Refine: proper scoping of the future goals.

In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use.
Put evars remaining after a tactic on the shelf.

Uses the new architecture which allows to keep track of all new evars. The [future_goals] are flushed at the end of the tactics, the [principal_future_goal] is ignored.
Proofview: cleanup: no more reference to Goal.goal.
Grab Existential Variables: restore the goal order from v8.4.

Changes in the implementation details had unwittingly changed the order in which Grab Existential Variables displayed the goals.
Bug fixed by Hugo.