Refactoring proofview: make the definition of the logic monad polymorphic.

Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad.

The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer.