This commit adds full universe polymorphism and fast projections to Coq.

Add [Polymorphic] and [Monomorphic] local flag for definitions as well as
[Set Universe Polymorphism] global flag to make all following definitions
polymorphic. Mainly syntax for now.

First part of the big changes to the kernel:
- Const, Ind, Construct now come with a universe level instance
- It is used for type inference in the kernel, which now also takes
a graph as input: actually a set of local universe variables and their
constraints. Type inference just checks that the constraints are enough
to satisfy its own rules.
- Remove polymorphic_arity and _knowing_parameters everywhere: we
don't need full applications for polymorphism to apply anymore, as
we generate fresh variables at each constant/inductive/constructor
application. However knowing_parameters variants might be reinstated
later for optimization.
- New structures exported in univ.mli:
  - universe_list for universe level instances
  - universe_context(_set) for the local universe constraints, also
recording which variables will be local and hence generalized after
inference if defining a polymorphic ind/constant.
- this patch makes coq stop compiling at indtypes.ml

Adapt kernel, library, pretyping, tactics and toplevel to universe polymorphism.
Various degrees of integration, places where I was not sure what to do or
just postponed bigger reorganizations of the code are marked with FIXMEs.
Main changes:
- Kernel now checks constraints and does not infer them anymore.
- The inference functions produce a context of constraints that were checked
during inference, useful to do double-checking of the univ. poly. code
but might be removed later.
- Constant, Inductive entries now have a universe context (local variables
and constraints) associated to them.
- Printing, debugging functions for the new structures are also implemented.
- Now stopping at Logic.v
- Lots of new code in kernel/univ.ml that should be reviewed.
- kernel/indtypes probably does not do what's right when inferring inductive
type constraints.
- Adapted evd to use the new universe context structure.
- Did not deal with unification/evar_conv.

- Add externalisation code for universe level instances.
- Support for polymorphism in pretyping/command and proofs/proofview etc.
  Needed wrapping of [fresh_.._instance] through the evar_map, which
  contains the local state of universes during type-checking.
- Correct the inductive scheme generation to support polymorphism as well.
- Have to review kernel code for correctness, and especially rework the
  computation of universe constraints for inductives.
Stops somewhat later in Logic.v

- Fix naming of local/toplevel universes to be correctly done at typechecking time:
  local variables have no dirpath.
- Add code to do substitution of universes in modules, not finished yet.
- Move fresh_* functions out of kernel, it won't ever build a universe level again!
- Adapt a lot of new_Type to use the correct dirpath and declare the new types in the evar_map
so we keep track of them.
- A bit of code factorization (evd_comb moved, pretype_global).

- Refactor more code
- Adapt plugins code (sometimes wrong, marked with FIXME)
- Fix cases generating unneeded universe (not sure it's ok though)
- Fix scheme generation for good, might have opportunity to cleanup
the terms later.

Init compiles now (which means rewrite, inversion, elim etc.. work as well).
- Unsolved issue of pretyping to lower sorts properly (to Prop for example).
  This has to do with the (Retyping.get_type_of) giving algebraic universes that
  would appear on the right of constraints.
  This makes checking for dangling universes at the end of pretyping fail,
  hence the check in kernel/univ was removed. It should come back when we have
  a fix for this.
- Correctly (?) compute the levels of inductive types.
  Removed old code pertaining to universe polymorphism. Note that we generate
  constraint variables for the conclusion of inductive types invariably.
- Shrink constraints before going to the kernel, combine substitution of the
  smaller universe set with normalization of evars (maybe not done everywhere,
  only ordinary inductives, definitions and proofs)
- More API reworks overall. tclPUSHCONTEXT can be used to add fresh universes
  to the proof goal (used in a few places to get the right instance.
- Quick fix for auto that won't work in the long run. It should always have been
  restricted to take constant references as input, without any loss of generality
  over constrs.

Fix some plugins and insertion of non-polymorphic constants in a module.
Now stops in relation classes.

Cleanup and move code from kernel to library and from pretyping to library too.
Now there is a unique universe counter declared in library/universes.ml along
with all the functions to generate new universes and get fresh constant/inductive
terms.
- Various function renamings
- One important change in kernel/univ.ml: now [sup] can be applied to Prop.
- Adapt records/classes to universe polymorphism
- Now stops in EqDepFacts due to imprecise universe polymorphism.

Forgot to git add those files.

interp_constr returns the universe context

The context is then pushed through the environment (or proof goal
sigma).
- Fix insertion of constants/inductives in env, pushing constraints to
the global env for non-polymorphic ones.
- Add Prop as a universe level to do proper type inference with sorts.
It is allowed to take [sup] of [Prop] now.
- New nf_evar based on new Evd.map(_undefined)
- In proofs/logic.ml: conv_leq_goal might create some constraints that
are now recorded.
- Adapt Program code to universes.

Merge with latest trunk + fixes

-Use new constr_of_global from universes
- fix eqschemes to use polymorphic universes
- begin fixing cctac but f_equal still fails
- fix [simpl] and rest of tacred
- all the eq_constr with mkConst foo should be fixed as well, only
partially done

- Fix term hashing function to recognize equal terms up to universe instances.
- Fix congruence closure to equate terms that differ only in universe instances,
these will be resolved by constraints.

Add a set of undefined universe variables to unification.
Universe variables can now be declared rigid or flexible (unifiable).
Flexible variables are resolved at the end of typechecking by instantiating
them to their glb, adding upper bound constraints associated to them.
Also:
- Add polymorphic flag for inductives.
- Fix cooking partially
- Fix kernel/univ.ml to do normalization of universe expressions at
the end of substitution.

Correct classes/structures universe inference

- Required a bit of extension in Univ to handle Max properly (sup u
(u+1)) was returning (max(u,u+1)) for example.
- Try a version where substitution of universe expressions for universe
levels is allowed at the end of unification. By an invariant this
should only instantiate with max() types that are morally "on the
right" only.
This is controlled using a rigidity attribute of universe variables,
also allowing to properly do unification w.r.t. universes during
typechecking/inference.
- Currently fails in Vectors/Fin.v because case compilation generates
"flexible" universes that actually appear in the term...

Fix unification of universe variables.

- Fix choice of canonical universe in presence of universe constraints,
and do so by relying on a trichotomy for universe variables: rigid
(won't be substituted), flexible (might be if not substituted by an
algebraic) and flexible_alg (always substituted).
- Fix romega code and a few more plugins, most of the standard library
goes through now.
- Had to define some inductives as Polymorphic explicitly to make
proofs go through, more to come, and definitions should be polymorphic
too, otherwise inconsistencies appear quickly (two uses of the same
polymorphic ind through monomorphic functions (like nth on lists of
Props and nats) will fix the monomorphic function's universe with eq
constraints that are incompatible).
- Correct universe polymorphism handling for fixpoint/cofixpoint
definitions.

- Fix romega to use the right universes for list constructors.
- Fix internalization/externalization to deal properly with the
implicit parsing of params.
- Fix fourier tactic w.r.t. GRefs

- Fix substitution saturation of universes.
- Fix number syntax plugin.
- Fix setoid_ring to take its coefficients in a Set rather
than a Type, avoiding a large number of useless universe constraints.

- Fix minor checker decl
- Fix btauto w.r.t. GRef
- Fix proofview to normalize universes in the original types as well.
- Fix definitions of projections to not take two universes at the same level,
but at different levels instead, avoiding unnecessary constraints that could
lower the level of one component depending on the use of the other component.

Fix simpl fst, snd to use @fst @snd as they have maximal implicits now.

- More simpl snd, fst fixes.
- Try to make the nth theory of lists polymorphic.

Check with Enrico if this change is ok. Case appearing in RingMicromega's call
to congruence l417, through a call to refine -> the_conv_x_leq.

Compile everything.
- "Fix" checker by deactivating code related to polymorphism, should
be updated.
- Make most of List.v polymorphic to help with following definitions.
- When starting a lemma, normalize w.r.t. universes, so that the types
get a fixed universe, not refinable later.
- In record, don't assign a fully flexible universe variable to the record
type if it is a definitional typeclass, as translate_constant doesn't expect
an algebraic universe in the type of a constant. It certainly should though.
- Fix micromega code.

Fix after rebase.

Update printing functions to print the polymorphic status of definitions
and their universe context.

Refine printing of universe contexts

- Fix printer for universe constraints
- Rework normalization of constraints to separate the Union-Find result
  from computation of lubs/glbs.

Keep universe contexts of inductives/constants in entries for correct
substitution inside modules. Abstract interface to get an instantiation
of an inductive with its universe substitution in the kernel (no
substitution if the inductive is not polymorphic, even if mind_universes
is non-empty).

Make fst and snd polymorphic, fix instances in RelationPairs to use
different universes for the two elements of a pair.

- Fix bug in nf_constraints: was removing Set <= constraints, but should
remove Prop <= constraints only.
- Make proj1_sig, projT1... polymorphic to avoid weird universe unifications,
giving rise to universe inconsistenties.

Adapt auto hints to polymorphic references.

Really produce polymorphic hints... second try

- Remove algebraic universes that can't appear in the goal when taking the
  type of a lemma to start.

Proper handling of universe contexts in clenv and auto so that
polymorphic hints are really refreshed at each application.

Fix erroneous shadowing of sigma variable.

- Make apparent the universe context used in pretyping, including information
about flexibility of universe variables.
- Fix induction to generate a fresh constant instance with flexible universe variables.

Add function to do conversion w.r.t. an evar map and its local universes.

- Fix define_evar_as_sort to not forget constraints coming from the refinement.
- Do not nf_constraints while we don't have the whole term at hand to substitute in.

- Move substitution of full universes to Universes
- Normalize universes inside an evar_map when doing nf_evar_map_universes.
- Normalize universes at each call to interp_ltac (potentially expensive)

Do not normalize all evars at each call to interp_gen in tactics: rather
incrementally normalize the terms at hand, supposing the normalization of universes
will concern only those appearing in it (dangerous but much more efficient).

Do not needlessly generate new universes constraints for projections of records.

Correct polymorphic discharge of section variables.

Fix autorewrite w.r.t. universes: polymorphic rewrite hints get fresh universe
instances at each application.

Fix r2l rewrite scheme to support universe polymorphism

Fix a bug in l2r_forward scheme and fix congruence scheme to handle polymorphism correctly.

Second try at fixing autorewrite, cannot do without pushing the constraints and the set of fresh
universe variables into the proof context.

- tclPUSHCONTEXT allow to set the ctx universe variables as flexible or rigid
- Fix bug in elimschemes, not taking the right sigma

Wrong sigma used in leibniz_rewrite

Avoid recomputation of bounds for equal universes in normalization of constraints,
only the canonical one need to be computed.

Make coercions work with universe polymorphic projections.

Fix eronneous bound in universes constraint solving.

Make kernel reduction and term comparison strictly aware of universe instances,
with variants for relaxed comparison that output constraints.
Otherwise some constraints that should appear during pretyping don't and we generate
unnecessary constraints/universe variables.
Have to adapt a few tactics to this new behavior by making them universe aware.

- Fix elimschemes to minimize universe variables
- Fix coercions to not forget the universe constraints generated by an application
- Change universe substitutions to maps instead of assoc lists.
- Fix absurd tactic to handle univs properly
- Make length and app polymorphic in List, unification sets their levels otherwise.

Move to modules for namespace management instead of long names in universe code.

More putting things into modules.

Change evar_map structure to support an incremental substitution of universes
(populated from Eq constraints), allowing safe and fast inference of precise levels,
without computing lubs.
- Add many printers and reorganize code
- Extend nf_evar to normalize universe variables according to the substitution.
- Fix ChoiceFacts.v in Logic, no universe inconsistencies anymore. But Diaconescu
still has one (something fixes a universe to Set).
- Adapt omega, functional induction to the changes.

Fix congruence, eq_constr implem, discharge of polymorphic inductives.

Fix merge in auto.

The [-parameters-matter] option (formerly relevant_equality).

Add -parameters-matter to coqc

Do compute the param levels at elaboration time if parameters_matter.

- Fix generalize tactic
- add ppuniverse_subst
- Start fixing normalize_universe_context w.r.t. normalize_univ_variables.

- Fix HUGE bug in Ltac interpretation not folding the sigma correctly if interpreting a tactic application
to multiple arguments.
- Fix bug in union of universe substitution.

- rename parameters-matter to indices-matter
- Fix computation of levels from indices not parameters.

- Fixing parsing so that [Polymorphic] can be applied to gallina extensions.
- When elaborating definitions, make the universes from the type rigid when
checking the term: they should stay abstracted.
- Fix typeclasses eauto's handling of universes for exact hints.

Rework all the code for infering the levels of inductives and checking their
allowed eliminations sorts.

This is based on the computation of a natural level for an inductive type I.
The natural level [nat] of [I : args -> sort := c1 : A1 -> I t1 .. cn : An -> I tn] is
computed by taking the max of the levels of the args (if indices matter) and the
levels of the constructor arguments.
The declared level [decl] of I is [sort], which might be Prop, Set or some Type u (u fresh
or not).
If [decl >= nat && not (decl = Prop && n >= 2)], the level of the inductive is [decl],
otherwise, _smashing_ occured.
If [decl] is impredicative (Prop or Set when Set is impredicative), we accept the
declared level, otherwise it's an error.

To compute the allowed elimination sorts, we have the following situations:
- No smashing occured: all sorts are allowed. (Recall props that are not
smashed are Empty/Unitary props)
- Some smashing occured:
 - if [decl] is Type, we allow all eliminations (above or below [decl],
   not sure why this is justified in general).
 - if [decl] is Set, we used smashing for impredicativity, so only
   small sorts are allowed (Prop, Set).
 - if [decl] is Prop, only logical sorts are allowed: I has either
   large universes inside it or more than 1 constructor.
   This does not treat the case where only a Set appeared in I which
   was previously accepted it seems.

All the standard library works with these changes. Still have to cleanup
kernel/indtypes.ml. It is a good time to have a whiskey with OJ.

Thanks to Peter Lumsdaine for bug reporting:
- fix externalisation of universe instances (still appearing when no Printing Universes)
- add [convert] and [convert_leq] tactics that keep track of evars and universe constraints.
- use them in [exact_check].

Fix odd behavior in inductive type declarations allowing to silently lower a Type i parameter
to Set for squashing a naturally Type i inductive to Set. Reinstate the LargeNonPropInductiveNotInType
exception.

Fix the is_small function not dealing properly with aliases of Prop/Set in Type.

Add check_leq in Evd and use it to decide if we're trying to squash an
inductive naturally in some Type to Set.

- Fix handling of universe polymorphism in typeclasses Class/Instance declarations.
- Don't allow lowering a rigid Type universe to Set silently.

- Move Ring/Field back to Type. It was silently putting R in Set due to the definition of ring_morph.
- Rework inference of universe levels for inductive definitions.
- Make fold_left/right polymorphic on both levels A and B (the list's type). They don't have to be
at the same level.

Handle selective Polymorphic/Monomorphic flag right for records.

Remove leftover command

Fix after update with latest trunk.

Backport patches on HoTT/coq to rebased version of universe polymorphism.

- Fix autorewrite wrong handling of universe-polymorphic rewrite rules. Fixes part of issue #7.
- Fix the [eq_constr_univs] and add an [leq_constr_univs] to avoid eager equation of universe
 levels that could just be inequal. Use it during kernel conversion. Fixes issue #6.
- Fix a bug in unification that was failing too early if a choice in unification of universes
 raised an inconsistency.
- While normalizing universes, remove Prop in the le part of Max expressions.
- Stop rigidifying the universes on the right hand side of a : in definitions.
- Now Hints can be declared polymorphic or not. In the first case they
 must be "refreshed" (undefined universes are renamed) at each application.
- Have to refresh the set of universe variables associated to a hint
 when it can be used multiple times in a single proof to avoid fixing
 a level... A better & less expensive solution should exist.
- Do not include the levels of let-ins as part of records levels.
- Fix a NotConvertible uncaught exception to raise a more informative
 error message.
- Better substitution of algebraics in algebraics (for universe variables that
 can be algebraics).
- Fix issue #2, Context was not properly normalizing the universe context.
- Fix issue with typeclasses that were not catching UniverseInconsistencies
  raised by unification, resulting in early failure of proof-search.
- Let the result type of definitional classes be an algebraic.
- Adapt coercions to universe polymorphic flag (Identity Coercion etc..)
- Move away a dangerous call in autoinstance that added constraints for every
polymorphic definitions once in the environment for no use.

Forgot one part of the last patch on coercions.

- Adapt auto/eauto to polymorphic hints as well.
- Factor out the function to refresh a clenv w.r.t. undefined universes.

Use leq_univ_poly in evarconv to avoid fixing universes.

Disallow polymorphic hints based on a constr as it is not possible to infer their universe
context. Only global references can be made polymorphic. Fixes issue #8.

Fix SearchAbout bug (issue #10).

Fix program w.r.t. universes: the universe context of a definition changes
according to the successive refinements due to typechecking obligations.
This requires the Proof modules to return the generated universe substitution
when finishing a proof, and this information is passed in the closing hook.
The interface is not very clean, will certainly change in the future.

- Better treatment of polymorphic hints in auto: terms can be polymorphic now, we refresh their
context as well.
- Needs a little change in test-pattern that seems breaks multiary uses of destruct in NZDiv.v, l495.
FIX to do.

Fix [make_pattern_test] to keep the universe information around and still
allow tactics to take multiple patterns at once.

- Fix printing of universe instances that should not be factorized blindly
- Fix handling of the universe context in program definitions by allowing the
hook at the end of an interactive proof to give back the refined universe context,
before it is transformed in the kernel.
- Fix a bug in evarconv where solve_evar_evar was not checking types of instances,
resulting in a loss of constraints in unification of universes and a growing number
of useless parametric universes.

- Move from universe_level_subst to universe_subst everywhere.

- Changed representation of universes for a canonical one
- Adapt the code so that universe variables might be substituted by
arbitrary universes (including algebraics). Not used yet except for
polymorphic universe variables instances.

- Adapt code to new constraint structure.
- Fix setoid rewrite handling of evars that was forgetting the initial
universe substitution !
- Fix code that was just testing conversion instead of keeping the
resulting universe constraints around in the proof engine.
- Make a version of reduction/fconv that deals with the more general
set of universe constraints.

- [auto using] should use polymorphic versions of the constants.
- When starting a proof, don't forget about the algebraic universes in
the universe context.

Rationalize substitution and normalization functions for universes.
Also change back the structure of universes to avoid considering levels
n+k as pure levels: they are universe expressions like max.
Everything is factored out in the Universes and Univ modules now and
the normalization functions can be efficient in the sense that they
can cache the normalized universes incrementally.

- Adapt normalize_context code to new normalization/substitution functions.
- Set more things to be polymorphic, e.g. in Ring or SetoidList for the rest
of the code to work properly while the constraint generation code is not adapted.
And temporarily extend the universe constraint code in univ to solve max(is) = max(js)
by first-order unification (these constraints should actually be implied not enforced).
- Fix romega plugin to use the right universes for polymorphic lists.
- Fix auto not refreshing the poly hints correctly.

- Proper postponing of universe constraints during unification, avoid making
arbitrary choices.
- Fix nf_evars_and* to keep the substitution around for later normalizations.
- Do add simplified universe constraints coming from unification during typechecking.
- Fix solve_by_tac in obligations to handle universes right, and the corresponding
substitution function.

Test global universe equality early during simplication of constraints.

Better hashconsing, but still not good on universe lists.

- Add postponing of "lub" constraints that should not be checked early,
they are implied by the others.
- Fix constructor tactic to use a fresh constructor instance avoiding
fixing universes.
- Use [eq_constr_universes] instead of [eq_constr_univs] everywhere,
this is the comparison function that doesn't care about the universe
instances.
- Almost all the library compiles in this new setting, but some more tactics
need to be adapted.

- Reinstate hconsing.
- Keep Prop <= u constraints that can be used to set the level of a universe
metavariable.

Add better hashconsing and unionfind in normalisation of constraints.
Fix a few problems in choose_canonical, normalization and substitution functions.

Fix after merge

Fixes after rebase with latest Coq trunk, everything compiles again,
albeit slowly in some cases.
- Fix module substitution and comparison of table keys in conversion
using the wrong order (should always be UserOrd now)
- Cleanup in universes, removing commented code.
- Fix normalization of universe context which was assigning global
levels to local ones. Should always be the other way!
- Fix universe implementation to implement sorted cons of universes
preserving order. Makes Univ.sup correct again, keeping universe in
normalized form.
- In evarconv.ml, allow again a Fix to appear as head of a weak-head normal
form (due to partially applied fixpoints).
- Catch anomalies of conversion as errors in reductionops.ml, sad but
necessary as eta-expansion might build ill-typed stacks like FProd,
[shift;app Rel 1], as it expands not only if the other side is rigid.
- Fix module substitution bug in auto.ml

- Fix case compilation: impossible cases compilation was generating useless universe
levels. Use an IDProp constant instead of the polymorphic identity to not influence
the level of the original type when building the case construct for the return type.
- Simplify normalization of universe constraints.
- Compute constructor levels of records correctly.

Fall back to levels for universe instances, avoiding issues of unification.
Add more to the test-suite for universe polymorphism.

Fix after rebase with trunk

Fix substitution of universes inside fields/params of records to be made
after all normalization is done and the level of the record has been
computed.

Proper sharing of lower bounds with fixed universes.

Conflicts:
	library/universes.ml
	library/universes.mli

Constraints were not enforced in compilation of cases

Fix after rebase with trunk

- Canonical projections up to universes
- Fix computation of class/record universe levels to allow
squashing to Prop/Set in impredicative set mode.

- Fix descend_in_conjunctions to properly instantiate projections with universes
- Avoid Context-bound variables taking extra universes in their associated universe context.

- Fix evar_define using the wrong direction when refreshing a universe under cumulativity
- Do not instantiate a local universe with some lower bound to a global one just because
they have the same local glb (they might not have the same one globally).

- Was loosing some global constraints during normalization (brought again by the kernel), fixed now.
- Proper [abstract] with polymorphic lemmas (polymorphic if the current proof is).
- Fix silly bug in autorewrite: any hint after the first one was always monomorphic.

- Fix fourier after rebase
- Refresh universes when checking types of metas in unification (avoid (sup (sup univ))).
- Speedup a script in FSetPositive.v

Rework definitions in RelationClasses and Morphisms to share universe
levels as much as possible. This factorizes many useless x <=
RelationClasses.foo constraints in code that uses setoid rewriting.
Slight incompatible change in the implicits for Reflexivity and
Irreflexivity as well.

- Share even more universes in Morphisms using a let.
- Use splay_prod instead of splay_prod_assum which doesn't reduce let's
to find a relation in setoid_rewrite
- Fix [Declare Instance] not properly dealing with let's in typeclass contexts.

Fixes in inductiveops, evarutil.

Patch by Yves Bertot to allow naming universes in inductive definitions.

Fixes in tacinterp not propagating evars correctly.

Fix for issue #27: lowering a Type to Prop is allowed during
inference (resulting in a Type (* Set *)) but kernel reduction
was wrongly refusing the equation [Type (*Set*) = Set].

Fix in interface of canonical structures: an instantiated polymorphic
projection is not needed to lookup a structure, just the projection name
is enough (reported by C. Cohen).

Move from universe inference to universe checking in the kernel.

All tactics have to be adapted so that they carry around their generated
constraints (living in their sigma), which is mostly straightforward.
The more important changes are when refering to Coq constants, the
tactics code is adapted so that primitive eq, pairing and sigma types might
be polymorphic.
Fix another few places in tacinterp and evarconv/evarsolve where the sigma
was not folded correctly.

- Fix discharge adding spurious global constraints on polymorphic universe variables
appearing in assumptions.
- Fixes in inductiveops not taking into account universe polymorphic inductives.

WIP on checked universe polymorphism, it is clearly incompatible
with the previous usage of polymorphic inductives + non-polymorphic
definitions on them as universe levels now appear in the inductive type,
and add equality constraints between universes that were otherwise just
in a cumulativity relation (not sure that was actually correct).

Refined version of unification of universe instances for first-order unification,
prefering unfolding to arbitrary identification of universes.

Moved kernel to universe checking only.

Adapt the code to properly infer constraints during typechecking and
refinement (tactics) and only check constraints when adding
constants/inductives to the environment. Exception made of module
subtyping that needs inference of constraints...  The kernel conversion
(fconv) has two modes: checking only and inference, the later being used
by modules only. Evarconv/unification make use of a different strategy for
conversion of constants that prefer unfolding to blind unification of
rigid universes. Likewise, conversion checking backtracks on different universe
instances (modulo the constraints).

- adapt congruence/funind/ring plugins to this new mode, forcing them to
declare their constraints.
- To avoid big performance penalty with reification, make ring/field non-polymorphic
(non-linear explosion in run time to be investigated further).
- pattern and change tactics need special treatment: as they are not _reduction_
but conversion functions, their operation requires to update an evar_map with
new universe constraints.
- Fix vm_compute to work better with universes. If the normal
form is made only of constructors then the readback is correct. However a deeper change will
be needed to treat substitution of universe instances when unfolding constants.

Remove libtypes.ml

Fix after merge.

Fix after rebase with trunk.

**** Add projections to the kernel, as optimized implementations of constants.

- New constructor Proj expects a projection constant applied to its principal
inductive argument.
- Reduction machines shortcut the expansion to a case and directly project the
right argument.
- No need to keep parameters as part of the projection's arguments as they
are inferable from the type of the principal argument.
- ML code now compiles, debugging needed.

Start debugging the implementation of projections. Externalisation should
keep the information about projections.

Internalization, pattern-matching, unification and reduction
of projections.

Fix some code that used to have _ for parameters that are no longer
present in projections.

Fixes in unification, reduction, term indexing, auto hints based on projections,
add debug printers.

Fix byte-compilation of projections, unification, congruence with projections.
Adapt .v files using "@proj _ _ record" syntax, should come back on this later.
Fix coercion insertion code to properly deal with projection coercions.
Fix [simpl proj]... TODO [unfold proj], proj is not considered evaluable.

- Fix whnf of projections, now respecting opacity information.
- Fix conversion of projections to try first-order first and then
incrementally unfold them.
- Fix computation of implicit args for projections, simply dropping
the information for parameters.
- Fix a few scripts that relied on projections carrying their parameters (few at's,
rewrites).
- Fix unify_with_subterm to properly match under projections.
- Fix bug in cooking of projections.
- Add pattern PProj for projections.
- A very strange bug appeared in BigZ.v, making coqtop segfault on the export
of BigN... tofix

Fixes after rebase with trunk. Everything compiles now, with efficient
projections.

Fixes after rebase with trunk (esp. reductionops).

Remove warnings, backport patch from old univs+projs branch.

Proper expansion of projections during unification.

They are considered as maybe flexible keys in evarconv/unification. We
try firstorder unification and otherwise expand them as necessary,
completely mimicking the original behavior, when they were
constants.  Fix head_constr_bound interface, the arguments are never
needed (they're outside their environment actually).  [simpl] and
[red]/[intro] should behave just like before now.

Fix evarconv that was giving up on proj x = ?e problems too early.

- Port patch by Maxime Denes implementing fast projections in the native conversion.
- Backport patch to add eta-expansion for records.

Do not raise an exception but simply fails if trying to do eta on an inductive that is not a record.

Fix projections detyping/matching and unification.ml not always
recovering on first-order universe inequalities.

Correct eta-expansion for records, and change strategy for conversion
with projections to favor reduction over first-order unification a
little more. Fix a bug in Ltac pattern matching on projections.

Fix evars_reset_evd to not recheck existing constraints in case it is just an update
(performance improvement for typeclass resolution).

- Respect Global/Transparent oracle during unification. Opaque means
_never_ unfolded there.
- Add empty universes as well as the initial universes (having Prop < Set).
- Better display of universe inconsistencies.

- Add Beta Ziliani's patch to go fast avoiding imitation when possible.
- Allow instantiation by lower bound even if there are universes above
- (tentative) In refinement, avoid incremental refinement of terms
  containing no holes and do it in one step (much faster on big terms).
  Turned on only if not a checked command.

Remove dead code in univ/universes.ml and cleanup setup of hashconsing,
for a small speed and memory footprint improvement.

- Fix bug in unification using cumulativity when conversion should have been used.
- Fix unification of evars having type Type, no longer forcing them to be equal
(potentially more constraints): algorithm is now complete w.r.t. cumulativity.
- In clenvtac, use refine_nocheck as we are guaranteed to get well-typed terms
from unification now, including sufficient universe constraints. Small general
speedup.

- Fix inference of universe levels of inductive types to avoid smashing
  inadvertently from Set to Prop.
- Fix computation of discharged hypotheses forgetting the arity in inductives.

- Fix wrong order in printing of universe inconsistency explanation
- Allow coercions between two polymorphic instances of the same inductive/constant.
- Do evar normalization and saturation by classes before trying to use program coercion
  during pretyping.
- In unification, force equalities of universes when unifying the same rigid head constants.

- Fix omission of projections in constr_leq
- Fix [admit] tactic's handling of normalized universes.

Fix typing of projections not properly normalizing w.r.t. evars, resulting in anomaly sometimes.

Adapt rewrite to work with computational relations (in Type), while
maintaining backward compatibility with Propositional rewriting.

Introduce a [diff] function on evar maps and universe contexts to
properly deal with clause environments. Local hints in auto now store
just the extension of the evar map they rely on, so merging them becomes
efficient. This fixes an important performance issue in auto and typeclass
resolution in presence of a large number of universe constraints.

Change FSetPositive and MSetPositive to put their [elt] and [t] universes in
Type to avoid restricting global universes to [Set]. This is due to [flip]s
polymorphic type being fixed in monomorphic instances of Morphisms.v,
and rewriting hence forcing unification of levels that could be left unrelated.

- Try a fast_typeops implementation of kernel type inference that
  allocates less by not rebuilding the term, shows a little performance
  improvement, and less allocation.
- Build universe inconsistency explanations lazily, avoiding huge blowup
  (x5) in check_constraints/merge_constraints in time and space (these
  are stressed in universe polymorphic mode).
- Hashcons universe instances.

Add interface file for fast_typeops

Use monomorphic comparisons, little optimizations of hashconsing and
comparison in univ.ml.

Fix huge slowdown due to building huge error messages. Lazy is not
enough to tame this completely.

Fix last performance issue, due to abstracts building huge terms abstracting on parts of the section
context. Was due to wrong handling of Let... Qed.s in abstract. Performance is a tiny bit better than the
trunk now.

First step at compatibility layer for projections.

Compatibility mode for projections. c.(p), p c use primitive projs,
while @p refers to an expansion [λ params c, c.(p)]. Recovers almost
entire source compatibility with trunk scripts, except when mixing
@p and p and doing syntactic matching (they're unifiable though).

Add a [Set Primitive Projections] flag to set/unset the use of primitive
projections, selectively for each record. Adapt code to handle both the
legacy encoding and the primitive projections. Library is almost
source-to-source compatible, except for syntactic operations relying
on the presence of parameters. In primitive projections mode, @p refers
to an expansion [λ params r. p.(r)]. More information in CHANGES (to be
reformated/moved to reference manual).

Backport changes from HoTT/coq:

- Fix anomaly on uncatched NotASort in retyping.
- Better recognition of evars that are subject to typeclass resolution.
  Fixes bug reported by J. Gross on coq-club.
- Print universe polymorphism information for parameters as well.

Fix interface for unsatisfiable constraints error, now a type error.
Try making ring polymorphic again, with a big slowdown, to be investigated.
Fix evar/universe leak in setoid rewrite.

- Add profiling flag
- Move setoid_ring back to non-polymorphic mode to compare perfs with trunk
- Change unification to allow using infer_conv more often (big perf culprit),
  but semantics of backtracking on unification of constants is not properly
  implemented there.
- Fix is_empty/union_evar_universe_context forgetting about some assignments.
- Performance is now very close to the trunk from june,
  with projections deactivated.

1 files changed, 1472 insertions, 350 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 551d740434..8322a7e962 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -29,13 +29,56 @@ open Util
    union-find algorithm. The assertions $<$ and $\le$ are represented by
    adjacency lists *)
 
-module UniverseLevel = struct
+module Level = struct
 
   open Names
 
   type t =
+    | Prop
     | Set
-    | Level of int * DirPath.t
+    | Level of int * Names.DirPath.t
+  type _t = t
+
+  (* Hash-consing *)
+    
+  module Hunivlevel =
+  Hashcons.Make(
+    struct
+      type t = _t
+      type u = Names.DirPath.t -> Names.DirPath.t
+      let hashcons hdir = function
+	| Prop as x -> x
+	| Set as x -> x
+	| Level (n,d) -> Level (n,hdir d)
+      let equal l1 l2 =
+        l1 == l2 ||
+        match l1,l2 with
+	| Prop, Prop -> true
+	| Set, Set -> true
+	| Level (n,d), Level (n',d') ->
+	  n == n' && d == d'
+	| _ -> false
+      let hash = Hashtbl.hash
+    end)
+  
+  let hcons = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons
+
+  let make m n = hcons (Level (n, m))
+
+  let set = hcons Set
+  let prop = hcons Prop
+
+  let is_small = function
+    | Level _ -> false
+    | _ -> true
+
+  let is_prop = function
+    | Prop -> true
+    | _ -> false
+
+  let is_set = function
+    | Set -> true
+    | _ -> false
 
   (* A specialized comparison function: we compare the [int] part first.
      This way, most of the time, the [DirPath.t] part is not considered.
@@ -49,6 +92,9 @@ module UniverseLevel = struct
     if u == v then 0
     else
     (match u,v with
+    | Prop,Prop -> 0
+    | Prop, _ -> -1
+    | _, Prop -> 1
     | Set, Set -> 0
     | Set, _ -> -1
     | _, Set -> 1
@@ -63,27 +109,385 @@ module UniverseLevel = struct
       Int.equal i1 i2 && DirPath.equal dp1 dp2
     | _ -> false
 
-  let hash = function
-  | Set -> 0
-  | Level (i, dp) ->
-    Hashset.Combine.combine (Int.hash i) (DirPath.hash dp)
-
-  let make m n = Level (n, m)
+  let eq u v = u == v
+  let leq u v = compare u v <= 0
 
   let to_string = function
+    | Prop -> "Prop"
     | Set -> "Set"
-    | Level (n,d) -> DirPath.to_string d^"."^string_of_int n
+    | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+
+  let pr u = str (to_string u)
+
+  let apart u v =
+    match u, v with
+    | Prop, Set | Set, Prop -> true
+    | _ -> false
+
 end
 
-module UniverseLMap = Map.Make (UniverseLevel)
-module UniverseLSet = Set.Make (UniverseLevel)
+let pr_universe_level_list l = 
+  prlist_with_sep spc Level.pr l
+
+module LSet = struct
+  module M = Set.Make (Level)
+  include M
+
+  let pr s = 
+    str"{" ++ pr_universe_level_list (elements s) ++ str"}"
 
-type universe_level = UniverseLevel.t
+  let of_list l =
+    List.fold_left (fun acc x -> add x acc) empty l
 
-let compare_levels = UniverseLevel.compare
+  let of_array l =
+    Array.fold_left (fun acc x -> add x acc) empty l
+end
+
+module LMap = struct 
+  module M = Map.Make (Level)
+  include M
+
+  let union l r = 
+    merge (fun k l r -> 
+      match l, r with
+      | Some _, _ -> l
+      | _, _ -> r) l r
+
+  let subst_union l r = 
+    merge (fun k l r -> 
+      match l, r with
+      | Some (Some _), _ -> l
+      | Some None, None -> l
+      | _, _ -> r) l r
+
+  let diff ext orig =
+    fold (fun u v acc -> 
+      if mem u orig then acc 
+      else add u v acc)
+      ext empty
+
+  let elements = bindings
+  let of_set s d = 
+    LSet.fold (fun u -> add u d) s
+      empty
+    
+  let of_list l =
+    List.fold_left (fun m (u, v) -> add u v m) empty l 
+    
+  let universes m =
+    fold (fun u _ acc -> LSet.add u acc) m LSet.empty
+
+  let pr f m =
+    h 0 (prlist_with_sep fnl (fun (u, v) ->
+      Level.pr u ++ f v) (elements m))
+
+  let find_opt t m =
+    try Some (find t m)
+    with Not_found -> None
+end
+
+type universe_level = Level.t
+
+module LList = struct
+  type t = Level.t list
+  type _t = t
+  module Huniverse_level_list = 
+  Hashcons.Make(
+    struct
+      type t = _t
+      type u = universe_level -> universe_level
+      let hashcons huc s =
+	List.fold_right (fun x a -> huc x :: a) s []
+      let equal s s' = List.for_all2eq (==) s s'
+      let hash = Hashtbl.hash
+    end)
+
+  let hcons = 
+    Hashcons.simple_hcons Huniverse_level_list.generate Level.hcons
+
+  let empty = hcons []
+  let eq l l' = l == l' ||
+    (try List.for_all2 Level.eq l l'
+     with Invalid_argument _ -> false)
+
+  let levels =
+    List.fold_left (fun s x -> LSet.add x s) LSet.empty
+
+end
+
+type universe_level_list = universe_level list
+
+type universe_level_subst_fn = universe_level -> universe_level
+
+type universe_set = LSet.t
+type 'a universe_map = 'a LMap.t
+
+let compare_levels = Level.compare
+let eq_levels = Level.eq
+
+module Hashconsing = struct
+  module Uid = struct
+    type t = int
+
+    let make_maker () =
+      let _id = ref ~-1 in
+	((fun () -> incr _id;!_id),
+	 (fun () -> !_id),
+	 (fun i -> _id := i))
+
+    let dummy = -1
+
+    external to_int : t -> int = "%identity"
+
+
+    external of_int : int -> t= "%identity"
+  end
+    
+  module Hcons = struct
+
+    module type SA =
+    sig
+      type data
+      type t
+      val make : data -> t
+      val node : t -> data
+      val hash : t -> int
+      val uid : t -> Uid.t
+      val equal : t -> t -> bool
+      val stats : unit -> unit
+      val init : unit -> unit
+    end
+
+    module type S =
+    sig
+
+      type data
+      type t = private { id : Uid.t;
+			 key : int;
+			 node : data }
+      val make : data -> t
+      val node : t -> data
+      val hash : t -> int
+      val uid : t -> Uid.t
+      val equal : t -> t -> bool
+      val stats : unit -> unit
+      val init : unit -> unit
+    end
+
+    module Make (H : Hashtbl.HashedType) : S with type data = H.t =
+    struct
+      let uid_make,uid_current,uid_set = Uid.make_maker()
+      type data = H.t
+      type t = { id : Uid.t;
+		 key : int;
+		 node : data }
+      let node t = t.node
+      let uid t = t.id
+      let hash t = t.key
+      let equal t1 t2 = t1 == t2
+      module WH = Weak.Make( struct
+	type _t = t
+	type t = _t
+	let hash = hash
+	let equal a b = a == b || H.equal a.node b.node
+      end)
+      let pool = WH.create 491
+
+      exception Found of Uid.t
+      let total_count = ref 0
+      let miss_count = ref 0
+      let init () =
+	total_count := 0;
+	miss_count := 0
+
+      let make x =
+	incr total_count;
+	let cell = { id = Uid.dummy; key = H.hash x; node = x } in
+	  try
+	  WH.find pool cell
+	  with
+	  | Not_found ->
+	  let cell = { cell with id = uid_make(); } in
+	    incr miss_count;
+	    WH.add pool cell;
+	    cell
+
+      exception Found of t
+
+      let stats () = ()
+    end
+  end
+  module HList = struct
+
+    module type S = sig
+      type elt
+      type 'a node = Nil | Cons of elt * 'a
+
+      module rec Node :
+      sig
+	include Hcons.S with type data = Data.t
+      end
+      and Data : sig
+	include Hashtbl.HashedType with type t = Node.t node
+      end
+      type data = Data.t
+      type t = Node.t
+      val hash : t -> int
+      val uid : t -> Uid.t
+      val make : data -> t
+      val equal : t -> t -> bool
+      val nil : t
+      val is_nil : t -> bool
+      val tip : elt -> t
+      val node : t -> t node
+      val cons : (* ?sorted:bool -> *) elt -> t -> t
+      val hd : t -> elt
+      val tl : t -> t
+      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+      val map : (elt -> elt) -> t -> t
+      val iter : (elt -> 'a) -> t -> unit
+      val exists : (elt -> bool) -> t -> bool
+      val for_all : (elt -> bool) -> t -> bool
+      val rev : t -> t
+      val rev_map : (elt -> elt) -> t -> t
+      val length : t -> int
+      val mem : elt -> t -> bool
+      val remove : elt -> t -> t
+      val stats : unit -> unit
+      val init : unit -> unit
+      val to_list : t -> elt list
+      val compare : (elt -> elt -> int) -> t -> t -> int
+    end
+
+    module Make (H : Hcons.SA) : S with type elt = H.t =
+    struct
+      type elt = H.t
+      type 'a node = Nil | Cons of elt * 'a
+      module rec Node : Hcons.S with type data = Data.t = Hcons.Make (Data)
+				and Data : Hashtbl.HashedType  with type t = Node.t node =
+      struct
+	type t = Node.t node
+	let equal x y =
+	  match x,y with
+	  | _,_ when x==y -> true
+	  | Cons (a,aa), Cons(b,bb) -> (aa==bb) && (H.equal a b)
+	  | _ -> false
+	let hash = function
+	  | Nil -> 0
+	  | Cons(a,aa) -> 17 + 65599 * (Uid.to_int (H.uid a)) + 491 * (Uid.to_int aa.Node.id)
+      end
+      
+    type data = Data.t
+    type t = Node.t
+    let make = Node.make
+    let node x = x.Node.node
+    let hash x = x.Node.key
+    let equal = Node.equal
+    let uid x= x.Node.id
+    let nil = Node.make Nil
+    let stats = Node.stats
+    let init = Node.init
+
+    let is_nil =
+      function { Node.node = Nil } -> true | _ -> false
+				  
+    (* doing sorted insertion allows to make
+       better use of hash consing *)
+    let rec sorted_cons e l =
+      match l.Node.node with
+      |	Nil -> Node.make (Cons(e, l))
+      | Cons (x, ll) ->
+      if H.uid e < H.uid x
+      then Node.make (Cons(e, l))
+      else Node.make (Cons(x, sorted_cons e ll))
+
+    let cons e l =
+      Node.make(Cons(e, l))
+      
+    let tip e = Node.make (Cons(e, nil))
+
+    (* let cons ?(sorted=true) e l = *)
+    (*   if sorted then sorted_cons e l else cons e l *)
+
+    let hd = function { Node.node = Cons(a,_) } -> a | _ -> failwith "hd"
+    let tl = function { Node.node = Cons(_,a) } -> a | _ -> failwith "tl"
+    
+    let fold f l acc =
+      let rec loop acc l = match l.Node.node with
+	| Nil -> acc
+	| Cons (a, aa) -> loop (f a acc) aa
+      in
+	loop acc l
+
+    let map f l  =
+      let rec loop l = match l.Node.node with
+	| Nil -> nil
+	| Cons(a, aa) -> cons (f a) (loop aa)
+      in
+	loop l
+
+    let iter f l =
+      let rec loop l = match l.Node.node with
+	| Nil -> ()
+	| Cons(a,aa) ->  (f a);(loop aa)
+      in
+	loop l
+	
+    let exists f l =
+      let rec loop l = match l.Node.node with
+	| Nil -> false
+	| Cons(a,aa) -> f a || loop aa
+      in
+	loop l
+	
+    let for_all f l =
+      let rec loop l = match l.Node.node with
+	| Nil -> true
+	| Cons(a,aa) -> f a && loop aa
+      in
+	loop l
+
+    let to_list l =
+      let rec loop l = match l.Node.node with
+	| Nil -> []
+	| Cons(a,aa) -> a :: loop aa
+      in
+	loop l
+	
+    let remove x l =
+      let rec loop l = match l.Node.node with
+	| Nil -> l
+	| Cons(a,aa) -> 
+	  if H.equal a x then aa
+	  else cons a (loop aa)
+      in
+	loop l
+
+    let rev l = fold cons l nil
+    let rev_map f l = fold (fun x acc -> cons (f x) acc) l nil
+    let length l = fold (fun _ c -> c+1) l 0
+    let rec mem e l =
+      match l.Node.node with
+      | Nil -> false
+      | Cons (x, ll) -> x == e || mem e ll
+
+    let rec compare cmp l1 l2 =
+      if l1 == l2 then 0 else
+	match node l1, node l2 with
+	| Nil, Nil -> 0
+	| _, Nil -> 1
+	| Nil, _ -> -1
+	| Cons (x1,l1), Cons(x2,l2) ->
+          (match cmp x1 x2 with
+          | 0 -> compare cmp l1 l2
+          | c -> c)
+      
+    end
+  end
+end
 
 (* An algebraic universe [universe] is either a universe variable
-   [UniverseLevel.t] or a formal universe known to be greater than some
+   [Level.t] or a formal universe known to be greater than some
    universe variables and strictly greater than some (other) universe
    variables
 
@@ -96,158 +500,346 @@ let compare_levels = UniverseLevel.compare
 
 module Universe =
 struct
-  type t =
-  | Atom of UniverseLevel.t
-  | Max of UniverseLevel.t list * UniverseLevel.t list
+  (* Invariants: non empty, sorted and without duplicates *)
+
+  module Expr = 
+  struct
+    type t = Level.t * int
+    type _t = t
+	
+    (* Hashing of expressions *)
+    module ExprHash = 
+    struct
+      type t = _t
+      type u = Level.t -> Level.t
+      let hashcons hdir (b,n as x) = 
+	let b' = hdir b in 
+	  if b' == b then x else (b',n)
+      let equal l1 l2 =
+        l1 == l2 || 
+        match l1,l2 with
+	| (b,n), (b',n') -> b == b' && n == n'
+      let hash = Hashtbl.hash
+
+    end
+
+    module HExpr = 
+    struct 
+
+      include Hashcons.Make(ExprHash)
+
+      type data = t
+      type node = t
+
+      let make =
+	Hashcons.simple_hcons generate Level.hcons
+      external node : node -> data = "%identity"
+      let hash = ExprHash.hash
+      let uid = hash
+      let equal x y = x == y
+      let stats _ = ()
+      let init _ = ()
+    end
+
+    let hcons = HExpr.make
+
+    let make l = hcons (l, 0)
+
+    let compare u v =
+      if u == v then 0
+      else 
+	let (x, n) = u and (x', n') = v in
+	  if Int.equal n n' then Level.compare x x'
+	  else n - n'
+
+    let prop = make Level.prop
+    let set = make Level.set
+    let type1 = hcons (Level.set, 1)
+
+    let is_prop = function
+      | (l,0) -> Level.is_prop l
+      | _ -> false
+
+    let is_set = function
+      | (l,0) -> Level.is_set l
+      | _ -> false
+      
+    let is_type1 = function
+      | (l,1) -> Level.is_set l
+      | _ -> false
+          
+    let is_small = function
+      | (l, 0) -> Level.is_small l
+      | _ -> false
+
+    (* let eq (u,n) (v,n') = *)
+    (*   Int.equal n n' && Level.eq u v *)
+    let eq x y = x == y
+
+    let leq (u,n) (v,n') =
+      let cmp = Level.compare u v in
+	if Int.equal cmp 0 then n <= n'
+	else if n <= n' then 
+	  (Level.is_prop u && Level.is_small v)
+	else false
+
+    let successor (u,n) =
+      if Level.is_prop u then type1
+      else hcons (u, n + 1)
+
+    let addn k (u,n as x) = 
+      if k = 0 then x 
+      else if Level.is_prop u then
+	hcons (Level.set,n+k)
+      else hcons (u,n+k)
+	
+    let super (u,n as x) (v,n' as y) =
+      let cmp = Level.compare u v in
+	if Int.equal cmp 0 then 
+	  if n < n' then Inl true
+	  else Inl false
+	else if is_prop x then Inl true
+	else if is_prop y then Inl false
+	else Inr cmp
+
+    let to_string (v, n) =
+      if Int.equal n 0 then Level.to_string v
+      else Level.to_string v ^ "+" ^ string_of_int n
+
+    let pr x = str(to_string x)
+
+    let level = function
+      | (v,0) -> Some v
+      | _ -> None
+	
+    let get_level (v,n) = v
+
+    let map f (v, n as x) = 
+      let v' = f v in 
+	if v' == v then x
+	else if Level.is_prop v' && n != 0 then
+	  hcons (Level.set, n)
+	else hcons (v', n)
+
+  end
+
+  module Hunivelt = struct
+    let node x = x
+    let make x = x
+  end
+
+  (* module Hunivelt = Hashconsing.Hcons.Make( *)
+  (* struct *)
+  (*   type t = Expr.t *)
+  (*   let equal l1 l2 = *)
+  (*     l1 == l2 ||  *)
+  (*     match l1,l2 with *)
+  (*     | (b,n), (b',n') -> b == b' && n == n' *)
+  (*   let hash = Hashtbl.hash *)
+  (* end) *)
+    
+  let compare_expr n m = Expr.compare (Hunivelt.node n) (Hunivelt.node m)
+  let pr_expr n = Expr.pr (Hunivelt.node n)
+
+  module Huniv = Hashconsing.HList.Make(Expr.HExpr)
+  type t = Huniv.t
+  open Huniv
+    
+  let eq x y = x == y (* Huniv.equal *)
 
   let compare u1 u2 =
-    if u1 == u2 then 0 else
-    match u1, u2 with
-    | Atom l1, Atom l2 -> UniverseLevel.compare l1 l2
-    | Max (lt1, le1), Max (lt2, le2) ->
-      let c = List.compare UniverseLevel.compare lt1 lt2 in
-      if Int.equal c 0 then
-        List.compare UniverseLevel.compare le1 le2
-      else c
-    | Atom _, Max _ -> -1
-    | Max _, Atom _ -> 1
-
-  let equal u1 u2 = Int.equal (compare u1 u2) 0
-
-  let make l = Atom l
-
-  open Hashset.Combine
-
-  let rec hash_list accu = function
-  | [] -> 0
-  | u :: us ->
-    let accu = combine (UniverseLevel.hash u) accu in
-    hash_list accu us
-
-  let hash = function
-  | Atom u -> combinesmall 1 (UniverseLevel.hash u)
-  | Max (lt, le) ->
-    let hlt = hash_list 0 lt in
-    let hle = hash_list 0 le in
-    combinesmall 2 (combine hlt hle)
+    if eq u1 u2 then 0 else 
+      Huniv.compare compare_expr u1 u2
+
+  let hcons_unique = Huniv.make
+  let normalize x = x
+  (* let hcons_unique x = x *)
+  let hcons x = hcons_unique (normalize x)
+
+  let make l = Huniv.tip (Hunivelt.make (Expr.make l))
+  let tip x = Huniv.tip (Hunivelt.make x)
+    
+  let equal_universes x y = 
+    x == y
+(* then true *)
+(*     else *)
+(* 	(\* Consider lists as sets, i.e. up to reordering, *)
+(* 	   they are already without duplicates thanks to normalization. *\) *)
+(*         CList.eq_set x' y' *)
+
+  let pr l = match node l with
+    | Cons (u, n) when is_nil n -> Expr.pr (Hunivelt.node u)
+    | _ -> 
+      str "max(" ++ hov 0
+	(prlist_with_sep pr_comma Expr.pr (List.map Hunivelt.node (to_list l))) ++
+        str ")"
+      
+  let atom l = match node l with
+    | Cons (l, n) when is_nil n -> Some l
+    | _ -> None
+
+  let level l = match node l with
+    | Cons (l, n) when is_nil n -> Expr.level (Hunivelt.node l)
+    | _ -> None
+
+  let levels l = 
+    fold (fun x acc -> LSet.add (Expr.get_level (Hunivelt.node x)) acc) l LSet.empty
+
+  let is_small u = 
+    match level (normalize u) with
+    | Some l -> Level.is_small l
+    | _ -> false
 
-end
+  (* The lower predicative level of the hierarchy that contains (impredicative)
+     Prop and singleton inductive types *)
+  let type0m = tip Expr.prop
 
-open Universe
+  (* The level of sets *)
+  let type0 = tip Expr.set
+
+  (* When typing [Prop] and [Set], there is no constraint on the level,
+     hence the definition of [type1_univ], the type of [Prop] *)    
+  let type1 = tip (Expr.successor Expr.set)
+
+  let is_type0m u =
+    match level u with
+    | Some l -> Level.is_prop l
+    | _ -> false
+
+  let is_type0 u =
+    match level u with
+    | Some l -> Level.is_set l
+    | _ -> false
+
+  let is_type1 u =
+    match node u with
+    | Cons (l, n) when is_nil n -> Expr.is_type1 (Hunivelt.node l)
+    | _ -> false
+
+  (* Returns the formal universe that lies juste above the universe variable u.
+     Used to type the sort u. *)
+  let super l = 
+    Huniv.map (fun x -> Hunivelt.make (Expr.successor (Hunivelt.node x))) l
+
+  let addn n l =
+    Huniv.map (fun x -> Hunivelt.make (Expr.addn n (Hunivelt.node x))) l
+
+  let rec merge_univs l1 l2 =
+    match node l1, node l2 with
+    | Nil, _ -> l2
+    | _, Nil -> l1
+    | Cons (h1, t1), Cons (h2, t2) ->
+      (match Expr.super (Hunivelt.node h1) (Hunivelt.node h2) with
+      | Inl true (* h1 < h2 *) -> merge_univs t1 l2
+      | Inl false -> merge_univs l1 t2
+      | Inr c -> 
+        if c <= 0 (* h1 < h2 is name order *)
+	then cons h1 (merge_univs t1 l2)
+	else cons h2 (merge_univs l1 t2))
+
+  let sort u =
+    let rec aux a l = 
+      match node l with
+      | Cons (b, l') -> 
+        (match Expr.super (Hunivelt.node a) (Hunivelt.node b) with
+	| Inl false -> aux a l'
+	| Inl true -> l
+	| Inr c ->
+	  if c <= 0 then cons a l
+	  else cons b (aux a l'))
+      | Nil -> cons a l
+    in 
+      fold (fun a acc -> aux a acc) u nil
+	
+  (* Returns the formal universe that is greater than the universes u and v.
+     Used to type the products. *)
+  let sup x y = merge_univs x y
+
+  let of_list l = 
+    List.fold_right
+      (fun x acc -> cons (Hunivelt.make x) acc)
+      l nil
+    
+  let empty = nil
+  let is_empty n = is_nil n
+
+  let exists f l = 
+    Huniv.exists (fun x -> f (Hunivelt.node x)) l
+
+  let for_all f l = 
+    Huniv.for_all (fun x -> f (Hunivelt.node x)) l
+
+  let smartmap f l =
+    Huniv.map (fun x -> 
+      let n = Hunivelt.node x in
+      let x' = f n in
+	if x' == n then x else Hunivelt.make x')
+      l
+
+end
 
 type universe = Universe.t
 
-let universe_level = function
-  | Atom l -> Some l
-  | Max _ -> None
+open Universe
 
-let pr_uni_level u = str (UniverseLevel.to_string u)
+(* type universe_list = UList.t *)
+(* let pr_universe_list = UList.pr *)
 
-let pr_uni = function
-  | Atom u ->
-      pr_uni_level u
-  | Max ([],[u]) ->
-      str "(" ++ pr_uni_level u ++ str ")+1"
-  | Max (gel,gtl) ->
-      let opt_sep = match gel, gtl with
-      | [], _ | _, [] -> mt ()
-      | _ -> pr_comma ()
-      in
-      str "max(" ++ hov 0
-       (prlist_with_sep pr_comma pr_uni_level gel ++ opt_sep ++
-	prlist_with_sep pr_comma
-	  (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++
-      str ")"
-
-(* Returns the formal universe that lies juste above the universe variable u.
-   Used to type the sort u. *)
-let super = function
-  | Atom u ->
-      Max ([],[u])
-  | Max _ ->
-      anomaly (str "Cannot take the successor of a non variable universe" ++ spc () ++
-               str "(maybe a bugged tactic)")
-
-(* Returns the formal universe that is greater than the universes u and v.
-   Used to type the products. *)
-let sup u v =
-  match u,v with
-    | Atom u, Atom v ->
-	if UniverseLevel.equal u v then Atom u else Max ([u;v],[])
-    | u, Max ([],[]) -> u
-    | Max ([],[]), v -> v
-    | Atom u, Max (gel,gtl) -> Max (List.add_set UniverseLevel.equal u gel,gtl)
-    | Max (gel,gtl), Atom v -> Max (List.add_set UniverseLevel.equal v gel,gtl)
-    | Max (gel,gtl), Max (gel',gtl') ->
-	let gel'' = List.union UniverseLevel.equal gel gel' in
-	let gtl'' = List.union UniverseLevel.equal gtl gtl' in
-	Max (List.subtract UniverseLevel.equal gel'' gtl'',gtl'')
+let pr_uni = Universe.pr
+let is_small_univ = Universe.is_small
+
+let universe_level = Universe.level
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
-    { univ: UniverseLevel.t;
-      lt: UniverseLevel.t list;
-      le: UniverseLevel.t list;
-      rank: int }
+    { univ: Level.t;
+      lt: Level.t list;
+      le: Level.t list;
+      rank : int}
 
 let terminal u = {univ=u; lt=[]; le=[]; rank=0}
 
-(* A UniverseLevel.t is either an alias for another one, or a canonical one,
+(* A Level.t is either an alias for another one, or a canonical one,
    for which we know the universes that are above *)
 
 type univ_entry =
     Canonical of canonical_arc
-  | Equiv of UniverseLevel.t
+  | Equiv of Level.t
 
 
-type universes = univ_entry UniverseLMap.t
+type universes = univ_entry LMap.t
 
 let enter_equiv_arc u v g =
-  UniverseLMap.add u (Equiv v) g
+  LMap.add u (Equiv v) g
 
 let enter_arc ca g =
-  UniverseLMap.add ca.univ (Canonical ca) g
-
-(* The lower predicative level of the hierarchy that contains (impredicative)
-   Prop and singleton inductive types *)
-let type0m_univ = Max ([],[])
+  LMap.add ca.univ (Canonical ca) g
 
-let is_type0m_univ = function
-  | Max ([],[]) -> true
-  | _ -> false
+let is_type0m_univ = Universe.is_type0m
 
 (* The level of predicative Set *)
-let type0_univ = Atom UniverseLevel.Set
+let type0m_univ = Universe.type0m
+let type0_univ = Universe.type0
+let type1_univ = Universe.type1
 
-let is_type0_univ = function
-  | Atom UniverseLevel.Set -> true
-  | Max ([UniverseLevel.Set], []) -> msg_warning (str "Non canonical Set"); true
-  | u -> false
+let sup = Universe.sup
+let super = Universe.super
 
-let is_univ_variable = function
-  | Atom UniverseLevel.Set -> false
-  | Atom _ -> true
-  | _ -> false
+let is_type0_univ = Universe.is_type0
 
-(* When typing [Prop] and [Set], there is no constraint on the level,
-   hence the definition of [type1_univ], the type of [Prop] *)
+let is_univ_variable l = Universe.level l != None
 
-let type1_univ = Max ([], [UniverseLevel.Set])
+(* Every Level.t has a unique canonical arc representative *)
 
-let initial_universes = UniverseLMap.empty
-let is_initial_universes = UniverseLMap.is_empty
-
-(* Every UniverseLevel.t has a unique canonical arc representative *)
-
-(* repr : universes -> UniverseLevel.t -> canonical_arc *)
+(* repr : universes -> Level.t -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 
 let repr g u =
   let rec repr_rec u =
     let a =
-      try UniverseLMap.find u g
+      try LMap.find u g
       with Not_found -> anomaly ~label:"Univ.repr"
-	  (str "Universe" ++ spc () ++ pr_uni_level u ++ spc () ++ str "undefined")
+	  (str"Universe " ++ Level.pr u ++ str" undefined")
     in
     match a with
       | Equiv v -> repr_rec v
@@ -262,7 +854,7 @@ let can g = List.map (repr g)
 
 let safe_repr g u =
   let rec safe_repr_rec u =
-    match UniverseLMap.find u g with
+    match LMap.find u g with
       | Equiv v -> safe_repr_rec v
       | Canonical arc -> arc
   in
@@ -286,7 +878,7 @@ let reprleq g arcu =
   searchrec [] arcu.le
 
 
-(* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *)
+(* between : Level.t -> canonical_arc -> canonical_arc list *)
 (* between u v = { w | u<=w<=v, w canonical }          *)
 (* between is the most costly operation *)
 
@@ -320,6 +912,7 @@ let between g arcu arcv =
  *)
 
 type constraint_type = Lt | Le | Eq
+
 type explanation = (constraint_type * universe) list
 
 let constraint_type_ord c1 c2 = match c1, c2 with
@@ -335,10 +928,10 @@ let constraint_type_ord c1 c2 = match c1, c2 with
    correspond to the universes in (direct) relation [rel] with it,
    make a list of canonical universe, updating the relation with
    the starting point (path stored in reverse order). *)
-let canp g (p:explanation) rel l : (canonical_arc * explanation) list =
-  List.map (fun u -> (repr g u, (rel,Atom u)::p)) l
+let canp g (p:explanation Lazy.t) rel l : (canonical_arc * explanation Lazy.t) list =
+  List.map (fun u -> (repr g u, lazy ((rel,Universe.make u):: Lazy.force p))) l
 
-type order = EQ | LT of explanation | LE of explanation | NLE
+type order = EQ | LT of explanation Lazy.t | LE of explanation Lazy.t | NLE
 
 (** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
 
@@ -375,14 +968,14 @@ let compare_neq strict g arcu arcv =
         | [] -> cmp c (arc :: lt_done) le_done lt_todo le_todo
         | u :: lt ->
           let arc = repr g u in
-          let p = (Lt, Atom u) :: p in
+          let p = lazy ((Lt, make u) :: Lazy.force p) in
           if arc == arcv then
             if strict then LT p else LE p
           else find ((arc, p) :: lt_todo) lt le
         end
       | u :: le ->
         let arc = repr g u in
-        let p = (Le, Atom u) :: p in
+        let p = lazy ((Le, make u) :: Lazy.force p) in
         if arc == arcv then
           if strict then LT p else LE p
         else find ((arc, p) :: lt_todo) lt le
@@ -402,21 +995,22 @@ let compare_neq strict g arcu arcv =
         let rec find lt_todo lt = match lt with
         | [] ->
           let fold accu u =
-            let node = (repr g u, (Le, Atom u) :: p) in
+            let p = lazy ((Le, make u) :: Lazy.force p) in
+            let node = (repr g u, p) in
             node :: accu
           in
           let le_new = List.fold_left fold le_todo arc.le in
           cmp c lt_done (arc :: le_done) lt_todo le_new
         | u :: lt ->
           let arc = repr g u in
-          let p = (Lt, Atom u) :: p in
+          let p = lazy ((Lt, make u) :: Lazy.force p) in
           if arc == arcv then
             if strict then LT p else LE p
           else find ((arc, p) :: lt_todo) lt
         in
         find [] arc.lt
   in
-  cmp NLE [] [] [] [arcu, []]
+  cmp NLE [] [] [] [arcu, Lazy.lazy_from_val []]
 
 let compare g arcu arcv =
   if arcu == arcv then EQ else compare_neq true g arcu arcv
@@ -456,50 +1050,80 @@ let check_smaller g strict u v =
   if strict then
     is_lt g arcu arcv
   else
-    arcu == snd (safe_repr g UniverseLevel.Set) || is_leq g arcu arcv
+    arcu == snd (safe_repr g Level.prop) || is_leq g arcu arcv
 
 (** Then, checks on universes *)
 
-type check_function = universes -> universe -> universe -> bool
+type 'a check_function = universes -> 'a -> 'a -> bool
+
+(* let equiv_list cmp l1 l2 = *)
+(*   let rec aux l1 l2 = *)
+(*     match l1 with *)
+(*     | [] -> l2 = [] *)
+(*     | hd :: tl1 -> *)
+(*       let rec aux' acc = function *)
+(* 	| hd' :: tl2 ->  *)
+(* 	  if cmp hd hd' then aux tl1 (acc @ tl2) *)
+(* 	  else aux' (hd' :: acc) tl2 *)
+(* 	| [] -> false *)
+(*       in aux' [] l2 *)
+(*   in aux l1 l2 *)
 
 let incl_list cmp l1 l2 =
-  List.for_all (fun x1 -> List.exists (fun x2 -> cmp x1 x2) l2) l1
+  Huniv.for_all (fun x1 -> Huniv.exists (fun x2 -> cmp x1 x2) l2) l1
 
 let compare_list cmp l1 l2 =
-  (l1 == l2)
-  || (incl_list cmp l1 l2 && incl_list cmp l2 l1)
+  (l1 == l2) || (* (equiv_list cmp l1 l2) *)
+  (incl_list cmp l1 l2 && incl_list cmp l2 l1)
+
+let check_equal_expr g x y =
+  x == y || (let (u, n) = Hunivelt.node x and (v, m) = Hunivelt.node y in 
+	       n = m && check_equal g u v)
 
 (** [check_eq] is also used in [Evd.set_eq_sort],
     hence [Evarconv] and [Unification]. In this case,
     it seems that the Atom/Max case may occur,
     hence a relaxed version. *)
 
-let gen_check_eq strict g u v =
-  match u,v with
-    | Atom ul, Atom vl -> check_equal g ul vl
-    | Max(ule,ult), Max(vle,vlt) ->
-        (* TODO: remove elements of lt in le! *)
-        compare_list (check_equal g) ule vle &&
-        compare_list (check_equal g) ult vlt
-    | _ ->
-      (* not complete! (Atom(u) = Max([u],[]) *)
-      if strict then anomaly (str "check_eq")
-      else false (* in non-strict mode, under-approximation *)
-
-let check_eq = gen_check_eq true
-let lax_check_eq = gen_check_eq false
+(* let gen_check_eq strict g u v = *)
+(*   match u,v with *)
+(*     | Atom ul, Atom vl -> check_equal g ul vl *)
+(*     | Max(ule,ult), Max(vle,vlt) -> *)
+(*         (\* TODO: remove elements of lt in le! *\) *)
+(*         compare_list (check_equal g) ule vle && *)
+(*         compare_list (check_equal g) ult vlt *)
+(*     | _ -> *)
+(*       (\* not complete! (Atom(u) = Max([u],[]) *\) *)
+(*       if strict then anomaly (str "check_eq") *)
+(*       else false (\* in non-strict mode, under-approximation *\) *)
+
+(* let check_eq = gen_check_eq true *)
+(* let lax_check_eq = gen_check_eq false *)
+let check_eq g u v =
+  compare_list (check_equal_expr g) u v
+let check_eq_level g u v = u == v || check_equal g u v
+let lax_check_eq = check_eq
+
+let check_smaller_expr g (u,n) (v,m) =
+  if n <= m then
+    check_smaller g false u v
+  else if n - m = 1 then
+    check_smaller g true u v
+  else false
+
+let exists_bigger g ul l =
+  Huniv.exists (fun ul' -> 
+    check_smaller_expr g (Hunivelt.node ul) (Hunivelt.node ul')) l
 
 let check_leq g u v =
-  match u,v with
-    | Atom ul, Atom vl -> check_smaller g false ul vl
-    | Max(le,lt), Atom vl ->
-        List.for_all (fun ul -> check_smaller g false ul vl) le &&
-        List.for_all (fun ul -> check_smaller g true ul vl) lt
-    | _ -> anomaly (str "check_leq")
+  u == v ||
+  match Universe.level u with
+  | Some l when Level.is_prop l -> true
+  | _ -> Huniv.for_all (fun ul -> exists_bigger g ul v) u
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
-(* setlt : UniverseLevel.t -> UniverseLevel.t -> reason -> unit *)
+(* setlt : Level.t -> Level.t -> reason -> unit *)
 (* forces u > v *)
 (* this is normally an update of u in g rather than a creation. *)
 let setlt g arcu arcv =
@@ -512,7 +1136,7 @@ let setlt_if (g,arcu) v =
   if is_lt g arcu arcv then g, arcu
   else setlt g arcu arcv
 
-(* setleq : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* setleq : Level.t -> Level.t -> unit *)
 (* forces u >= v *)
 (* this is normally an update of u in g rather than a creation. *)
 let setleq g arcu arcv =
@@ -526,7 +1150,7 @@ let setleq_if (g,arcu) v =
   if is_leq g arcu arcv then g, arcu
   else setleq g arcu arcv
 
-(* merge : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* merge : Level.t -> Level.t -> unit *)
 (* we assume  compare(u,v) = LE *)
 (* merge u v  forces u ~ v with repr u as canonical repr *)
 let merge g arcu arcv =
@@ -559,7 +1183,7 @@ let merge g arcu arcv =
   let g_arcu = List.fold_left setleq_if g_arcu w' in
   fst g_arcu
 
-(* merge_disc : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* merge_disc : Level.t -> Level.t -> unit *)
 (* we assume  compare(u,v) = compare(v,u) = NLE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
 let merge_disc g arc1 arc2 =
@@ -579,36 +1203,37 @@ let merge_disc g arc1 arc2 =
 (* Universe inconsistency: error raised when trying to enforce a relation
    that would create a cycle in the graph of universes. *)
 
-exception UniverseInconsistency of
-  constraint_type * universe * universe * explanation
+type univ_inconsistency = constraint_type * universe * universe * explanation
+
+exception UniverseInconsistency of univ_inconsistency
 
 let error_inconsistency o u v (p:explanation) =
-  raise (UniverseInconsistency (o,Atom u,Atom v,p))
+  raise (UniverseInconsistency (o,make u,make v,p))
 
-(* enforce_univ_leq : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
   let g,arcu = safe_repr g u in
   let g,arcv = safe_repr g v in
   if is_leq g arcu arcv then g
   else match compare g arcv arcu with
-    | LT p -> error_inconsistency Le u v (List.rev p)
+    | LT p -> error_inconsistency Le u v (List.rev (Lazy.force p))
     | LE _ -> merge g arcv arcu
     | NLE -> fst (setleq g arcu arcv)
     | EQ -> anomaly (Pp.str "Univ.compare")
 
-(* enforc_univ_eq : UniverseLevel.t -> UniverseLevel.t -> unit *)
+(* enforc_univ_eq : Level.t -> Level.t -> unit *)
 (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
 let enforce_univ_eq u v g =
   let g,arcu = safe_repr g u in
   let g,arcv = safe_repr g v in
   match compare g arcu arcv with
     | EQ -> g
-    | LT p -> error_inconsistency Eq u v (List.rev p)
+    | LT p -> error_inconsistency Eq v u (List.rev (Lazy.force p))
     | LE _ -> merge g arcu arcv
     | NLE ->
 	(match compare g arcv arcu with
-           | LT p -> error_inconsistency Eq u v (List.rev p)
+           | LT p -> error_inconsistency Eq u v (List.rev (Lazy.force p))
            | LE _ -> merge g arcv arcu
            | NLE -> merge_disc g arcu arcv
            | EQ -> anomaly (Pp.str "Univ.compare"))
@@ -620,16 +1245,20 @@ let enforce_univ_lt u v g =
   match compare g arcu arcv with
     | LT _ -> g
     | LE _ -> fst (setlt g arcu arcv)
-    | EQ -> error_inconsistency Lt u v [(Eq,Atom v)]
+    | EQ -> error_inconsistency Lt u v [(Eq,make v)]
     | NLE ->
       (match compare_neq false g arcv arcu with
 	  NLE -> fst (setlt g arcu arcv)
 	| EQ -> anomaly (Pp.str "Univ.compare")
-	| (LE p|LT p) -> error_inconsistency Lt u v (List.rev p))
+	| (LE p|LT p) -> error_inconsistency Lt u v (List.rev (Lazy.force p)))
 
-(* Constraints and sets of consrtaints. *)
+let empty_universes = LMap.empty
+let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty
+let is_initial_universes g = LMap.equal (==) g initial_universes
 
-type univ_constraint = UniverseLevel.t * constraint_type * UniverseLevel.t
+(* Constraints and sets of constraints. *)    
+
+type univ_constraint = Level.t * constraint_type * Level.t
 
 let enforce_constraint cst g =
   match cst with
@@ -637,6 +1266,14 @@ let enforce_constraint cst g =
     | (u,Le,v) -> enforce_univ_leq u v g
     | (u,Eq,v) -> enforce_univ_eq u v g
 
+let pr_constraint_type op = 
+  let op_str = match op with
+    | Lt -> " < "
+    | Le -> " <= "
+    | Eq -> " = "
+  in str op_str
+
+
 module UConstraintOrd =
 struct
   type t = univ_constraint
@@ -644,51 +1281,566 @@ struct
     let i = constraint_type_ord c c' in
     if not (Int.equal i 0) then i
     else
-      let i' = UniverseLevel.compare u u' in
+      let i' = Level.compare u u' in
       if not (Int.equal i' 0) then i'
-      else UniverseLevel.compare v v'
+      else Level.compare v v'
 end
 
-module Constraint = Set.Make(UConstraintOrd)
+module Constraint = 
+struct 
+  module S = Set.Make(UConstraintOrd)
+  include S
 
-type constraints = Constraint.t
+  let pr c =
+    fold (fun (u1,op,u2) pp_std ->
+      pp_std ++  Level.pr u1 ++ pr_constraint_type op ++
+	Level.pr u2 ++ fnl () )  c (str "")
+
+end
 
 let empty_constraint = Constraint.empty
 let is_empty_constraint = Constraint.is_empty
+let union_constraint = Constraint.union
 let eq_constraint = Constraint.equal
 
-let union_constraints = Constraint.union
+type constraints = Constraint.t
+
+module Hconstraint =
+  Hashcons.Make(
+    struct
+      type t = univ_constraint
+      type u = universe_level -> universe_level
+      let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
+      let equal (l1,k,l2) (l1',k',l2') =
+	l1 == l1' && k == k' && l2 == l2'
+      let hash = Hashtbl.hash
+    end)
+
+module Hconstraints =
+  Hashcons.Make(
+    struct
+      type t = constraints
+      type u = univ_constraint -> univ_constraint
+      let hashcons huc s =
+	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
+      let equal s s' =
+	List.for_all2eq (==)
+	  (Constraint.elements s)
+	  (Constraint.elements s')
+      let hash = Hashtbl.hash
+    end)
+
+let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Level.hcons
+let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint
+
+type universe_constraint_type = ULe | UEq | ULub
+
+type universe_constraint = universe * universe_constraint_type * universe
+module UniverseConstraints = struct
+  module S = Set.Make(
+  struct 
+    type t = universe_constraint
+
+    let compare_type c c' =
+      match c, c' with
+      | ULe, ULe -> 0
+      | ULe, _ -> -1
+      | _, ULe -> 1
+      | UEq, UEq -> 0
+      | UEq, _ -> -1
+      | ULub, ULub -> 0
+      | ULub, _ -> 1
+      
+    let compare (u,c,v) (u',c',v') =
+      let i = compare_type c c' in
+	if Int.equal i 0 then
+	  let i' = Universe.compare u u' in
+	    if Int.equal i' 0 then Universe.compare v v'
+	    else 
+	      if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0
+	      else i'
+	else i
+  end)
+  
+  include S
+  
+  let add (l,d,r as cst) s = 
+    if Universe.eq l r then s
+    else add cst s
+
+  let tr_dir = function
+    | ULe -> Le
+    | UEq -> Eq
+    | ULub -> Eq
+
+  let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ "
+
+  let pr c =
+    fold (fun (u1,op,u2) pp_std ->
+	pp_std ++ Universe.pr u1 ++ str (op_str op) ++
+	Universe.pr u2 ++ fnl ()) c (str "")
+
+  let equal x y = 
+    x == y || equal x y
 
-type constraint_function =
-    universe -> universe -> constraints -> constraints
+end
+
+type universe_constraints = UniverseConstraints.t
+type 'a universe_constrained = 'a * universe_constraints
+
+(** A value with universe constraints. *)
+type 'a constrained = 'a * constraints
+
+let level_subst_of f = 
+  fun l -> 
+    try let u = f l in 
+	  match Universe.level u with
+	  | None -> l
+	  | Some l -> l
+    with Not_found -> l
+     
+module Instance = struct
+  type t = Level.t array
+
+  module HInstance =
+    Hashcons.Make(
+      struct
+	type _t = t
+	type t = _t
+	type u = Level.t -> Level.t
+	let hashcons huniv a = 
+	  CArray.smartmap huniv a
+
+	let equal t1 t2 =
+	  t1 == t2 ||
+	    (Int.equal (Array.length t1) (Array.length t2) &&
+	       let rec aux i =
+		 (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
+	       in aux 0)
+
+	let hash = Hashtbl.hash
+    end)
+
+  let hcons_instance = Hashcons.simple_hcons HInstance.generate Level.hcons
+
+  let hcons = hcons_instance
+  let empty = [||]
+  let is_empty x = Int.equal (Array.length x) 0
+
+  let eq t u = t == u || CArray.for_all2 Level.eq t u
+
+  let of_array a = a
+  let to_array a = a
+    
+  let eqeq t1 t2 =
+    t1 == t2 ||
+      (Int.equal (Array.length t1) (Array.length t2) &&
+	 let rec aux i =
+	   (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
+	 in aux 0)
+
+  let subst_fn fn t = CArray.smartmap fn t
+  let subst s t = CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+
+  let levels x = LSet.of_array x
+
+  let pr =
+    prvect_with_sep spc Level.pr
+
+  let append x y =
+    if Array.length x = 0 then y
+    else if Array.length y = 0 then x 
+    else Array.append x y
+
+  let max_level i = 
+    if Array.is_empty i then 0
+    else
+      let l = CArray.last i in
+	match l with
+	| Level.Level (i,_) -> i
+	| _ -> assert false
+
+  let check_eq g t1 t2 =
+    t1 == t2 ||
+      (Int.equal (Array.length t1) (Array.length t2) &&
+	 let rec aux i =
+	   (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
+	 in aux 0)
+
+end
+
+type universe_instance = Instance.t
+
+type 'a puniverses = 'a * Instance.t
+let out_punivs (x, y) = x
+let in_punivs x = (x, Instance.empty)
+
+(** A context of universe levels with universe constraints,
+    representiong local universe variables and constraints *)
+
+module UContext =
+struct
+  type t = Instance.t constrained
+
+  let make x = x
+
+  (** Universe contexts (variables as a list) *)
+  let empty = (Instance.empty, Constraint.empty)
+  let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
+
+  let pr (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      Instance.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst)
+
+  let hcons (univs, cst) =
+    (Instance.hcons univs, hcons_constraints cst)
+
+  let instance (univs, cst) = univs
+  let constraints (univs, cst) = cst
+
+  let union (univs, cst) (univs', cst') =
+    Instance.append univs univs', Constraint.union cst cst'
+end
+
+type universe_context = UContext.t
+let hcons_universe_context = UContext.hcons
+
+(** A set of universes with universe constraints.
+    We linearize the set to a list after typechecking. 
+    Beware, representation could change.
+*)
+
+module ContextSet =
+struct
+  type t = universe_set constrained
+
+  let empty = (LSet.empty, Constraint.empty)
+  let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
+
+  let of_context (ctx,cst) =
+    (Instance.levels ctx, cst)
+
+  let of_set s = (s, Constraint.empty)
+  let singleton l = of_set (LSet.singleton l)
+  let of_instance i = of_set (Instance.levels i)
+
+  let union (univs, cst) (univs', cst') =
+    LSet.union univs univs', Constraint.union cst cst'
+
+  let diff (univs, cst) (univs', cst') =
+    LSet.diff univs univs', Constraint.diff cst cst'
+
+  let add_constraints (univs, cst) cst' =
+    univs, Constraint.union cst cst'
+
+  let add_universes univs ctx =
+    union (of_instance univs) ctx
+
+  let to_context (ctx, cst) =
+    (Array.of_list (LSet.elements ctx), cst)
+
+  let of_context (ctx, cst) =
+    (Instance.levels ctx, cst)
+
+  let pr (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      LSet.pr univs ++ str " |= " ++ v 1 (Constraint.pr cst)
+
+  let constraints (univs, cst) = cst
+  let levels (univs, cst) = univs
+
+end
+
+type universe_context_set = ContextSet.t
+
+(** A value in a universe context (resp. context set). *)
+type 'a in_universe_context = 'a * universe_context
+type 'a in_universe_context_set = 'a * universe_context_set
+
+(** A universe level substitution, note that no algebraic universes are
+    involved *)
+type universe_level_subst = universe_level universe_map
+
+(** A full substitution might involve algebraic universes *)
+type universe_subst = universe universe_map
+
+(** Pretty-printing *)
+let pr_constraints = Constraint.pr
+
+let pr_universe_context = UContext.pr
+
+let pr_universe_context_set = ContextSet.pr
+
+let pr_universe_subst = 
+  LMap.pr (fun u -> str" := " ++ Universe.pr u ++ spc ())
+
+let pr_universe_level_subst = 
+  LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ())
+
+let constraints_of (_, cst) = cst
+
+let constraint_depend (l,d,r) u =
+  Level.eq l u || Level.eq l r
+
+let constraint_depend_list (l,d,r) us =
+  List.mem l us || List.mem r us
+
+let constraints_depend cstr us = 
+  Constraint.exists (fun c -> constraint_depend_list c us) cstr
+
+let remove_dangling_constraints dangling cst =
+  Constraint.fold (fun (l,d,r as cstr) cst' -> 
+    if List.mem l dangling || List.mem r dangling then cst'
+    else
+      (** Unnecessary constraints Prop <= u *)
+      if Level.eq l Level.prop && d == Le then cst'
+      else Constraint.add cstr cst') cst Constraint.empty
+  
+let check_context_subset (univs, cst) (univs', cst') =
+  let newunivs, dangling = List.partition (fun u -> LSet.mem u univs) (Array.to_list univs') in
+    (* Some universe variables that don't appear in the term 
+       are still mentionned in the constraints. This is the 
+       case for "fake" universe variables that correspond to +1s. *)
+    (* if not (CList.is_empty dangling) then  *)
+    (*   todo ("A non-empty set of inferred universes do not appear in the term or type"); *)
+      (* (not (constraints_depend cst' dangling));*)
+    (* TODO: check implication *)
+  (** Remove local universes that do not appear in any constraint, they
+      are really entirely parametric. *)
+  (* let newunivs, dangling' = List.partition (fun u -> constraints_depend cst [u]) newunivs in *)
+  let cst' = remove_dangling_constraints dangling cst in
+    Array.of_list newunivs, cst'
+
+(** Substitutions. *)
+
+let make_universe_subst inst (ctx, csts) = 
+  try Array.fold_left2 (fun acc c i -> LMap.add c (Universe.make i) acc)
+        LMap.empty ctx inst
+  with Invalid_argument _ -> 
+    anomaly (Pp.str "Mismatched instance and context when building universe substitution")
+
+let empty_subst = LMap.empty
+let is_empty_subst = LMap.is_empty
+
+let empty_level_subst = LMap.empty
+let is_empty_level_subst = LMap.is_empty
+
+(** Substitution functions *)
+
+(** With level to level substitutions. *)
+let subst_univs_level_level subst l =
+  try LMap.find l subst
+  with Not_found -> l
+
+let rec normalize_univs_level_level subst l =
+  try 
+    let l' = LMap.find l subst in
+      normalize_univs_level_level subst l'
+  with Not_found -> l
+
+let subst_univs_level_fail subst l =
+  try match Universe.level (subst l) with 
+  | Some l' -> l'
+  | None -> l
+  with Not_found -> l
+
+let rec subst_univs_level_universe subst u =
+  let u' = Universe.smartmap (Universe.Expr.map (subst_univs_level_level subst)) u in
+    if u == u' then u
+    else Universe.sort u'
+	
+let subst_univs_level_constraint subst (u,d,v) =
+  let u' = subst_univs_level_level subst u 
+  and v' = subst_univs_level_level subst v in
+    if d != Lt && Level.eq u' v' then None
+    else Some (u',d,v')
+
+let subst_univs_level_constraints subst csts =
+  Constraint.fold 
+    (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
+    csts Constraint.empty 
+
+(* let subst_univs_level_constraint_key = Profile.declare_profile "subst_univs_level_constraint";; *)
+(* let subst_univs_level_constraint = *)
+(*   Profile.profile2 subst_univs_level_constraint_key subst_univs_level_constraint *)
+
+(** With level to universe substitutions. *)
+type universe_subst_fn = universe_level -> universe
+
+let make_subst subst = fun l -> LMap.find l subst
+
+let subst_univs_level fn l = 
+  try fn l
+  with Not_found -> make l
+
+let subst_univs_expr_opt fn (l,n) =
+  try Some (Universe.addn n (fn l))
+  with Not_found -> None
+
+let subst_univs_universe fn ul =
+  let subst, nosubst = 
+    Universe.Huniv.fold (fun u (subst,nosubst) -> 
+      match subst_univs_expr_opt fn (Hunivelt.node u) with
+      | Some a' -> (a' :: subst, nosubst)
+      | None -> (subst, u :: nosubst))
+    ul ([], [])
+  in 
+    if CList.is_empty subst then ul
+    else 
+      let substs = 
+	List.fold_left Universe.merge_univs Universe.empty subst
+      in
+	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
+	  substs nosubst
+
+let subst_univs_constraint fn (u,d,v) =
+  let u' = subst_univs_level fn u and v' = subst_univs_level fn v in
+    if d != Lt && Universe.eq u' v' then None
+    else Some (u',d,v')
+
+let subst_univs_universe_constraint fn (u,d,v) =
+  let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+    if Universe.eq u' v' then None
+    else Some (u',d,v')
+
+(** Constraint functions. *)
+
+type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
 let constraint_add_leq v u c =
-  (* We just discard trivial constraints like Set<=u or u<=u *)
-  if UniverseLevel.equal v UniverseLevel.Set || UniverseLevel.equal v u then c
-  else Constraint.add (v,Le,u) c
+  (* We just discard trivial constraints like u<=u *)
+  if Expr.eq v u then c
+  else 
+    match v, u with
+    | (x,n), (y,m) -> 
+    let j = m - n in
+      if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
+	Constraint.add (x,Lt,y) c
+      else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
+	if Level.eq x y then (* u+(k+1) <= u *)
+	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, []))
+	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
+      else if j = 0 then
+	Constraint.add (x,Le,y) c
+      else (* j >= 1 *) (* m = n + k, u <= v+k *)
+	if Level.eq x y then c (* u <= u+k, trivial *)
+	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
+	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
+	  
+let check_univ_eq u v = Universe.eq u v
+
+let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
+
+let check_univ_leq u v = 
+  Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
-  match u, v with
-  | Atom u, Atom v -> constraint_add_leq u v c
-  | Max (gel,gtl), Atom v ->
-      let d = List.fold_right (fun u -> constraint_add_leq u v) gel c in
-      List.fold_right (fun u -> Constraint.add (u,Lt,v)) gtl d
-  | _ -> anomaly (Pp.str "A universe bound can only be a variable")
+  match Huniv.node v with
+  | Universe.Huniv.Cons (v, n) when Universe.is_empty n -> 
+    Universe.Huniv.fold (fun u -> constraint_add_leq (Hunivelt.node u) (Hunivelt.node v)) u c
+  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+
+let enforce_leq u v c =
+  if check_univ_leq u v then c
+  else enforce_leq u v c
+
+let enforce_eq_level u v c =
+  (* We discard trivial constraints like u=u *)
+  if Level.eq u v then c 
+  else if Level.apart u v then
+    error_inconsistency Eq u v []
+  else Constraint.add (u,Eq,v) c
 
 let enforce_eq u v c =
-  match (u,v) with
-    | Atom u, Atom v ->
-      (* We discard trivial constraints like u=u *)
-      if UniverseLevel.equal u v then c else Constraint.add (u,Eq,v) c
+  match Universe.level u, Universe.level v with
+    | Some u, Some v -> enforce_eq_level u v c
     | _ -> anomaly (Pp.str "A universe comparison can only happen between variables")
 
+let enforce_eq u v c =
+  if check_univ_eq u v then c
+  else enforce_eq u v c
+
+let enforce_leq_level u v c =
+  if Level.eq u v then c else Constraint.add (u,Le,v) c
+
+let enforce_eq_instances = CArray.fold_right2 enforce_eq_level 
+
+type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
+
+let enforce_eq_instances_univs strict t1 t2 c = 
+  let d = if strict then ULub else UEq in
+    CArray.fold_right2 (fun x y -> UniverseConstraints.add (Universe.make x, d, Universe.make y))
+      t1 t2 c
+
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
 
+(* let merge_constraints_key = Profile.declare_profile "merge_constraints";; *)
+(* let merge_constraints = Profile.profile2 merge_constraints_key merge_constraints *)
+
+let check_constraint g (l,d,r) =
+  match d with
+  | Eq -> check_equal g l r
+  | Le -> check_smaller g false l r
+  | Lt -> check_smaller g true l r
+
+let check_constraints c g =
+  Constraint.for_all (check_constraint g) c
+
+(* let check_constraints_key = Profile.declare_profile "check_constraints";; *)
+(* let check_constraints = *)
+(*   Profile.profile2 check_constraints_key check_constraints *)
+
+let enforce_univ_constraint (u,d,v) =
+  match d with
+  | Eq -> enforce_eq u v
+  | Le -> enforce_leq u v
+  | Lt -> enforce_leq (super u) v
+
+let subst_univs_constraints subst csts =
+  Constraint.fold 
+    (fun c -> Option.fold_right enforce_univ_constraint (subst_univs_constraint subst c))
+    csts Constraint.empty 
+
+(* let subst_univs_constraints_key = Profile.declare_profile "subst_univs_constraints";; *)
+(* let subst_univs_constraints = *)
+(*   Profile.profile2 subst_univs_constraints_key subst_univs_constraints *)
+
+let subst_univs_universe_constraints subst csts =
+  UniverseConstraints.fold 
+    (fun c -> Option.fold_right UniverseConstraints.add (subst_univs_universe_constraint subst c))
+    csts UniverseConstraints.empty 
+
+(* let subst_univs_universe_constraints_key = Profile.declare_profile "subst_univs_universe_constraints";; *)
+(* let subst_univs_universe_constraints = *)
+(*   Profile.profile2 subst_univs_universe_constraints_key subst_univs_universe_constraints *)
+
+(** Substitute instance inst for ctx in csts *)
+let instantiate_univ_context subst (_, csts) = 
+  subst_univs_constraints (make_subst subst) csts
+
+let check_consistent_constraints (ctx,cstrs) cstrs' =
+  (* TODO *) ()
+
+let to_constraints g s = 
+  let rec tr (x,d,y) acc =
+    let add l d l' acc = Constraint.add (l,UniverseConstraints.tr_dir d,l') acc in
+      match Universe.level x, d, Universe.level y with
+      | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc
+      | _, ULe, Some l' -> enforce_leq x y acc
+      | _, ULub, _ -> acc
+      | _, d, _ -> 
+	let f = if d == ULe then check_leq else check_eq in
+	  if f g x y then acc else 
+	    raise (Invalid_argument 
+		   "to_constraints: non-trivial algebraic constraint between universes")
+  in UniverseConstraints.fold tr s Constraint.empty
+     
+
 (* Normalization *)
 
 let lookup_level u g =
-  try Some (UniverseLMap.find u g) with Not_found -> None
+  try Some (LMap.find u g) with Not_found -> None
 
 (** [normalize_universes g] returns a graph where all edges point
     directly to the canonical representent of their target. The output
@@ -702,20 +1854,20 @@ let normalize_universes g =
     | Some x -> x, cache
     | None -> match Lazy.force arc with
     | None ->
-      u, UniverseLMap.add u u cache
+      u, LMap.add u u cache
     | Some (Canonical {univ=v; lt=_; le=_}) ->
-      v, UniverseLMap.add u v cache
+      v, LMap.add u v cache
     | Some (Equiv v) ->
       let v, cache = visit v (lazy (lookup_level v g)) cache in
-      v, UniverseLMap.add u v cache
+      v, LMap.add u v cache
   in
-  let cache = UniverseLMap.fold
+  let cache = LMap.fold
     (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache))
-    g UniverseLMap.empty
+    g LMap.empty
   in
-  let repr x = UniverseLMap.find x cache in
+  let repr x = LMap.find x cache in
   let lrepr us = List.fold_left
-    (fun e x -> UniverseLSet.add (repr x) e) UniverseLSet.empty us
+    (fun e x -> LSet.add (repr x) e) LSet.empty us
   in
   let canonicalize u = function
     | Equiv _ -> Equiv (repr u)
@@ -723,24 +1875,24 @@ let normalize_universes g =
       assert (u == v);
       (* avoid duplicates and self-loops *)
       let lt = lrepr lt and le = lrepr le in
-      let le = UniverseLSet.filter
-        (fun x -> x != u && not (UniverseLSet.mem x lt)) le
+      let le = LSet.filter
+        (fun x -> x != u && not (LSet.mem x lt)) le
       in
-      UniverseLSet.iter (fun x -> assert (x != u)) lt;
+      LSet.iter (fun x -> assert (x != u)) lt;
       Canonical {
         univ = v;
-        lt = UniverseLSet.elements lt;
-        le = UniverseLSet.elements le;
+        lt = LSet.elements lt;
+        le = LSet.elements le;
 	rank = rank
       }
   in
-  UniverseLMap.mapi canonicalize g
+  LMap.mapi canonicalize g
 
 (** [check_sorted g sorted]: [g] being a universe graph, [sorted]
     being a map to levels, checks that all constraints in [g] are
     satisfied in [sorted]. *)
 let check_sorted g sorted =
-  let get u = try UniverseLMap.find u sorted with
+  let get u = try LMap.find u sorted with
     | Not_found -> assert false
   in
   let iter u arc =
@@ -751,7 +1903,7 @@ let check_sorted g sorted =
       List.iter (fun v -> assert (lu <= get v)) le;
       List.iter (fun v -> assert (lu < get v)) lt
   in
-  UniverseLMap.iter iter g
+  LMap.iter iter g
 
 (**
   Bellman-Ford algorithm with a few customizations:
@@ -765,7 +1917,7 @@ let bellman_ford bottom g =
   | None -> ()
   | Some _ -> assert false
   in
-  let ( << ) a b = match a, b with
+  let ( <? ) a b = match a, b with
     | _, None -> true
     | None, _ -> false
     | Some x, Some y -> (x : int) < y
@@ -774,38 +1926,38 @@ let bellman_ford bottom g =
     | Some x -> Some (x-y)
   and push u x m = match x with
     | None -> m
-    | Some y -> UniverseLMap.add u y m
+    | Some y -> LMap.add u y m
   in
   let relax u v uv distances =
     let x = lookup_level u distances ++ uv in
-    if x << lookup_level v distances then push v x distances
+    if x <? lookup_level v distances then push v x distances
     else distances
   in
-  let init = UniverseLMap.add bottom 0 UniverseLMap.empty in
-  let vertices = UniverseLMap.fold (fun u arc res ->
-    let res = UniverseLSet.add u res in
+  let init = LMap.add bottom 0 LMap.empty in
+  let vertices = LMap.fold (fun u arc res ->
+    let res = LSet.add u res in
     match arc with
-      | Equiv e -> UniverseLSet.add e res
+      | Equiv e -> LSet.add e res
       | Canonical {univ=univ; lt=lt; le=le} ->
         assert (u == univ);
-        let add res v = UniverseLSet.add v res in
+        let add res v = LSet.add v res in
         let res = List.fold_left add res le in
         let res = List.fold_left add res lt in
-        res) g UniverseLSet.empty
+        res) g LSet.empty
   in
   let g =
     let node = Canonical {
       univ = bottom;
       lt = [];
-      le = UniverseLSet.elements vertices;
+      le = LSet.elements vertices;
       rank = 0
-    } in UniverseLMap.add bottom node g
+    } in LMap.add bottom node g
   in
   let rec iter count accu =
     if count <= 0 then
       accu
     else
-      let accu = UniverseLMap.fold (fun u arc res -> match arc with
+      let accu = LMap.fold (fun u arc res -> match arc with
         | Equiv e -> relax e u 0 (relax u e 0 res)
         | Canonical {univ=univ; lt=lt; le=le} ->
           assert (u == univ);
@@ -814,16 +1966,16 @@ let bellman_ford bottom g =
           res) g accu
       in iter (count-1) accu
   in
-  let distances = iter (UniverseLSet.cardinal vertices) init in
-  let () = UniverseLMap.iter (fun u arc ->
+  let distances = iter (LSet.cardinal vertices) init in
+  let () = LMap.iter (fun u arc ->
     let lu = lookup_level u distances in match arc with
       | Equiv v ->
         let lv = lookup_level v distances in
-        assert (not (lu << lv) && not (lv << lu))
+        assert (not (lu <? lv) && not (lv <? lu))
       | Canonical {univ=univ; lt=lt; le=le} ->
         assert (u == univ);
-        List.iter (fun v -> assert (not (lu ++ 0 << lookup_level v distances))) le;
-        List.iter (fun v -> assert (not (lu ++ 1 << lookup_level v distances))) lt) g
+        List.iter (fun v -> assert (not (lu ++ 0 <? lookup_level v distances))) le;
+        List.iter (fun v -> assert (not (lu ++ 1 <? lookup_level v distances))) lt) g
   in distances
 
 (** [sort_universes g] builds a map from universes in [g] to natural
@@ -837,23 +1989,23 @@ let bellman_ford bottom g =
 let sort_universes orig =
   let mp = Names.DirPath.make [Names.Id.of_string "Type"] in
   let rec make_level accu g i =
-    let type0 = UniverseLevel.Level (i, mp) in
+    let type0 = Level.make mp i in
     let distances = bellman_ford type0 g in
-    let accu, continue = UniverseLMap.fold (fun u x (accu, continue) ->
+    let accu, continue = LMap.fold (fun u x (accu, continue) ->
       let continue = continue || x < 0 in
       let accu =
-        if Int.equal x 0 && u != type0 then UniverseLMap.add u i accu
+        if Int.equal x 0 && u != type0 then LMap.add u i accu
         else accu
       in accu, continue) distances (accu, false)
     in
-    let filter x = not (UniverseLMap.mem x accu) in
+    let filter x = not (LMap.mem x accu) in
     let push g u =
-      if UniverseLMap.mem u g then g else UniverseLMap.add u (Equiv u) g
+      if LMap.mem u g then g else LMap.add u (Equiv u) g
     in
-    let g = UniverseLMap.fold (fun u arc res -> match arc with
+    let g = LMap.fold (fun u arc res -> match arc with
       | Equiv v as x ->
         begin match filter u, filter v with
-          | true, true -> UniverseLMap.add u x res
+          | true, true -> LMap.add u x res
           | true, false -> push res u
           | false, true -> push res v
           | false, false -> res
@@ -863,24 +2015,24 @@ let sort_universes orig =
         if filter u then
           let lt = List.filter filter lt in
           let le = List.filter filter le in
-          UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le; rank=r}) res
+          LMap.add u (Canonical {univ=u; lt=lt; le=le; rank=r}) res
         else
           let res = List.fold_left (fun g u -> if filter u then push g u else g) res lt in
           let res = List.fold_left (fun g u -> if filter u then push g u else g) res le in
-          res) g UniverseLMap.empty
+          res) g LMap.empty
     in
     if continue then make_level accu g (i+1) else i, accu
   in
-  let max, levels = make_level UniverseLMap.empty orig 0 in
+  let max, levels = make_level LMap.empty orig 0 in
   (* defensively check that the result makes sense *)
   check_sorted orig levels;
-  let types = Array.init (max+1) (fun x -> UniverseLevel.Level (x, mp)) in
-  let g = UniverseLMap.map (fun x -> Equiv types.(x)) levels in
+  let types = Array.init (max+1) (fun x -> Level.make mp x) in
+  let g = LMap.map (fun x -> Equiv types.(x)) levels in
   let g =
     let rec aux i g =
       if i < max then
         let u = types.(i) in
-        let g = UniverseLMap.add u (Canonical {
+        let g = LMap.add u (Canonical {
           univ = u;
           le = [];
           lt = [types.(i+1)];
@@ -893,26 +2045,19 @@ let sort_universes orig =
 (**********************************************************************)
 (* Tools for sort-polymorphic inductive types                         *)
 
-(* Temporary inductive type levels *)
-
-let fresh_local_univ, set_remote_fresh_local_univ =
-  RemoteCounter.new_counter ~name:"local_univ" 0 ~incr:((+) 1)
-    ~build:(fun n -> Atom (UniverseLevel.Level (n, Names.DirPath.empty)))
-
 (* Miscellaneous functions to remove or test local univ assumed to
    occur only in the le constraints *)
 
-let make_max = function
-  | ([u],[]) -> Atom u
-  | (le,lt) -> Max (le,lt)
-
-let remove_large_constraint u = function
-  | Atom u' as x -> if UniverseLevel.equal u u' then Max ([],[]) else x
-  | Max (le,lt) -> make_max (List.remove UniverseLevel.equal u le,lt)
+let remove_large_constraint u v min = 
+  match Universe.level v with
+  | Some u' -> if Level.eq u u' then min else v
+  | None -> Huniv.remove (Hunivelt.make (Universe.Expr.make u)) v
 
-let is_direct_constraint u = function
-  | Atom u' -> UniverseLevel.equal u u'
-  | Max (le,lt) -> List.mem_f UniverseLevel.equal u le
+(* [is_direct_constraint u v] if level [u] is a member of universe [v] *)
+let is_direct_constraint u v =
+  match Universe.level v with
+  | Some u' -> Level.eq u u'
+  | None -> Huniv.mem (Hunivelt.make (Universe.Expr.make u)) v
 
 (*
    Solve a system of universe constraint of the form
@@ -932,29 +2077,31 @@ let is_direct_sort_constraint s v = match s with
   | Some u -> is_direct_constraint u v
   | None -> false
 
-let solve_constraints_system levels level_bounds =
+let solve_constraints_system levels level_bounds level_min =
   let levels =
-    Array.map (Option.map (function Atom u -> u | _ -> anomaly (Pp.str "expects Atom")))
+    Array.map (Option.map (fun u -> match level u with Some u -> u | _ -> anomaly (Pp.str"expects Atom")))
       levels in
   let v = Array.copy level_bounds in
   let nind = Array.length v in
   for i=0 to nind-1 do
     for j=0 to nind-1 do
       if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
-	v.(i) <- sup v.(i) level_bounds.(j)
+	(v.(i) <- Universe.sup v.(i) level_bounds.(j);
+	 level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
     done;
     for j=0 to nind-1 do
       match levels.(j) with
-      | Some u -> v.(i) <- remove_large_constraint u v.(i)
+      | Some u -> v.(i) <- remove_large_constraint u v.(i) level_min.(i)
       | None -> ()
     done
   done;
   v
 
 let subst_large_constraint u u' v =
-  match u with
-  | Atom u ->
-      if is_direct_constraint u v then sup u' (remove_large_constraint u v)
+  match level u with
+  | Some u ->
+      if is_direct_constraint u v then 
+	Universe.sup u' (remove_large_constraint u v type0m_univ)
       else v
   | _ ->
       anomaly (Pp.str "expect a universe level")
@@ -963,21 +2110,30 @@ let subst_large_constraints =
   List.fold_right (fun (u,u') -> subst_large_constraint u u')
 
 let no_upper_constraints u cst =
-  match u with
-  | Atom u ->
-    let test (u1, _, _) = not (UniverseLevel.equal u1 u) in
+  match level u with
+  | Some u ->
+    let test (u1, _, _) =
+      not (Int.equal (Level.compare u1 u) 0) in
     Constraint.for_all test cst
-  | Max _ -> anomaly (Pp.str "no_upper_constraints")
+  | _ -> anomaly (Pp.str "no_upper_constraints")
 
 (* Is u mentionned in v (or equals to v) ? *)
 
-let level_list_mem u l = List.mem_f UniverseLevel.equal u l
-
 let univ_depends u v =
-  match u, v with
-    | Atom u, Atom v -> UniverseLevel.equal u v
-    | Atom u, Max (gel,gtl) -> level_list_mem u gel || level_list_mem u gtl
-    | _ -> anomaly (Pp.str "univ_depends given a non-atomic 1st arg")
+  match atom u with
+    | Some u -> Huniv.mem u v
+    | _ -> anomaly (Pp.str"univ_depends given a non-atomic 1st arg")
+
+let constraints_of_universes g =
+  let constraints_of u v acc =
+    match v with
+    | Canonical {univ=u; lt=lt; le=le} ->
+      let acc = List.fold_left (fun acc v -> Constraint.add (u,Lt,v) acc) acc lt in
+      let acc = List.fold_left (fun acc v -> Constraint.add (u,Le,v) acc) acc le in
+	acc
+    | Equiv v -> Constraint.add (u,Eq,v) acc
+  in
+    LMap.fold constraints_of g Constraint.empty
 
 (* Pretty-printing *)
 
@@ -989,101 +2145,67 @@ let pr_arc = function
       | [], _ | _, [] -> mt ()
       | _ -> spc ()
       in
-      pr_uni_level u ++ str " " ++
+      Level.pr u ++ str " " ++
       v 0
-        (pr_sequence (fun v -> str "< " ++ pr_uni_level v) lt ++
+        (pr_sequence (fun v -> str "< " ++ Level.pr v) lt ++
 	 opt_sep ++
-         pr_sequence (fun v -> str "<= " ++ pr_uni_level v) le) ++
+         pr_sequence (fun v -> str "<= " ++ Level.pr v) le) ++
       fnl ()
   | u, Equiv v ->
-      pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
+      Level.pr u  ++ str " = " ++ Level.pr v ++ fnl ()
 
 let pr_universes g =
-  let graph = UniverseLMap.fold (fun u a l -> (u,a)::l) g [] in
+  let graph = LMap.fold (fun u a l -> (u,a)::l) g [] in
   prlist pr_arc graph
 
-let pr_constraints c =
-  Constraint.fold (fun (u1,op,u2) pp_std ->
-		     let op_str = match op with
-		       | Lt -> " < "
-		       | Le -> " <= "
-		       | Eq -> " = "
-		     in pp_std ++  pr_uni_level u1 ++ str op_str ++
-			  pr_uni_level u2 ++ fnl () )  c (str "")
-
 (* Dumping constraints to a file *)
 
 let dump_universes output g =
   let dump_arc u = function
     | Canonical {univ=u; lt=lt; le=le} ->
-	let u_str = UniverseLevel.to_string u in
-	List.iter (fun v -> output Lt u_str (UniverseLevel.to_string v)) lt;
-	List.iter (fun v -> output Le u_str (UniverseLevel.to_string v)) le
+	let u_str = Level.to_string u in
+	List.iter (fun v -> output Lt u_str (Level.to_string v)) lt;
+	List.iter (fun v -> output Le u_str (Level.to_string v)) le
     | Equiv v ->
-      output Eq (UniverseLevel.to_string u) (UniverseLevel.to_string v)
+      output Eq (Level.to_string u) (Level.to_string v)
   in
-    UniverseLMap.iter dump_arc g
+    LMap.iter dump_arc g
 
-(* Hash-consing *)
-
-module Hunivlevel =
+module Huniverse_set = 
   Hashcons.Make(
     struct
-      type t = universe_level
-      type u = Names.DirPath.t -> Names.DirPath.t
-      let hashcons hdir = function
-	| UniverseLevel.Set -> UniverseLevel.Set
-	| UniverseLevel.Level (n,d) -> UniverseLevel.Level (n,hdir d)
-      let equal l1 l2 =
-        l1 == l2 ||
-        match l1,l2 with
-	| UniverseLevel.Set, UniverseLevel.Set -> true
-	| UniverseLevel.Level (n,d), UniverseLevel.Level (n',d') ->
-	  n == n' && d == d'
-	| _ -> false
-      let hash = UniverseLevel.hash
-    end)
-
-module Huniv =
-  Hashcons.Make(
-    struct
-      type t = universe
+      type t = universe_set
       type u = universe_level -> universe_level
-      let hashcons hdir = function
-	| Atom u -> Atom (hdir u)
-	| Max (gel,gtl) -> Max (List.map hdir gel, List.map hdir gtl)
-      let equal u v =
-        u == v ||
-	match u, v with
-	  | Atom u, Atom v -> u == v
-	  | Max (gel,gtl), Max (gel',gtl') ->
-	      (List.for_all2eq (==) gel gel') &&
-              (List.for_all2eq (==) gtl gtl')
-	  | _ -> false
-      let hash = Universe.hash
+      let hashcons huc s =
+	LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty
+      let equal s s' =
+	LSet.equal s s'
+      let hash = Hashtbl.hash
     end)
 
-let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons
-let hcons_univ = Hashcons.simple_hcons Huniv.generate hcons_univlevel
+let hcons_universe_set = 
+  Hashcons.simple_hcons Huniverse_set.generate Level.hcons
 
-module Hconstraint =
-  Hashcons.Make(
-    struct
-      type t = univ_constraint
-      type u = universe_level -> universe_level
-      let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
-      let equal (l1,k,l2) (l1',k',l2') =
-	l1 == l1' && k == k' && l2 == l2'
-      let hash = Hashtbl.hash
-    end)
+let hcons_universe_context_set (v, c) = 
+  (hcons_universe_set v, hcons_constraints c)
 
-module UConstraintHash =
-struct
-  type t = univ_constraint
-  let hash = Hashtbl.hash
-end
 
-module Hconstraints = Set.Hashcons(UConstraintOrd)(UConstraintHash)
+let hcons_univlevel = Level.hcons
+let hcons_univ x = x (* Universe.hcons (Huniv.node x) *)
+let equal_universes = Universe.equal_universes
 
-let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate hcons_univlevel
-let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint
+let explain_universe_inconsistency (o,u,v,p) =
+    let pr_rel = function
+      | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" 
+    in
+    let reason = match p with
+	[] -> mt()
+      | _::_ ->
+	str " because" ++ spc() ++ pr_uni v ++
+	  prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
+	  p ++
+	  (if Universe.eq (snd (List.last p)) u then mt() else
+	      (spc() ++ str "= " ++ pr_uni u)) 
+    in
+      str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
+        pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"