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.