Retype application of fix_proto to get the right universes in Program
Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.
Correct universe handling in program coercions (bug #2378).
Refresh some universes in cases.ml as they might appear in the term.
Proper calculation of constructor levels, forgetting the level of lets.
Comment in Funind.v test-suite file