Stm: remove an assertion.

In the code which indents proof scripts, you cannot assume that a single goal is closed at a time (because of dependent subgoals).

This change had been lost in the rebase over the paral-itp commits in october.
Documentation of the Derive plugin.

I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.