Reuse universe level substitutions for template polymorphism, fixing performance
problem with hashconsing at the same time. This fixes bug# 3302.
Restore implicit arguments of irreflexivity (fixes bug #3305).
Fix second-order matching to properly check that the predicate found by
abstraction has the right type. Fixes bug# 3306.
Add test-suite files for bugs 3305 and 3306.
Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq into JasonGross-working-polyproj-tests
Refresh universes for Ltac's type_of, as the term can be used anywhere,
fixing two opened bugs from HoTT/coq.
More documentation of new features in CHANGE.
Update and start testing rewrite-in-type code.
Code cleaning & factorizing functions in Equality.
Add more regression tests for univ poly/prim proj

hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.

These are the tests that trunk currently fails.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.
Move opened bugs to bugs/opened
Add appropriate Fail(s) to opened bugs

The contract is that a file in bugs/opened should not raise errors if
the bug is still open.

Some of them fail for different reasons than they used to; I'm not sure
what to do about these.
Eliminating a potentially quadratic behaviour in Require, by using maps
instead of lists to test if a library has already been encountered.
Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,
and the lookup operation proved to be costly when dealing with big libraries.
Fixing the undocumented -dumpgraphbox option of coqdep.
Adding the possibility for ML modules to declare functions to be called at
caching time, i.e. when the Declare ML Module command is evaluated. This can
be used by both static and dynamic plugins.
Plugin names must be declared in the header of .ml4 file, be they static or
dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro.
Moving the ML tactic extension mechanism to a Libobject-based one.
Now parsing rules of ML-declared tactics are only made available after the
corresponding Declare ML Module command. This changes essentially two
things:

1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.

2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.
Update various polyproj bugs w.r.t. latest trunk
Rewritten the sorting algorithm for universes with a better complexity.
This should be now linear instead of the cubic Bellman-Ford algorithm.
The new algorithm assumes that the universe graph is a DAG if we remove
the {Le, Eq}-cycles, which is the case when the graph is consistent.
Luckily we only use the sorting algorithm on such consistent graphs,
in the Print Sorted Universes command.