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.