Tactic primitives: missing [advance] lead to spurious dangling goals.

Closes #3801.
Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.

When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.

Fixes test-suite/success/apply.v