Adding generic solvers to term holes. For now, no resolution mechanism nor
parsing is plugged.
Adding the necessary hooks to handle tactics in terms.
Actually adding the grammar entry to handle tactics in terms.
Fixing abstract tactic by using a dummy name out of a declared proof.
Getting rid of goal-dependency in declarative mode argument evaluation.
Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)