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.