Small tactic improvement

[SimonGuilloud]

Implements a few improvements:

• Pretty printing of formula in theorems and errors changed to correspond to high level printing instead of relying on the parser/printer. In particular, makes it possible to copy-paste formulas that a part of the output directly into a working document.
• Fix and improve issues with extractor paterns. In particular, can now do such thing as:

  formula match
  case x === y => ???
  case P(x, y) => ???
  ...

• Change the behaviour of TacticSubproof to permit tactics to return InvalidProofTactics from inside it, i.e. when it is discovered that the Tactic can't succeed during proof generation. This prevented to have tactics whose success where depending from the success of other tactics (or recursive calls) without throwing and catching exceptions or modifying non-local variables. "Returning" was not possible either because the content inside TacticSubproof {} was technically an anonymous functions, and non-local returns are not supported anymore. Some inlining of functions solved this issue.

[SimonGuilloud]

To merge after #181 and #183.

[SimonGuilloud]

I fixed the build settings. "organization" was actually apparently incorectly used here, and "-Ximport-suggestion-timeout" was also apparently incorrect (it was to prevent the "generate" suggestions on implicit). At some point it would be awsome if someone a bit expert can chack our build.sbt file, I'm really not too sure we're doing it right.