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.

18 files changed, 1074 insertions, 127 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index b1f133ac3..9cfe531ce 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -204,7 +204,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
 	| Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array)
 	| Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
           (iter_array e1_array) ** (iter_array e2_array)
-	| Const kn -> do_memoize_kn kn
+	| Const (kn,_) -> do_memoize_kn kn
 	| _ -> identity2 (* closed atomic types + rel *)
     and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2
     in iter t s acc
@@ -222,11 +222,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
   and add_kn kn s acc =
     let cb = lookup_constant kn in
     let do_type cst =
-      let ctype =
-	match cb.Declarations.const_type with
-	| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
-	| NonPolymorphicType t -> t
-      in
+      let ctype = cb.Declarations.const_type in
 	(s,ContextObjectMap.add cst ctype acc)
     in
     let (s,acc) =
diff --git a/library/declare.ml b/library/declare.ml
index c0c4dd571..452504bf0 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -44,36 +44,40 @@ let if_xml f x = if !Flags.xml_export then f x else ()
 
 type section_variable_entry =
   | SectionLocalDef of definition_entry
-  | SectionLocalAssum of types * bool (* Implicit status *)
+  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
-  | Inl cst -> Global.add_constraints cst
+  | Inl ctx -> Global.push_context_set ctx
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
     alreadydeclared (pr_id id ++ str " already exists");
-  let impl,opaq,cst = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum (ty, impl) ->
-        let cst = Global.push_named_assum (id,ty) in
-	let impl = if impl then Implicit else Explicit in
-	impl, true, cst
-    | SectionLocalDef de ->
-        let cst = Global.push_named_def (id,de) in
-        Explicit, de.const_entry_opaque, cst in
+
+  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum ((ty,ctx),poly,impl) ->
+      let () = Global.push_named_assum ((id,ty),ctx) in
+      let impl = if impl then Implicit else Explicit in
+	impl, true, poly, ctx
+    | SectionLocalDef (de) ->
+      let () = Global.push_named_def (id,de) in
+        Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
+	(Univ.ContextSet.of_context de.const_entry_universes) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl;
+  add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
-  add_variable_data id (p,opaq,cst,mk)
+  add_variable_data id (p,opaq,ctx,poly,mk)
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) -> Some (Inl (variable_constraints id))
+  | Inr (id,_) -> 
+    if variable_polymorphic id then None
+    else Some (Inl (variable_context id))
   | Inl _ -> Some o
 
 type variable_obj =
-    (Univ.constraints, Id.t * variable_declaration) union
+    (Univ.ContextSet.t, Id.t * variable_declaration) union
 
 let inVariable : variable_obj -> obj =
   declare_object { (default_object "VARIABLE") with
@@ -139,7 +143,8 @@ let cache_constant ((sp,kn), obj) =
   let kn' = Global.add_constant dir id obj.cst_decl in
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
-  add_section_constant kn' (Global.lookup_constant kn').const_hyps;
+  let cst = Global.lookup_constant kn' in
+  add_section_constant (cst.const_proj <> None) kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
   add_constant_kind (constant_of_kn kn) obj.cst_kind
 
@@ -150,16 +155,18 @@ let discharged_hyps kn sechyps =
 
 let discharge_constant ((sp, kn), obj) =
   let con = constant_of_kn kn in
+
   let from = Global.lookup_constant con in
   let modlist = replacement_context () in
-  let hyps = section_segment_of_constant con in
+  let hyps,uctx = section_segment_of_constant con in
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
-  let abstract = named_of_variable_context hyps in
+  let abstract = (named_of_variable_context hyps, uctx) in
   let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
   Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None))
+let dummy_constant_entry = 
+  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -187,6 +194,18 @@ let declare_constant_common id cst =
   Notation.declare_ref_arguments_scope (ConstRef c);
   c
 
+let definition_entry ?(opaque=false) ?types 
+    ?(poly=false) ?(univs=Univ.UContext.empty) body =
+  { const_entry_body = Future.from_val (body,Declareops.no_seff);
+    const_entry_secctx = None;
+    const_entry_type = types;
+    const_entry_proj = None;
+    const_entry_polymorphic = poly;
+    const_entry_universes = univs;
+    const_entry_opaque = opaque;
+    const_entry_feedback = None;
+    const_entry_inline_code = false}
+
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
 let declare_sideff se =
@@ -203,8 +222,7 @@ let declare_sideff se =
   in
   let ty_of cb =
     match cb.Declarations.const_type with
-    | Declarations.NonPolymorphicType t -> Some t
-    | _ -> None in
+    | (* Declarations.NonPolymorphicType  *)t -> Some t in
   let cst_of cb =
     let pt, opaque = pt_opaque_of cb in
     let ty = ty_of cb in
@@ -215,6 +233,9 @@ let declare_sideff se =
         const_entry_opaque = opaque;
         const_entry_inline_code = false;
         const_entry_feedback = None;
+	const_entry_polymorphic = cb.const_polymorphic;
+	const_entry_universes = Future.join cb.const_universes;
+	const_entry_proj = None;
     });
     cst_hyps = [] ;
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
@@ -252,16 +273,11 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
   let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
   kn
 
-let declare_definition ?(internal=UserVerbose)
+let declare_definition ?(internal=UserVerbose) 
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
-  id ?types body =
+  ?(poly=false) id ?types (body,ctx) =
   let cb = 
-    { Entries.const_entry_body = body;
-      const_entry_type = types;
-      const_entry_opaque = opaque;
-      const_entry_inline_code = false;
-      const_entry_secctx = None;
-      const_entry_feedback = None }
+    definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
     declare_constant ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
@@ -311,7 +327,8 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_mind dir id mie in
   assert (eq_mind kn' (mind_of_kn kn));
-  add_section_kn kn' (Global.lookup_mind kn').mind_hyps;
+  let mind = Global.lookup_mind kn' in
+  add_section_kn kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
@@ -319,9 +336,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
-  let sechyps = section_segment_of_mutual_inductive mind in
+  let sechyps,uctx = section_segment_of_mutual_inductive mind in
   Some (discharged_hyps kn sechyps,
-        Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
+        Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
@@ -335,7 +352,9 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_params = [];
   mind_entry_record = false;
   mind_entry_finite = true;
-  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
+  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
+  mind_entry_polymorphic = false;
+  mind_entry_universes = Univ.UContext.empty })
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
diff --git a/library/declare.mli b/library/declare.mli
index 663d240dc..848bab618 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -23,7 +23,7 @@ open Decl_kinds
 
 type section_variable_entry =
   | SectionLocalDef of definition_entry
-  | SectionLocalAssum of types * bool (** Implicit status *)
+  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
@@ -47,12 +47,18 @@ type internal_flag =
   | KernelSilent
   | UserVerbose
 
+(* Defaut definition entries, transparent with no secctx or proj information *)
+val definition_entry : ?opaque:bool -> ?types:types -> 
+  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+  constr -> definition_entry
+
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  ?local:bool -> Id.t -> ?types:constr -> Entries.const_entry_body -> constant
+  ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
+  constr Univ.in_universe_context_set -> constant
 
 (** Since transparent constant's side effects are globally declared, we
  *  need that *)
diff --git a/library/decls.ml b/library/decls.ml
index 2d8807f80..811d09667 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -18,17 +18,18 @@ open Libnames
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
-    DirPath.t * bool (* opacity *) * Univ.constraints * logical_kind
+  DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind
 
 let vartab =
   Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
 
 let add_variable_data id o = vartab := Id.Map.add id o !vartab
 
-let variable_path id = let (p,_,_,_) = Id.Map.find id !vartab in p
-let variable_opacity id = let (_,opaq,_,_) = Id.Map.find id !vartab in opaq
-let variable_kind id = let (_,_,_,k) = Id.Map.find id !vartab in k
-let variable_constraints id = let (_,_,cst,_) = Id.Map.find id !vartab in cst
+let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p
+let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq
+let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k
+let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx
+let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p
 
 let variable_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
diff --git a/library/decls.mli b/library/decls.mli
index f45e4f121..6e9d4a4ab 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -17,14 +17,15 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-    DirPath.t * bool (** opacity *) * Univ.constraints * logical_kind
+  DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
-val variable_constraints : variable -> Univ.constraints
+val variable_context : variable -> Univ.universe_context_set
+val variable_polymorphic : variable -> polymorphic
 val variable_exists : variable -> bool
 
 (** Registration and access to the table of constants *)
diff --git a/library/global.ml b/library/global.ml
index a8121d15f..c56bc9e77 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -70,9 +70,12 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum a = globalize (Safe_typing.push_named_assum a)
-let push_named_def d = globalize (Safe_typing.push_named_def d)
+let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
+let push_named_def d = globalize0 (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
+let push_context_set c = globalize0 (Safe_typing.push_context_set c)
+let push_context c = globalize0 (Safe_typing.push_context c)
+
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
@@ -101,6 +104,7 @@ let named_context_val () = named_context_val (env())
 let lookup_named id = lookup_named id (env())
 let lookup_constant kn = lookup_constant kn (env())
 let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
+let lookup_pinductive (ind,_) = Inductive.lookup_mind_specif (env()) ind
 let lookup_mind kn = lookup_mind kn (env())
 
 let lookup_module mp = lookup_module mp (env())
@@ -139,19 +143,43 @@ let env_of_context hyps =
 
 open Globnames
 
-let type_of_reference env = function
+(** Build a fresh instance for a given context, its associated substitution and 
+    the instantiated constraints. *)
+
+let type_of_global_unsafe r = 
+  let env = env() in
+  match r with
   | VarRef id -> Environ.named_type id env
-  | ConstRef c -> Typeops.type_of_constant env c
+  | ConstRef c -> 
+     let cb = Environ.lookup_constant c env in cb.Declarations.const_type
+  | IndRef ind ->
+     let (mib, oib) = Inductive.lookup_mind_specif env ind in
+       oib.Declarations.mind_arity.Declarations.mind_user_arity
+  | ConstructRef cstr ->
+     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+     let inst = Univ.UContext.instance mib.Declarations.mind_universes in
+       Inductive.type_of_constructor (cstr,inst) specif
+
+
+let is_polymorphic r = 
+  let env = env() in
+  match r with
+  | VarRef id -> false
+  | ConstRef c -> 
+     let cb = Environ.lookup_constant c env in cb.Declarations.const_polymorphic
   | IndRef ind ->
-     let specif = Inductive.lookup_mind_specif env ind in
-      Inductive.type_of_inductive env specif
+     let (mib, oib) = Inductive.lookup_mind_specif env ind in
+       mib.Declarations.mind_polymorphic
   | ConstructRef cstr ->
-     let specif =
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-       Inductive.type_of_constructor cstr specif
+     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+       mib.Declarations.mind_polymorphic
 
-let type_of_global t = type_of_reference (env ()) t
+let current_dirpath () = 
+  Safe_typing.current_dirpath (safe_env ())
 
+let with_global f = 
+  let (a, ctx) = f (env ()) (current_dirpath ()) in
+    push_context_set ctx; a
 
 (* spiwack: register/unregister functions for retroknowledge *)
 let register field value by_clause =
diff --git a/library/global.mli b/library/global.mli
index e11e1c017..b6825ffa5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -33,13 +33,19 @@ val add_constraints : Univ.constraints -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Term.types) -> Univ.constraints
-val push_named_def   : (Id.t * Entries.definition_entry) -> Univ.constraints
+val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
+val push_named_def   : (Id.t * Entries.definition_entry) -> unit
+
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
 val add_mind :
   DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
+val add_constraints : Univ.constraints -> unit
+
+val push_context : Univ.universe_context -> unit
+val push_context_set : Univ.universe_context_set -> unit
+
 (** Non-interactive modules and module types *)
 
 val add_module :
@@ -72,6 +78,8 @@ val lookup_named     : variable -> Context.named_declaration
 val lookup_constant  : constant -> Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
+val lookup_pinductive : Constr.pinductive -> 
+  Declarations.mutual_inductive_body * Declarations.one_inductive_body
 val lookup_mind      : mutual_inductive -> Declarations.mutual_inductive_body
 val lookup_module    : module_path -> Declarations.module_body
 val lookup_modtype   : module_path -> Declarations.module_type_body
@@ -94,11 +102,14 @@ val import :
 (** Function to get an environment from the constants part of the global
  * environment and a given context. *)
 
-val type_of_global : Globnames.global_reference -> Term.types
 val env_of_context : Environ.named_context_val -> Environ.env
 
 val join_safe_environment : unit -> unit
 
+val is_polymorphic : Globnames.global_reference -> bool
+
+(* val type_of_global : Globnames.global_reference -> types Univ.in_universe_context_set *)
+val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
 
 (** {6 Retroknowledge } *)
 
@@ -109,5 +120,10 @@ val register_inline : constant -> unit
 
 (** {6 Oracle } *)
 
-val set_strategy : 'a Names.tableKey -> Conv_oracle.level -> unit
+val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit
+
+(* Modifies the global state, registering new universes *)
+
+val current_dirpath : unit -> Names.dir_path
 
+val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a
diff --git a/library/globnames.ml b/library/globnames.ml
index 8a9e99621..c881e797e 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -38,19 +38,31 @@ let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
 
-let subst_constructor subst ((kn,i),j as ref) =
-  let kn' = subst_ind subst kn in
-    if kn==kn' then ref, mkConstruct ref
-    else ((kn',i),j), mkConstruct ((kn',i),j)
+let subst_constructor subst (ind,j as ref) =
+  let ind' = subst_ind subst ind in
+    if ind==ind' then ref, mkConstruct ref
+    else (ind',j), mkConstruct (ind',j)
+
+let subst_global_reference subst ref = match ref with
+  | VarRef var -> ref
+  | ConstRef kn ->
+    let kn' = subst_constant subst kn in
+      if kn==kn' then ref else ConstRef kn'
+  | IndRef ind ->
+    let ind' = subst_ind subst ind in
+      if ind==ind' then ref else IndRef ind'
+  | ConstructRef ((kn,i),j as c) ->
+    let c',t = subst_constructor subst c in
+      if c'==c then ref else ConstructRef c'
 
 let subst_global subst ref = match ref with
   | VarRef var -> ref, mkVar var
   | ConstRef kn ->
-     let kn',t = subst_con subst kn in
+     let kn',t = subst_con_kn subst kn in
       if kn==kn' then ref, mkConst kn else ConstRef kn', t
-  | IndRef (kn,i) ->
-      let kn' = subst_ind subst kn in
-      if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
+  | IndRef ind ->
+      let ind' = subst_ind subst ind in
+      if ind==ind' then ref, mkInd ind else IndRef ind', mkInd ind'
   | ConstructRef ((kn,i),j as c) ->
       let c',t = subst_constructor subst c in
 	if c'==c then ref,t else ConstructRef c', t
@@ -62,19 +74,26 @@ let canonical_gr = function
   | VarRef id -> VarRef id
 
 let global_of_constr c = match kind_of_term c with
-  | Const sp -> ConstRef sp
-  | Ind ind_sp -> IndRef ind_sp
-  | Construct cstr_cp -> ConstructRef cstr_cp
+  | Const (sp,u) -> ConstRef sp
+  | Ind (ind_sp,u) -> IndRef ind_sp
+  | Construct (cstr_cp,u) -> ConstructRef cstr_cp
   | Var id -> VarRef id
   |  _ -> raise Not_found
 
-let constr_of_global = function
+let is_global c t =
+  match c, kind_of_term t with
+  | ConstRef c, Const (c', _) -> eq_constant c c'
+  | IndRef i, Ind (i', _) -> eq_ind i i'
+  | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+  | VarRef id, Var id' -> id_eq id id'
+  | _ -> false
+
+let printable_constr_of_global = function
   | VarRef id -> mkVar id
   | ConstRef sp -> mkConst sp
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
 let global_eq_gen eq_cst eq_ind eq_cons x y =
@@ -179,10 +198,6 @@ type global_reference_or_constr =
   | IsGlobal of global_reference
   | IsConstr of constr
 
-let constr_of_global_or_constr = function
-  | IsConstr c -> c
-  | IsGlobal gr -> constr_of_global gr
-
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
 let encode_mind dir id = MutInd.make2 (MPfile dir) (Label.of_id id)
diff --git a/library/globnames.mli b/library/globnames.mli
index 5d717965e..5ea0c9de0 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -31,19 +31,21 @@ val destConstRef : global_reference -> constant
 val destIndRef : global_reference -> inductive
 val destConstructRef : global_reference -> constructor
 
+val is_global : global_reference -> constr -> bool
 
 val subst_constructor : substitution -> constructor -> constructor * constr
 val subst_global : substitution -> global_reference -> global_reference * constr
+val subst_global_reference : substitution -> global_reference -> global_reference
 
-(** Turn a global reference into a construction *)
-val constr_of_global : global_reference -> constr
+(** This constr is not safe to be typechecked, universe polymorphism is not 
+    handled here: just use for printing *)
+val printable_constr_of_global : global_reference -> constr
 
 (** Turn a construction denoting a global reference into a global reference;
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> global_reference
 
 (** Obsolete synonyms for constr_of_global and global_of_constr *)
-val constr_of_reference : global_reference -> constr
 val reference_of_constr : constr -> global_reference
 
 module RefOrdered : sig
@@ -87,8 +89,6 @@ type global_reference_or_constr =
   | IsGlobal of global_reference
   | IsConstr of constr
 
-val constr_of_global_or_constr : global_reference_or_constr -> constr
-
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
 val encode_mind : DirPath.t -> Id.t -> mutual_inductive
diff --git a/library/heads.ml b/library/heads.ml
index f64cdb05a..0faad827e 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -58,7 +58,7 @@ let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
 let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
 
 let kind_of_head env t =
-  let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with
+  let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta env t) with
   | Rel n when n > k -> NotImmediatelyComputableHead
   | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
   | Var id ->
@@ -68,7 +68,7 @@ let kind_of_head env t =
         match pi2 (lookup_named id env) with
         | Some c -> aux k l c b
         | None -> NotImmediatelyComputableHead)
-  | Const cst ->
+  | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
        with Not_found -> assert false)
   | Construct _ | CoFix _ ->
@@ -85,6 +85,10 @@ let kind_of_head env t =
   | LetIn _ -> assert false
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
   | App (c,al) -> aux k (Array.to_list al @ l) c b
+  | Proj (p,c) ->
+      (try on_subterm k (c :: l) b (constant_head p)
+       with Not_found -> assert false)
+
   | Case (_,_,c,_) -> aux k [] c true
   | Fix ((i,j),_) ->
       let n = i.(j) in
@@ -113,11 +117,18 @@ let kind_of_head env t =
   | x -> x
   in aux 0 [] t false
 
+(* FIXME: maybe change interface here *)
 let compute_head = function
 | EvalConstRef cst ->
-    (match constant_opt_value (Global.env()) cst with
+   let env = Global.env() in
+   let cb = Environ.lookup_constant cst env in
+   let body = 
+     if cb.Declarations.const_proj = None 
+     then Declareops.body_of_constant cb else None 
+   in
+     (match body with
      | None -> RigidHead (RigidParameter cst)
-     | Some c -> kind_of_head (Global.env()) c)
+     | Some c -> kind_of_head env c)
 | EvalVarRef id ->
     (match pi2 (Global.lookup_named id) with
      | Some c when not (Decls.variable_opacity id) ->
@@ -140,8 +151,8 @@ let cache_head o =
 
 let subst_head_approximation subst = function
   | RigidHead (RigidParameter cst) as k ->
-      let cst,c = subst_con subst cst in
-      if isConst c && eq_constant (destConst c) cst then
+      let cst,c = subst_con_kn subst cst in
+      if isConst c && eq_constant (fst (destConst c)) cst then
         (* A change of the prefix of the constant *)
         k
       else
diff --git a/library/impargs.ml b/library/impargs.ml
index 1bcff8695..5a44b5bdb 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -169,7 +169,7 @@ let is_flexible_reference env bound depth f =
     | Rel n when n >= bound+depth -> (* inductive type *) false
     | Rel n when n >= depth -> (* previous argument *) true
     | Rel n -> (* since local definitions have been expanded *) false
-    | Const kn ->
+    | Const (kn,_) ->
         let cb = Environ.lookup_constant kn env in
 	(match cb.const_body with Def _ -> true | _ -> false)
     | Var id ->
@@ -214,6 +214,7 @@ let rec is_rigid_head t = match kind_of_term t with
   | Rel _ | Evar _ -> false
   | Ind _ | Const _ | Var _ | Sort _ -> true
   | Case (_,_,f,_) -> is_rigid_head f
+  | Proj (p,c) -> true
   | App (f,args) ->
       (match kind_of_term f with
 	| Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i)))
@@ -401,7 +402,14 @@ let compute_semi_auto_implicits env f manual t =
 
 let compute_constant_implicits flags manual cst =
   let env = Global.env () in
-  compute_semi_auto_implicits env flags manual (Typeops.type_of_constant env cst)
+  let cb = Environ.lookup_constant cst env in
+  let ty = cb.const_type in
+  let impls = compute_semi_auto_implicits env flags manual ty in
+    impls
+    (* match cb.const_proj with *)
+    (* | None -> impls *)
+    (* | Some {proj_npars = n} ->  *)
+    (* List.map (fun (x,args) -> x, CList.skipn_at_least n args) impls *)
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -413,14 +421,15 @@ let compute_mib_implicits flags manual kn =
   let mib = lookup_mind kn env in
   let ar =
     Array.to_list
-      (Array.map  (* No need to lift, arities contain no de Bruijn *)
-        (fun mip ->
-	  (Name mip.mind_typename, None, type_of_inductive env (mib,mip)))
+      (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
+        (fun i mip ->
+	  (** No need to care about constraints here *)
+	  (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i))))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
-    let ar = type_of_inductive env (mib,mip) in
+    let ar = Global.type_of_global_unsafe (IndRef ind) in
     ((IndRef ind,compute_semi_auto_implicits env flags manual ar),
      Array.mapi (fun j c ->
        (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c))
@@ -517,7 +526,7 @@ let section_segment_of_reference = function
   | ConstRef con -> section_segment_of_constant con
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       section_segment_of_mutual_inductive kn
-  | _ -> []
+  | _ -> [], Univ.UContext.empty
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
@@ -532,24 +541,36 @@ let discharge_implicits (_,(req,l)) =
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
     (try
-      let vars = section_segment_of_reference ref in
+      let vars,_ = section_segment_of_reference ref in
+      (* let isproj =  *)
+      (* 	 match ref with *)
+      (* 	 | ConstRef cst -> is_projection cst (Global.env ()) *)
+      (* 	 | _ -> false *)
+      (* in *)
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
-      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+      let l' = 
+	(* if isproj then [ref',snd (List.hd l)] *)
+	(* else *)
+	  [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
     (try
       let con' = pop_con con in
-      let vars = section_segment_of_constant con in
+      let vars,_ = section_segment_of_constant con in
       let extra_impls = impls_of_context vars in
-      let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+      let newimpls = 
+	(* if is_projection con (Global.env()) then (snd (List.hd l)) *)
+	(* else *) List.map (add_section_impls vars extra_impls) (snd (List.hd l))
+      in
+      let l' = [ConstRef con',newimpls] in
 	Some (ImplConstant (con',flags),l')
     with Not_found -> (* con not defined in this section *) Some (req,l))
   | ImplMutualInductive (kn,flags) ->
     (try
       let l' = List.map (fun (gr, l) ->
-	let vars = section_segment_of_reference gr in
+	let vars,_ = section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
 	 List.map (add_section_impls vars extra_impls) l)) l
@@ -659,10 +680,14 @@ let check_rigidity isrigid =
   if not isrigid then
     errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
+let projection_implicits env p (x, impls) = 
+  let pb = Environ.lookup_projection p env in
+    x, CList.skipn_at_least pb.Declarations.proj_npars impls
+
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
-  let t = Global.type_of_global ref in
+  let t = Global.type_of_global_unsafe ref in
   let enriching = Option.default flags.auto enriching in
   let isrigid,autoimpls = compute_auto_implicits env flags enriching t in
   let l' = match l with
diff --git a/library/impargs.mli b/library/impargs.mli
index e70cff838..8ad86bdff 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -129,6 +129,8 @@ val make_implicits_list : implicit_status list -> implicits_list list
 
 val drop_first_implicits : int -> implicits_list -> implicits_list
 
+val projection_implicits : env -> projection -> implicits_list -> implicits_list
+
 val select_impargs_size : int -> implicits_list list -> implicit_status list
 
 val select_stronger_impargs : implicits_list list -> implicit_status list
diff --git a/library/kindops.ml b/library/kindops.ml
index 6e6c7527b..b8337f5d7 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -24,7 +24,7 @@ let string_of_theorem_kind = function
   | Corollary -> "Corollary"
 
 let string_of_definition_kind def =
-  let (locality, kind) = def in
+  let (locality, poly, kind) = def in
   let error () = Errors.anomaly (Pp.str "Internal definition kind") in
   match kind with
   | Definition ->
diff --git a/library/lib.ml b/library/lib.ml
index 331196565..31f983595 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -380,11 +380,14 @@ let find_opening_node id =
 *)
 
 type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types
+
 type variable_context = variable_info list
-type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t
+type abstr_list = variable_context Univ.in_universe_context Names.Cmap.t *
+  variable_context Univ.in_universe_context Names.Mindmap.t
 
 let sectab =
-  Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
+  Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * 
+		Decl_kinds.polymorphic * Univ.universe_context_set) list *
 		        Opaqueproof.work_list * abstr_list) list)
     ~name:"section-context"
 
@@ -392,18 +395,19 @@ let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),
                 (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
-let add_section_variable id impl =
+let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := ((id,impl)::vars,repl,abs)::sl
+	sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
-      (id',impl,b,t) :: aux (idl,hyps)
+    | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+      let l, r = aux (idl,hyps) in 
+	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
     | (id::idl,hyps) -> aux (idl,hyps)
-    | [], _ -> []
+    | [], _ -> [],Univ.ContextSet.empty
   in aux (secs,ohyps)
 
 let instance_from_variable_context sign =
@@ -413,23 +417,26 @@ let instance_from_variable_context sign =
     | [] -> [] in
   Array.of_list (inst_rec sign)
 
-let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t))
-
+let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx
+  
 let add_section_replacement f g hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
-    let sechyps = extract_hyps (vars,hyps) in
+    let sechyps,ctx = extract_hyps (vars,hyps) in
+    let ctx = Univ.ContextSet.to_context ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f args exps,g sechyps abs)::sl
+    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,ctx) abs)::sl
 
 let add_section_kn kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
   add_section_replacement f f
 
-let add_section_constant kn =
+let add_section_constant is_projection kn =
+  (* let g x (l1,l2) = (Names.Cmap.add kn (Univ.Instance.empty,[||]) l1,l2) in *)
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-  add_section_replacement f f
+    (* if is_projection then add_section_replacement g f *)
+    (* else *) add_section_replacement f f
 
 let replacement_context () = pi2 (List.hd !sectab)
 
@@ -445,7 +452,9 @@ let rec list_mem_assoc x = function
 
 let section_instance = function
   | VarRef id ->
-      if list_mem_assoc id (pi1 (List.hd !sectab)) then [||]
+      if List.exists (fun (id',_,_,_) -> Names.id_eq id id') 
+	(pi1 (List.hd !sectab))
+      then Univ.Instance.empty, [||]
       else raise Not_found
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
@@ -459,8 +468,8 @@ let full_replacement_context () = List.map pi2 !sectab
 let full_section_segment_of_constant con =
   List.map (fun (vars,_,(x,_)) -> fun hyps ->
     named_of_variable_context
-      (try Names.Cmap.find con x
-      with Not_found -> extract_hyps (vars, hyps))) !sectab
+      (try fst (Names.Cmap.find con x)
+       with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
 
 (*************)
 (* Sections. *)
diff --git a/library/lib.mli b/library/lib.mli
index 8975acd9a..759a1a135 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -161,23 +161,23 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t
 (** {6 Section management for discharge } *)
 type variable_info = Names.Id.t * Decl_kinds.binding_kind *
     Term.constr option * Term.types
-type variable_context = variable_info list
+type variable_context = variable_info list 
 
 val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Context.named_context
 
-val section_segment_of_constant : Names.constant -> variable_context
-val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
+val section_segment_of_constant : Names.constant -> variable_context Univ.in_universe_context
+val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context Univ.in_universe_context
 
-val section_instance : Globnames.global_reference -> Names.Id.t array
+val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
-val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> unit
+val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
 
-val add_section_constant : Names.constant -> Context.named_context -> unit
+val add_section_constant : bool (* is_projection *) -> 
+  Names.constant -> Context.named_context -> unit
 val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
-val replacement_context : unit ->
-  (Names.Id.t array Names.Cmap.t * Names.Id.t array Names.Mindmap.t)
+val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
 
diff --git a/library/library.mllib b/library/library.mllib
index 2568bcc18..6a58a1057 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -5,6 +5,7 @@ Libobject
 Summary
 Nametab
 Global
+Universes
 Lib
 Declaremods
 Loadpath
diff --git a/library/universes.ml b/library/universes.ml
new file mode 100644
index 000000000..79286792d
--- /dev/null
+++ b/library/universes.ml
@@ -0,0 +1,647 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Pp
+open Names
+open Term
+open Context
+open Environ
+open Locus
+open Univ
+
+(* Generator of levels *)
+let new_univ_level, set_remote_new_univ_level =
+  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
+    ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n)
+
+let new_univ_level _ = new_univ_level ()
+  (* Univ.Level.make db (new_univ_level ()) *)
+
+let fresh_level () = new_univ_level (Global.current_dirpath ())
+
+(* TODO: remove *)
+let new_univ dp = Univ.Universe.make (new_univ_level dp)
+let new_Type dp = mkType (new_univ dp)
+let new_Type_sort dp = Type (new_univ dp)
+
+let fresh_universe_instance ctx =
+  Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) 
+    (UContext.instance ctx)
+
+let fresh_instance_from_context ctx =
+  let inst = fresh_universe_instance ctx in
+  let subst = make_universe_subst inst ctx in
+  let constraints = instantiate_univ_context subst ctx in
+    (inst, subst), constraints
+
+let fresh_instance ctx =
+  let s = ref LSet.empty in
+  let inst = 
+    Instance.subst_fn (fun _ -> 
+      let u = new_univ_level (Global.current_dirpath ()) in 
+	s := LSet.add u !s; u) 
+      (UContext.instance ctx)
+  in !s, inst
+
+let fresh_instance_from ctx =
+  let ctx', inst = fresh_instance ctx in
+  let subst = make_universe_subst inst ctx in
+  let constraints = instantiate_univ_context subst ctx in
+    (inst, subst), (ctx', constraints)
+
+(** Fresh universe polymorphic construction *)
+
+let fresh_constant_instance env c =
+  let cb = lookup_constant c env in
+    if cb.Declarations.const_polymorphic then
+      let (inst,_), ctx = fresh_instance_from (Future.join cb.Declarations.const_universes) in
+	((c, inst), ctx)
+    else ((c,Instance.empty), ContextSet.empty)
+
+let fresh_inductive_instance env ind = 
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+    if mib.Declarations.mind_polymorphic then
+      let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in
+	((ind,inst), ctx)
+    else ((ind,Instance.empty), ContextSet.empty)
+
+let fresh_constructor_instance env (ind,i) = 
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+    if mib.Declarations.mind_polymorphic then
+      let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in
+	(((ind,i),inst), ctx)
+    else (((ind,i),Instance.empty), ContextSet.empty)
+
+open Globnames
+let fresh_global_instance env gr =
+  match gr with
+  | VarRef id -> mkVar id, ContextSet.empty
+  | ConstRef sp -> 
+     let c, ctx = fresh_constant_instance env sp in
+       mkConstU c, ctx
+  | ConstructRef sp ->
+     let c, ctx = fresh_constructor_instance env sp in
+       mkConstructU c, ctx
+  | IndRef sp -> 
+     let c, ctx = fresh_inductive_instance env sp in
+       mkIndU c, ctx
+
+let constr_of_global gr =
+  let c, ctx = fresh_global_instance (Global.env ()) gr in
+    Global.push_context_set ctx; c
+
+let constr_of_global_univ (gr,u) =
+  match gr with
+  | VarRef id -> mkVar id
+  | ConstRef sp -> mkConstU (sp,u)
+  | ConstructRef sp -> mkConstructU (sp,u)
+  | IndRef sp -> mkIndU (sp,u)
+
+let fresh_global_or_constr_instance env = function
+  | IsConstr c -> c, ContextSet.empty
+  | IsGlobal gr -> fresh_global_instance env gr
+
+let global_of_constr c =
+  match kind_of_term c with
+  | Const (c, u) -> ConstRef c, u
+  | Ind (i, u) -> IndRef i, u
+  | Construct (c, u) -> ConstructRef c, u
+  | Var id -> VarRef id, Instance.empty
+  | _ -> raise Not_found
+
+let global_app_of_constr c =
+  match kind_of_term c with
+  | Const (c, u) -> (ConstRef c, u), None
+  | Ind (i, u) -> (IndRef i, u), None
+  | Construct (c, u) -> (ConstructRef c, u), None
+  | Var id -> (VarRef id, Instance.empty), None
+  | Proj (p, c) -> (ConstRef p, Instance.empty), Some c
+  | _ -> raise Not_found
+
+open Declarations
+
+let type_of_reference env r =
+  match r with
+  | VarRef id -> Environ.named_type id env, ContextSet.empty
+  | ConstRef c ->
+     let cb = Environ.lookup_constant c env in
+       if cb.const_polymorphic then
+	 let (inst, subst), ctx = fresh_instance_from (Future.join cb.const_universes) in
+	   Vars.subst_univs_constr subst cb.const_type, ctx
+       else cb.const_type, ContextSet.empty
+
+  | IndRef ind ->
+     let (mib, oib) = Inductive.lookup_mind_specif env ind in
+       if mib.mind_polymorphic then
+	 let (inst, subst), ctx = fresh_instance_from mib.mind_universes in
+	   Vars.subst_univs_constr subst oib.mind_arity.mind_user_arity, ctx
+       else oib.mind_arity.mind_user_arity, ContextSet.empty
+  | ConstructRef cstr ->
+     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+       if mib.mind_polymorphic then
+	 let (inst, subst), ctx = fresh_instance_from mib.mind_universes in
+	   Inductive.type_of_constructor (cstr,inst) specif, ctx
+       else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
+
+let type_of_global t = type_of_reference (Global.env ()) t
+
+let fresh_sort_in_family env = function
+  | InProp -> prop_sort, ContextSet.empty
+  | InSet -> set_sort, ContextSet.empty
+  | InType -> 
+    let u = fresh_level () in
+      Type (Univ.Universe.make u), ContextSet.singleton u
+
+let new_sort_in_family sf =
+  fst (fresh_sort_in_family (Global.env ()) sf)
+
+let extend_context (a, ctx) (ctx') =
+  (a, ContextSet.union ctx ctx')
+
+let new_global_univ () =
+  let u = fresh_level () in
+    (Univ.Universe.make u, ContextSet.singleton u)
+
+(** Simplification *)
+
+module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
+
+let remove_trivial_constraints cst =
+  Constraint.fold (fun (l,d,r as cstr) nontriv ->
+    if d != Lt && eq_levels l r then nontriv
+    else if d == Le && is_type0m_univ (Univ.Universe.make l) then nontriv
+    else Constraint.add cstr nontriv)
+    cst Constraint.empty
+
+let add_list_map u t map = 
+  let l, d, r = LMap.split u map in
+  let d' = match d with None -> [t] | Some l -> t :: l in
+  let lr = 
+    LMap.merge (fun k lm rm -> 
+      match lm with Some t -> lm | None ->
+      match rm with Some t -> rm | None -> None) l r
+  in LMap.add u d' lr
+
+let find_list_map u map =
+  try LMap.find u map with Not_found -> []
+
+module UF = LevelUnionFind
+type universe_full_subst = (universe_level * universe) list
+  
+(** Precondition: flexible <= ctx *)
+let choose_canonical ctx flexible algs s =
+  let global = LSet.diff s ctx in
+  let flexible, rigid = LSet.partition (fun x -> LMap.mem x flexible) (LSet.inter s ctx) in
+    (** If there is a global universe in the set, choose it *)
+    if not (LSet.is_empty global) then
+      let canon = LSet.choose global in
+	canon, (LSet.remove canon global, rigid, flexible)
+    else (** No global in the equivalence class, choose a rigid one *)
+	if not (LSet.is_empty rigid) then
+	  let canon = LSet.choose rigid in
+	    canon, (global, LSet.remove canon rigid, flexible)
+	else (** There are only flexible universes in the equivalence
+		 class, choose a non-algebraic. *)
+	  let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
+	    if not (LSet.is_empty nonalgs) then
+	      let canon = LSet.choose nonalgs in
+		canon, (global, rigid, LSet.remove canon flexible)
+	    else
+	      let canon = LSet.choose algs in
+		canon, (global, rigid, LSet.remove canon flexible)
+
+open Universe
+
+let subst_puniverses subst (c, u as cu) =
+  let u' = Instance.subst subst u in
+    if u' == u then cu else (c, u')
+
+let nf_evars_and_universes_local f subst =
+  let rec aux c =
+    match kind_of_term c with
+    | Evar (evdk, _ as ev) ->
+      (match f ev with
+      | None -> c
+      | Some c -> aux c)
+    | Const pu -> 
+      let pu' = subst_puniverses subst pu in
+	if pu' == pu then c else mkConstU pu'
+    | Ind pu ->
+      let pu' = subst_puniverses subst pu in
+	if pu' == pu then c else mkIndU pu'
+    | Construct pu ->
+      let pu' = subst_puniverses subst pu in
+	if pu' == pu then c else mkConstructU pu'
+    | Sort (Type u) ->
+      let u' = Univ.subst_univs_level_universe subst u in
+	if u' == u then c else mkSort (sort_of_univ u')
+    | _ -> map_constr aux c
+  in aux
+
+let subst_univs_fn_puniverses lsubst (c, u as cu) =
+  let u' = Instance.subst_fn lsubst u in
+    if u' == u then cu else (c, u')
+
+let subst_univs_puniverses subst cu =
+  subst_univs_fn_puniverses (Univ.level_subst_of (Univ.make_subst subst)) cu
+
+let nf_evars_and_universes_gen f subst =
+  let lsubst = Univ.level_subst_of subst in
+  let rec aux c =
+    match kind_of_term c with
+    | Evar (evdk, _ as ev) ->
+      (match try f ev with Not_found -> None with
+      | None -> c
+      | Some c -> aux c)
+    | Const pu -> 
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+	if pu' == pu then c else mkConstU pu'
+    | Ind pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+	if pu' == pu then c else mkIndU pu'
+    | Construct pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+	if pu' == pu then c else mkConstructU pu'
+    | Sort (Type u) ->
+      let u' = Univ.subst_univs_universe subst u in
+	if u' == u then c else mkSort (sort_of_univ u')
+    | _ -> map_constr aux c
+  in aux
+
+let nf_evars_and_universes_subst f subst =
+  nf_evars_and_universes_gen f (Univ.make_subst subst)
+
+let nf_evars_and_universes_opt_subst f subst =
+  let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
+    nf_evars_and_universes_gen f subst
+
+let subst_univs_full_constr subst c = 
+  nf_evars_and_universes_subst (fun _ -> None) subst c
+
+let fresh_universe_context_set_instance ctx =
+  if ContextSet.is_empty ctx then LMap.empty, ctx
+  else
+    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
+    let univs',subst = LSet.fold
+      (fun u (univs',subst) ->
+	let u' = fresh_level () in
+	  (LSet.add u' univs', LMap.add u u' subst))
+      univs (LSet.empty, LMap.empty)
+    in
+    let cst' = subst_univs_level_constraints subst cst in
+      subst, (univs', cst')
+
+let normalize_univ_variable ~find ~update =
+  let rec aux cur =
+    let b = find cur in
+    let b' = subst_univs_universe aux b in
+      if Universe.eq b' b then b
+      else update cur b'
+  in fun b -> try aux b with Not_found -> Universe.make b
+
+let normalize_univ_variable_opt_subst ectx =
+  let find l = 
+    match Univ.LMap.find l !ectx with
+    | Some b -> b
+    | None -> raise Not_found
+  in
+  let update l b =
+    assert (match Universe.level b with Some l' -> not (Level.eq l l') | None -> true);
+    ectx := Univ.LMap.add l (Some b) !ectx; b
+  in normalize_univ_variable ~find ~update
+
+let normalize_univ_variable_subst subst =
+  let find l = Univ.LMap.find l !subst in
+  let update l b =
+    assert (match Universe.level b with Some l' -> not (Level.eq l l') | None -> true);
+    subst := Univ.LMap.add l b !subst; b in
+    normalize_univ_variable ~find ~update
+
+let normalize_universe_opt_subst subst =
+  let normlevel = normalize_univ_variable_opt_subst subst in
+    subst_univs_universe normlevel
+
+let normalize_universe_subst subst =
+  let normlevel = normalize_univ_variable_subst subst in
+    subst_univs_universe normlevel
+
+type universe_opt_subst = universe option universe_map
+	  
+let make_opt_subst s = 
+  fun x -> 
+    (match Univ.LMap.find x s with
+    | Some u -> u
+    | None -> raise Not_found)
+
+let subst_opt_univs_constr s = 
+  let f = make_opt_subst s in
+    Vars.subst_univs_fn_constr f
+
+let normalize_univ_variables ctx = 
+  let ectx = ref ctx in
+  let normalize = normalize_univ_variable_opt_subst ectx in
+  let _ = Univ.LMap.iter (fun u _ -> ignore(normalize u)) ctx in
+  let undef, def, subst = 
+    Univ.LMap.fold (fun u v (undef, def, subst) -> 
+      match v with
+      | None -> (Univ.LSet.add u undef, def, subst)
+      | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
+    !ectx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
+  in !ectx, undef, def, subst
+
+let pr_universe_body = function
+  | None -> mt ()
+  | Some v -> str" := " ++ Univ.Universe.pr v
+
+let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
+
+let is_defined_var u l = 
+  try
+    match LMap.find u l with
+    | Some _ -> true
+    | None -> false
+  with Not_found -> false
+
+let subst_univs_subst u l s = 
+  LMap.add u l s
+    
+exception Found of Level.t
+let find_inst insts v =
+  try LMap.iter (fun k (enf,alg,v') ->
+    if not alg && enf && Universe.eq v' v then raise (Found k))
+	insts; raise Not_found
+  with Found l -> l
+
+let add_inst u (enf,b,lbound) insts =
+  match lbound with
+  | Some v -> LMap.add u (enf,b,v) insts
+  | None -> insts
+
+exception Stays
+
+let compute_lbound left =
+ (** The universe variable was not fixed yet.
+     Compute its level using its lower bound. *)
+  if CList.is_empty left then None
+  else
+    let lbound = List.fold_left (fun lbound (d, l) -> 
+      if d == Le (* l <= ?u *) then (Universe.sup l lbound)
+      else (* l < ?u *) 
+	(assert (d == Lt); 
+	 (Universe.sup (Universe.super l) lbound)))	    
+      Universe.type0m left
+    in 
+      Some lbound
+  
+let maybe_enforce_leq lbound u cstrs = 
+  match lbound with
+  | Some lbound -> enforce_leq lbound (Universe.make u) cstrs
+  | None -> cstrs
+
+let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) =
+  if enforce then
+    let inst = Universe.make u in
+    let cstrs' = enforce_leq lbound inst cstrs in
+      (ctx, us, LSet.remove u algs, 
+       LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst)
+  else (* Actually instantiate *)
+    (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
+     LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound)
+
+type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
+
+let pr_constraints_map cmap =
+  LMap.fold (fun l cstrs acc -> 
+    Level.pr l ++ str " => " ++ 
+      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl ()
+    ++ acc)
+    cmap (mt ())
+	
+let minimize_univ_variables ctx us algs left right cstrs =
+  let left, lbounds = 
+    Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
+      if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc
+      else (* Fixed universe, just compute its glb for sharing *)
+	let lbounds' = 
+	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
+	  | None -> lbounds
+	  | Some lbound -> LMap.add r (true, false, lbound) lbounds
+	in (Univ.LMap.remove r left, lbounds'))
+      left (left, Univ.LMap.empty)
+  in
+  let rec instance (ctx', us, algs, insts, cstrs as acc) u =
+    let acc, left = 
+      try let l = LMap.find u left in
+	    List.fold_left (fun (acc, left') (d, l) -> 
+	      let acc', (enf,alg,l') = aux acc l in
+		(* if alg then assert(not alg); *)
+		let l' = 
+		  if enf then Universe.make l 
+		  else l' 
+		(* match Universe.level l' with Some _ -> l' | None -> Universe.make l  *)
+		in
+		  acc', (d, l') :: left') (acc, []) l
+      with Not_found -> acc, []
+    and right =
+      try Some (LMap.find u right)
+      with Not_found -> None
+    in
+    let instantiate_lbound lbound =
+      let alg = LSet.mem u algs in
+      if alg then
+	 (* u is algebraic and has no upper bound constraints: we
+	    instantiate it with it's lower bound, if any *)
+	 instantiate_with_lbound u lbound true false acc
+      else (* u is non algebraic *)
+	match Universe.level lbound with
+	| Some l -> (* The lowerbound is directly a level *) 
+	  (* u is not algebraic but has no upper bounds,
+	     we instantiate it with its lower bound if it is a 
+	     different level, otherwise we keep it. *)
+	  if not (Level.eq l u) && not (LSet.mem l algs) then
+	    (* if right = None then. Should check that u does not 
+	       have upper constraints that are not already in right *)
+	      instantiate_with_lbound u lbound false false acc
+	    (* else instantiate_with_lbound u lbound false true acc *)
+	  else
+	    (* assert false: l can't be alg *)
+	    acc, (true, false, lbound)
+	| None -> 
+	  try 
+	    (* if right <> None then raise Not_found; *)
+	    (* Another universe represents the same lower bound, 
+	       we can share them with no harm. *)
+	    let can = find_inst insts lbound in
+	      instantiate_with_lbound u (Universe.make can) false false acc
+	  with Not_found -> 
+	    (* We set u as the canonical universe representing lbound *)
+	    instantiate_with_lbound u lbound false true acc
+    in
+    let acc' acc = 
+      match right with
+      | None -> acc
+      | Some cstrs -> 
+	let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
+	  if List.is_empty dangling then acc
+	  else
+	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in
+	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
+	      if d == Univ.Le then
+		enforce_leq inst (Universe.make r) cstrs
+	      else 
+		try let lev = Option.get (Universe.level inst) in
+		      Constraint.add (lev, d, r) cstrs
+		with Option.IsNone -> assert false)
+	      cstrs dangling
+	    in
+	      (ctx', us, algs, insts, cstrs'), b
+    in
+      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u))
+      else
+	let lbound = compute_lbound left in
+	  match lbound with
+	  | None -> (* Nothing to do *)
+	    acc' (acc, (true, false, Universe.make u))
+	  | Some lbound ->
+	    acc' (instantiate_lbound lbound)
+  and aux (ctx', us, algs, seen, cstrs as acc) u =
+    try acc, LMap.find u seen 
+    with Not_found -> instance acc u
+  in
+    LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> 
+      if v == None then fst (aux acc u)
+      else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
+      us (ctx, us, algs, lbounds, cstrs)
+      
+let normalize_context_set ctx us algs = 
+  let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
+  let uf = UF.create () in
+  let csts = 
+    (* We first put constraints in a normal-form: all self-loops are collapsed
+       to equalities. *)
+    let g = Univ.merge_constraints csts Univ.empty_universes in
+      Univ.constraints_of_universes (Univ.normalize_universes g)
+  in
+  let noneqs =
+    Constraint.fold (fun (l,d,r) noneqs ->
+      if d == Eq then (UF.union l r uf; noneqs) 
+      else Constraint.add (l,d,r) noneqs)
+    csts Constraint.empty
+  in
+  let partition = UF.partition uf in
+  let subst, eqs = List.fold_left (fun (subst, cstrs) s -> 
+    let canon, (global, rigid, flexible) = choose_canonical ctx us algs s in
+    (* Add equalities for globals which can't be merged anymore. *)
+    let cstrs = LSet.fold (fun g cst -> 
+      Constraint.add (canon, Univ.Eq, g) cst) global cstrs 
+    in
+    (** Should this really happen? *)
+    let subst' = LSet.fold (fun f -> LMap.add f canon)
+      (LSet.union rigid flexible) LMap.empty
+    in 
+    let subst = LMap.union subst' subst in
+      (subst, cstrs))
+    (LMap.empty, Constraint.empty) partition
+  in
+  (* Noneqs is now in canonical form w.r.t. equality constraints, 
+     and contains only inequality constraints. *)
+  let noneqs = subst_univs_level_constraints subst noneqs in
+  let us = 
+    LMap.subst_union (LMap.map (fun v -> Some (Universe.make v)) subst) us
+  in
+  (* Compute the left and right set of flexible variables, constraints
+     mentionning other variables remain in noneqs. *)
+  let noneqs, ucstrsl, ucstrsr = 
+    Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> 
+      let lus = LMap.mem l us 
+      and rus = LMap.mem r us
+      in
+      let ucstrsl' = 
+	if lus then add_list_map l (d, r) ucstrsl
+	else ucstrsl
+      and ucstrsr' = 
+	add_list_map r (d, l) ucstrsr
+      in 
+      let noneqs = 
+	if lus || rus then noneq 
+	else Constraint.add cstr noneq
+      in (noneqs, ucstrsl', ucstrsr'))
+    noneqs (Constraint.empty, LMap.empty, LMap.empty)
+  in
+  (* Now we construct the instanciation of each variable. *)
+  let ctx', us, algs, inst, noneqs = 
+    minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
+  in
+  let us = ref us in
+  let norm = normalize_univ_variable_opt_subst us in
+  let _normalize_subst = LMap.iter (fun u v -> ignore(norm u)) !us in
+    (!us, algs), (ctx', Constraint.union noneqs eqs)
+
+(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *)
+(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *)
+
+let universes_of_constr c =
+  let rec aux s c = 
+    match kind_of_term c with
+    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+      LSet.union (Instance.levels u) s
+    | Sort u -> 
+      let u = univ_of_sort u in
+	LSet.union (Universe.levels u) s
+    | _ -> fold_constr aux s c
+  in aux LSet.empty c
+
+let shrink_universe_context (univs,csts) s =
+  let univs' = LSet.inter univs s in
+    Constraint.fold (fun (l,d,r as c) (univs',csts) ->
+      if LSet.mem l univs' then
+	let univs' = if LSet.mem r univs then LSet.add r univs' else univs' in
+	  (univs', Constraint.add c csts)
+      else if LSet.mem r univs' then
+	let univs' = if LSet.mem l univs then LSet.add l univs' else univs' in
+	  (univs', Constraint.add c csts)
+      else (univs', csts))
+      csts (univs',Constraint.empty)
+
+let restrict_universe_context (univs,csts) s =
+  let univs' = LSet.inter univs s in
+  (* Universes that are not necessary to typecheck the term.
+     E.g. univs introduced by tactics and not used in the proof term. *)
+  let diff = LSet.diff univs s in
+  let csts' = 
+    Constraint.fold (fun (l,d,r as c) csts ->
+      if LSet.mem l diff || LSet.mem r diff then csts
+      else Constraint.add c csts)
+      csts Constraint.empty
+  in (univs', csts')
+
+let is_prop_leq (l,d,r) =
+  Level.eq Level.prop l && d == Univ.Le
+
+(* Prop < i <-> Set+1 <= i <-> Set < i *)
+let translate_cstr (l,d,r as cstr) =
+  if Level.eq Level.prop l && d == Univ.Lt then
+    (Level.set, d, r)
+  else cstr
+
+let refresh_constraints univs (ctx, cstrs) =
+  let cstrs', univs' = 
+    Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
+      let c = translate_cstr c in
+      if Univ.check_constraint univs c && not (is_prop_leq c) then acc
+      else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
+      cstrs (Univ.Constraint.empty, univs)
+  in ((ctx, cstrs'), univs')
+
+let remove_trivial_constraints (ctx, cstrs) =
+  let cstrs' = 
+    Univ.Constraint.fold (fun c acc ->
+      if is_prop_leq c then Univ.Constraint.remove c acc
+      else acc) cstrs cstrs
+  in (ctx, cstrs')
diff --git a/library/universes.mli b/library/universes.mli
new file mode 100644
index 000000000..47876269a
--- /dev/null
+++ b/library/universes.mli
@@ -0,0 +1,170 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Pp
+open Names
+open Term
+open Context
+open Environ
+open Locus
+open Univ
+
+(** Universes *)
+val new_univ_level : Names.dir_path -> universe_level
+val set_remote_new_univ_level : universe_level RemoteCounter.installer
+val new_univ : Names.dir_path -> universe
+val new_Type : Names.dir_path -> types
+val new_Type_sort : Names.dir_path -> sorts
+
+(** Build a fresh instance for a given context, its associated substitution and 
+    the instantiated constraints. *)
+
+val fresh_instance_from_context : universe_context -> 
+  (universe_instance * universe_subst) constrained
+
+val fresh_instance_from : universe_context -> 
+  (universe_instance * universe_subst) in_universe_context_set
+
+val new_global_univ : unit -> universe in_universe_context_set
+val new_sort_in_family : sorts_family -> sorts
+
+val fresh_sort_in_family : env -> sorts_family -> 
+  sorts in_universe_context_set
+val fresh_constant_instance : env -> constant -> 
+  pconstant in_universe_context_set
+val fresh_inductive_instance : env -> inductive -> 
+  pinductive in_universe_context_set
+val fresh_constructor_instance : env -> constructor -> 
+  pconstructor in_universe_context_set
+
+val fresh_global_instance : env -> Globnames.global_reference -> 
+  constr in_universe_context_set
+
+val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> 
+  constr in_universe_context_set
+
+(** Raises [Not_found] if not a global reference. *)
+val global_of_constr : constr -> Globnames.global_reference puniverses
+
+val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option
+
+val constr_of_global_univ : Globnames.global_reference puniverses -> constr
+
+val extend_context : 'a in_universe_context_set -> universe_context_set -> 
+  'a in_universe_context_set
+
+(** Simplification and pruning of constraints:
+    [normalize_context_set ctx us]
+
+    - Instantiate the variables in [us] with their most precise
+    universe levels respecting the constraints.
+
+    - Normalizes the context [ctx] w.r.t. equality constraints, 
+    choosing a canonical universe in each equivalence class 
+    (a global one if there is one) and transitively saturate
+    the constraints w.r.t to the equalities. *)
+
+module UF : Unionfind.PartitionSig with type elt = universe_level
+
+type universe_opt_subst = universe option universe_map
+
+val make_opt_subst : universe_opt_subst -> universe_subst_fn
+
+val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
+
+val choose_canonical : universe_set -> universe_opt_subst -> universe_set -> universe_set -> 
+  universe_level * (universe_set * universe_set * universe_set)
+
+val instantiate_with_lbound : 
+  Univ.LMap.key ->
+  Univ.universe ->
+  bool ->
+  bool ->
+  Univ.LSet.t * Univ.universe option Univ.LMap.t *
+    Univ.LSet.t *
+    (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints ->
+  (Univ.LSet.t * Univ.universe option Univ.LMap.t *
+    Univ.LSet.t *
+     (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) *
+    (bool * bool * Univ.universe)
+    
+val compute_lbound : (constraint_type * Univ.universe) list -> universe option
+
+type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
+
+val pr_constraints_map : constraints_map -> Pp.std_ppcmds
+
+val minimize_univ_variables : 
+           Univ.LSet.t ->
+           Univ.universe option Univ.LMap.t ->
+           Univ.LSet.t ->
+  constraints_map -> constraints_map ->
+           Univ.constraints ->
+           Univ.LSet.t * Univ.universe option Univ.LMap.t *
+	     Univ.LSet.t *
+           (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
+
+
+val normalize_context_set : universe_context_set -> 
+  universe_opt_subst (* The defined and undefined variables *) ->
+  universe_set (* univ variables that can be substituted by algebraics *) -> 
+  (universe_opt_subst * universe_set) in_universe_context_set
+
+val normalize_univ_variables : universe_opt_subst -> 
+  universe_opt_subst * universe_set * universe_set * universe_subst
+
+val normalize_univ_variable : 
+  find:(universe_level -> universe) ->
+  update:(universe_level -> universe -> universe) ->
+  universe_level -> universe
+
+val normalize_univ_variable_opt_subst : universe_opt_subst ref ->
+  (universe_level -> universe)
+
+val normalize_univ_variable_subst : universe_subst ref ->
+  (universe_level -> universe)
+
+val normalize_universe_opt_subst : universe_opt_subst ref ->
+  (universe -> universe)
+
+val normalize_universe_subst : universe_subst ref ->
+  (universe -> universe)
+
+(** Create a fresh global in the global environment, shouldn't be done while
+    building polymorphic values as the constraints are added to the global
+    environment already. *)
+
+val constr_of_global : Globnames.global_reference -> constr
+
+val type_of_global : Globnames.global_reference -> types in_universe_context_set
+
+(** Full universes substitutions into terms *)
+
+val nf_evars_and_universes_local : (existential -> constr option) -> universe_level_subst -> 
+  constr -> constr
+
+val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
+  universe_opt_subst -> constr -> constr
+
+(** Get fresh variables for the universe context.
+    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
+val fresh_universe_context_set_instance : universe_context_set -> 
+  universe_level_subst * universe_context_set
+
+val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
+
+(** Shrink a universe context to a restricted set of variables *)
+
+val universes_of_constr : constr -> universe_set
+val shrink_universe_context : universe_context_set -> universe_set -> universe_context_set
+val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
+
+val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
+
+val remove_trivial_constraints : universe_context_set -> universe_context_set