Better struture for Ltac internalization environments in Constrintern.
Fixing #3483 (graceful failing with notations to non-constructors in "match").
Chapter 4: Fixing ambiguity about whether the return predicate refers
explicitly or implicitly to the variables in the as and in clauses +
formatting.
- Fix has_undefined_evars not using its or_sorts argument anymore.
- Allow apply's unification to use conversion even if some polymorphic
constants appear in the goal (consistent with occur_meta_or_evar, and
evarconv in general).
Move to a representation of universe polymorphic constants using indices for variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
- Fix handling of opaque polymorphic definitions which were turned transparent.
- Decomment code in reductionops forgotten after debugging.
Fix infer conv using the wrong universe conversion flexibility information
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
Fix to make Coq compile, I think this should still be accepted.
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.
Fix an exponential behavior in guard checker for cofixpoints.

I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
More optimization in guard checking.

When dynamically computing the recarg tree, we now prune it according to the
inferred tree. Compilation of CompCert is now ok.
One more optimization for guard checking of cofixpoints.

In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.