Adds a shelve tactic.

The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command.
Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used at the wrong time.

The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic
Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t))
had the correct semantics!
Make multiple-goal tactics possible after a tclTHEN.

Tacinterp used to interprete every tactics inside a goal, making
multiple-goal tactics act on a single goal anyway.

Uses a simple heuristic to decide when a goal is not needed.
Made multiple-goal tactic work after all: .

Internalization was done relative to a goal. It doesn't make sense in the
case of all:. When we make a tactic with all: the environment for
internalization is taken to be the global environment.
A tactic shelve_unifiable.

Puts on the shelf every goals under focus on which other goals under focus
depend. Useful when we want to solve these goals by unification (as in a
first order proof search procedure, for instance).

Also meant to be able to recover approximately the semantics of the old
refine with the new implementation (use refine t; shelve_unifiable).

TODO: bug dans l'example de shelve_unifiable