1. coercGraph.ml* moved from library to cic_unification (where it should
have been put in the first place). A few functions that must remain in
library moved to coercDb.ml* (where they should have been put in the first
place)
2. ProofEngineHelpers.saturate_term moved from tactic to cic_unification.
3. Bug fixed in saturate_term: the newmeta returned by the function was not
correct in some cases
4. CoercGraph.look_for_coercion* used to saturate the coercion with implicit
arguments (thus requirin a refinement pass later on). Now the same
functions saturate the term with metas. The return type has changed
accordingly.
5. the horrible hack to break composite coercions during unification has been
replaced by a nice implementation of unification towards the join of the
two coercions (called meet by Enrico I do not know why :-).
This solves many many problems found using multiple coercion pathes from
a source to a destination. (This is the case in DAMA that I am going to
commit soon).