Export algebraic universes.
Fix the multi-line comment style. This is the style used in the Coq code base.
Use similar comments for different term constructs.