Cleaning of the new implementation of the tactic monad.

* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v
Cleaning the new implementation of the tactic monad continued.

Remove proofview_gen, which was the repository of the extracted code, and move it to proofview_monad, which has the actual interface used by the [Proofview] module to implement tactics.
Some comments in the interface of Proofview_monad.
STM: VtQuery holds the id of the state it refers to
STM: encapsulate Pp.message in Feedback.feedback
STM: use a real priority queue
STM: generate Feedback message for parsing errors
STM: when looking up in the cache catch Expired exc
Fixing semantics of Univ.Level.equal.