- Fixes for canonical structure resolution (check that the initial term indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
Fix program Fixpoint not taking care of universes.
- Fix RecTutorial, and mutual induction schemes getting the wrong names.
Now the universe inconsistency appears at [exact t] instead of the Defined :)
Allow records whose sort is defined by a constant.
Fix declarations of monomorphic assumptions
Fix restrict_universe_context removing some universes that do appear in the term.
- Fix arity handling in retyping (de Bruijn bug!)
- Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints.
(Needs to be enforced in the kernel as well, but that's the main entry point).
- Fix a test-suite script and remove a regression comment, it's just as before now.