[ new ] Interactive tactic development.
  Unsolved metas are now allowed inside an `unquote ...'.