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.

61 files changed, 1081 insertions, 751 deletions

diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml
index c6a96b31a..906f5e383 100644
--- a/plugins/Derive/derive.ml
+++ b/plugins/Derive/derive.ml
@@ -7,14 +7,14 @@
 (************************************************************************)
 
 let interp_init_def_and_relation env sigma init_def r =
-  let init_def = Constrintern.interp_constr sigma env init_def in
+  let init_def, _ = Constrintern.interp_constr sigma env init_def in
   let init_type = Typing.type_of env sigma init_def in
 
   let r_type =
     let open Term in
     mkProd (Names.Anonymous,init_type, mkProd (Names.Anonymous,init_type,mkProp))
   in
-  let r = Constrintern.interp_casted_constr sigma env r r_type in
+  let r, _ = Constrintern.interp_casted_constr sigma env r r_type in
   init_def , init_type , r
   
 
@@ -23,7 +23,7 @@ let interp_init_def_and_relation env sigma init_def r =
     [lemma] as the proof. *)
 let start_deriving f init_def r lemma =
   let env = Global.env () in
-  let kind = Decl_kinds.(Global,DefinitionBody Definition) in
+  let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
   let ( init_def , init_type , r ) =
     interp_init_def_and_relation env Evd.empty init_def r
   in
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index a515deefd..795211c20 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -8,11 +8,37 @@ repeat match goal with
   apply <- andb_true_iff; split
 end.
 
+Arguments decide P /H.
+
 Hint Extern 5 => progress bool.
 
 Ltac define t x H :=
 set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x.
 
+Lemma Decidable_sound : forall P (H : Decidable P),
+                          decide P = true -> P.
+Proof.
+intros P H Hp; apply -> Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_complete : forall P (H : Decidable P),
+  P -> decide P = true.
+Proof.
+intros P H Hp; apply <- Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_sound_alt : forall P (H : Decidable P),
+   ~ P -> decide P = false.
+Proof.
+intros P [wit spec] Hd; destruct wit; simpl; tauto. 
+Qed.
+
+Lemma Decidable_complete_alt : forall P (H : Decidable P),
+  decide P = false -> ~ P.
+Proof.
+  intros P [wit spec] Hd Hc; simpl in *; intuition congruence.
+Qed.
+
 Ltac try_rewrite :=
 repeat match goal with
 | [ H : ?P |- _ ] => rewrite H
@@ -142,6 +168,7 @@ end.
 Program Instance Decidable_eq_poly : forall (p q : poly), Decidable (eq p q) := {
   Decidable_witness := beq_poly p q
 }.
+
 Next Obligation.
 split.
 revert q; induction p; intros [] ?; simpl in *; bool; try_decide;
@@ -185,8 +212,8 @@ Program Instance Decidable_valid : forall n p, Decidable (valid n p) := {
 }.
 Next Obligation.
 split.
-  revert n; induction p; simpl in *; intuition; bool; try_decide; auto.
-  intros H; induction H; simpl in *; bool; try_decide; auto.
+  revert n; induction p; unfold valid_dec in *; intuition; bool; try_decide; auto.
+  intros H; induction H; unfold valid_dec in *; bool; try_decide; auto.
 Qed.
 
 (** Basic algebra *)
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index b81821a2e..6a0f4d852 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -3,7 +3,7 @@ let contrib_name = "btauto"
 
 let init_constant dir s =
   let find_constant contrib dir s =
-    Globnames.constr_of_global (Coqlib.find_reference contrib dir s)
+    Universes.constr_of_global (Coqlib.find_reference contrib dir s)
   in
   find_constant contrib_name dir s
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 046ecf775..c726fd5de 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -123,7 +123,7 @@ module PacMap=Map.Make(PacOrd)
 module PafMap=Map.Make(PafOrd)
 
 type cinfo=
-    {ci_constr: constructor; (* inductive type *)
+    {ci_constr: pconstructor; (* inductive type *)
      ci_arity: int;     (* # args *)
      ci_nhyps: int}     (* # projectable args *)
 
@@ -142,13 +142,13 @@ type term=
 
 let rec term_equal t1 t2 =
   match t1, t2 with
-    | Symb c1, Symb c2 -> eq_constr c1 c2
+    | Symb c1, Symb c2 -> eq_constr_nounivs c1 c2
     | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2
     | Eps i1, Eps i2 -> Id.equal i1 i2
     | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
-    | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
-      Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
-      Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2
+    | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1},
+      Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} ->
+      Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *)
     | _ -> false
 
 open Hashset.Combine
@@ -163,7 +163,7 @@ let rec hash_term = function
   | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2)
   | Eps i -> combine 3 (Id.hash i)
   | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
-  | Constructor {ci_constr=c; ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
+  | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
 
 type ccpattern =
     PApp of term * ccpattern list (* arguments are reversed *)
@@ -234,7 +234,7 @@ type node =
 
 module Constrhash = Hashtbl.Make
   (struct type t = constr
-	  let equal = eq_constr
+	  let equal = eq_constr_nounivs
 	  let hash = hash_constr
    end)
 module Typehash = Constrhash
@@ -404,32 +404,50 @@ let _B_ = Name (Id.of_string "A")
 let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
 
 let cc_product s1 s2 =
-  mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
-	   mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
+  mkLambda(_A_,mkSort(Universes.new_sort_in_family s1),
+	   mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_))
 
 let rec constr_of_term = function
-    Symb s->s
+    Symb s-> applist_projection s []
   | Product(s1,s2) -> cc_product s1 s2
   | Eps id -> mkVar id
-  | Constructor cinfo -> mkConstruct cinfo.ci_constr
+  | Constructor cinfo -> mkConstructU cinfo.ci_constr
   | Appli (s1,s2)->
       make_app [(constr_of_term s2)] s1
 and make_app l=function
     Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
-  | other -> applistc (constr_of_term other) l
+  | other -> 
+    applist_proj other l
+and applist_proj c l =
+  match c with
+  | Symb s -> applist_projection s l
+  | _ -> applistc (constr_of_term c) l
+and applist_projection c l =
+  match kind_of_term c with
+  | Const c when Environ.is_projection (fst c) (Global.env()) ->
+    (match l with 
+    | [] -> (* Expand the projection *)
+      let kn = fst c in
+      let ty,_ = Typeops.type_of_constant (Global.env ()) c in
+      let pb = Environ.lookup_projection kn (Global.env()) in
+      let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
+	it_mkLambda_or_LetIn (mkProj(kn,mkRel 1)) ctx
+    | hd :: tl ->
+      applistc (mkProj (fst c, hd)) tl)
+  | _ -> applistc c l
 
 let rec canonize_name c =
   let func =  canonize_name in
     match kind_of_term c with
-      | Const kn ->
+      | Const (kn,u) ->
 	  let canon_const = constant_of_kn (canonical_con kn) in 
-	    (mkConst canon_const)
-      | Ind (kn,i) ->
+	    (mkConstU (canon_const,u))
+      | Ind ((kn,i),u) ->
 	  let canon_mind = mind_of_kn (canonical_mind kn) in
-	    (mkInd (canon_mind,i))
-      | Construct ((kn,i),j) ->
+	    (mkIndU ((canon_mind,i),u))
+      | Construct (((kn,i),j),u) ->
 	  let canon_mind = mind_of_kn (canonical_mind kn) in
-	    mkConstruct ((canon_mind,i),j) 
+	    mkConstructU (((canon_mind,i),j),u)
       | Prod (na,t,ct) ->
 	  mkProd (na,func t, func ct)
       | Lambda (na,t,ct) ->
@@ -438,6 +456,9 @@ let rec canonize_name c =
 	  mkLetIn (na, func b,func t,func ct)
       | App (ct,l) ->
 	  mkApp (func ct,Array.smartmap func l)
+      | Proj(kn,c) ->
+        let canon_const = constant_of_kn (canonical_con kn) in 
+	  (mkProj (canon_const, func c))
       | _ -> c
 
 (* rebuild a term from a pattern and a substitution *)
@@ -469,7 +490,7 @@ let rec add_term state t=
     try Termhash.find uf.syms t with
 	Not_found ->
 	  let b=next uf in
-          let trm = Termops.refresh_universes (constr_of_term t) in
+          let trm = constr_of_term t in
 	  let typ = pf_type_of state.gls trm in
 	  let typ = canonize_name typ in
 	  let new_node=
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 5d286c732..0c5d6ca1f 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -11,7 +11,7 @@ open Term
 open Names
 
 type cinfo =
-    {ci_constr: constructor; (* inductive type *)
+    {ci_constr: pconstructor; (* inductive type *)
      ci_arity: int;     (* # args *)
      ci_nhyps: int}     (* # projectable args *)
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 5244dcf17..4e1806f5a 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -20,7 +20,7 @@ type rule=
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
-  | Inject of proof*constructor*int*int
+  | Inject of proof*pconstructor*int*int
 and proof =
     {p_lhs:term;p_rhs:term;p_rule:rule}
 
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index b8a8d229a..50e3624d0 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -16,7 +16,7 @@ type rule=
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
-  | Inject of proof*constructor*int*int
+  | Inject of proof*pconstructor*int*int
 and proof =
     private {p_lhs:term;p_rhs:term;p_rule:rule}
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index ac148fe18..783abc5d8 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -23,21 +23,17 @@ open Pp
 open Errors
 open Util
 
-let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
-
-let _f_equal = constant ["Init";"Logic"] "f_equal"
-
-let _eq_rect = constant ["Init";"Logic"] "eq_rect"
-
-let _refl_equal = constant ["Init";"Logic"] "eq_refl"
-
-let _sym_eq = constant ["Init";"Logic"] "eq_sym"
-
-let _trans_eq = constant ["Init";"Logic"] "eq_trans"
-
-let _eq = constant ["Init";"Logic"] "eq"
-
-let _False = constant ["Init";"Logic"] "False"
+let reference dir s = Coqlib.gen_reference "CC" dir s
+
+let _f_equal = reference ["Init";"Logic"] "f_equal"
+let _eq_rect = reference ["Init";"Logic"] "eq_rect"
+let _refl_equal = reference ["Init";"Logic"] "eq_refl"
+let _sym_eq = reference ["Init";"Logic"] "eq_sym"
+let _trans_eq = reference ["Init";"Logic"] "eq_trans"
+let _eq = reference ["Init";"Logic"] "eq"
+let _False = reference ["Init";"Logic"] "False"
+let _True = reference ["Init";"Logic"] "True"
+let _I = reference ["Init";"Logic"] "I"
 
 let whd env=
   let infos=Closure.create_clos_infos Closure.betaiotazeta env in
@@ -64,32 +60,36 @@ let rec decompose_term env sigma t=
 	Appli(Appli(Product (sort_a,sort_b) ,
 		    decompose_term env sigma a),
 	      decompose_term env sigma b)
-    | Construct c->
-	let (mind,i_ind),i_con = c in 
+    | Construct c ->
+	let (((mind,i_ind),i_con),u)= c in 
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
 	let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in
-	  Constructor {ci_constr= (canon_ind,i_con);
+	  Constructor {ci_constr= ((canon_ind,i_con),u);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}
     | Ind c -> 
-	let mind,i_ind = c in 
+	let (mind,i_ind),u = c in 
 	let canon_mind = mind_of_kn (canonical_mind mind) in
-	let canon_ind = canon_mind,i_ind in  (Symb (mkInd canon_ind))
-    | Const c -> 
+	let canon_ind = canon_mind,i_ind in  (Symb (mkIndU (canon_ind,u)))
+    | Const (c,u) -> 
 	let canon_const = constant_of_kn (canonical_con c) in 
-	  (Symb (mkConst canon_const))
+	  (Symb (mkConstU (canon_const,u)))
+    | Proj (p, c) -> 
+	let canon_const = constant_of_kn (canonical_con p) in 
+	  (Appli (Symb (mkConst canon_const), decompose_term env sigma c))
     | _ ->if closed0 t then (Symb t) else raise Not_found
 
 (* decompose equality in members and type *)
+open Globnames
 
 let atom_of_constr env sigma term =
   let wh =  (whd_delta env term) in
   let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	  if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
+	if is_global _eq f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -124,7 +124,7 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
+	if is_global _eq f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
@@ -145,7 +145,7 @@ let patterns_of_constr env sigma nrels term=
 let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
       Prod (id,atom,ff) -> 
-	if eq_constr ff (Lazy.force _False) then
+	if is_global _False ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
@@ -157,7 +157,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
     | Prod (id,atom,ff) -> 
-	if eq_constr ff (Lazy.force _False) then
+	if is_global _False ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
@@ -218,13 +218,13 @@ let make_prb gls depth additionnal_terms =
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
-let build_projection intype outtype (cstr:constructor) special default gls=
+let build_projection intype outtype (cstr:pconstructor) special default gls=
   let env=pf_env gls in
   let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in
-  let ind=destInd h in
-  let types=Inductiveops.arities_of_constructors env ind in
+  let ind,u=destInd h in
+  let types=Inductiveops.arities_of_constructors env (ind,u) in
   let lp=Array.length types in
-  let ci=pred (snd cstr) in
+  let ci=pred (snd(fst cstr)) in
   let branch i=
     let ti= prod_appvect types.(i) argv in
     let rc=fst (decompose_prod_assum ti) in
@@ -243,60 +243,67 @@ let build_projection intype outtype (cstr:constructor) special default gls=
 
 let _M =mkMeta
 
+let app_global f args k = 
+  Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+
+let new_app_global f args k = 
+  Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+
+let new_exact_check c = Proofview.V82.tactic (exact_check c)
+let new_refine c = Proofview.V82.tactic (refine c)
+
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
   let type_of = Tacmach.New.pf_type_of gl in
+  try (* type_of can raise exceptions *)
   match p.p_rule with
-      Ax c -> Proofview.V82.tactic (exact_check c)
+      Ax c -> new_exact_check c
     | SymAx c ->
         Proofview.V82.tactic begin fun gls ->
-	  let l=constr_of_term p.p_lhs and
-	      r=constr_of_term p.p_rhs in
-          let typ = Termops.refresh_universes (pf_type_of gls l) in
-	  exact_check
-	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
+	let l=constr_of_term p.p_lhs and
+	    r=constr_of_term p.p_rhs in
+        let typ = (* Termops.refresh_universes *)pf_type_of gls l in
+	  (app_global _sym_eq [|typ;r;l;c|] exact_check) gls
         end
     | Refl t ->
         Proofview.V82.tactic begin fun gls ->
-	  let lr = constr_of_term t in
-	  let typ = Termops.refresh_universes (pf_type_of gls lr) in
-	  exact_check
-	    (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
+	let lr = constr_of_term t in
+	let typ = (* Termops.refresh_universes *) (pf_type_of gls lr) in
+	  (app_global _refl_equal [|typ;constr_of_term t|] exact_check) gls
         end
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = Termops.refresh_universes (type_of t2) in
-	let prf =
-	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
-	  Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) [(proof_tac p1);(proof_tac p2)]
+	let typ = (* Termops.refresh_universes *) (type_of t2) in
+	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
+          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	and tx1=constr_of_term p2.p_lhs
 	and tf2=constr_of_term p1.p_rhs
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = Termops.refresh_universes (type_of tf1) in
-	let typx = Termops.refresh_universes (type_of tx1) in
-	let typfx = Termops.refresh_universes (type_of (mkApp (tf1,[|tx1|]))) in
+	let typf = (* Termops.refresh_universes  *)(type_of tf1) in
+	let typx = (* Termops.refresh_universes *) (type_of tx1) in
+	let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in
         let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
-	  mkApp(Lazy.force _f_equal,
-		[|typf;typfx;appx1;tf1;tf2;_M 1|]) in
+	  app_global _f_equal
+		[|typf;typfx;appx1;tf1;tf2;_M 1|] in
 	let lemma2=
-	  mkApp(Lazy.force _f_equal,
-		[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
+	  app_global _f_equal
+		[|typx;typfx;tf2;tx1;tx2;_M 1|] in
 	let prf =
-	  mkApp(Lazy.force _trans_eq,
+	  app_global _trans_eq
 		[|typfx;
 		  mkApp(tf1,[|tx1|]);
 		  mkApp(tf2,[|tx1|]);
-		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
-	  Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf))
-	    [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma1)) (proof_tac p1);
+		  mkApp(tf2,[|tx2|]);_M 2;_M 3|] in
+	  Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine))
+	    [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1);
   	     Tacticals.New.tclFIRST
-	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma2)) (proof_tac p2);
+	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
 		reflexivity;
                 Proofview.tclZERO (UserError ("Congruence" ,
 		    (Pp.str
@@ -305,46 +312,48 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype = Termops.refresh_universes (type_of ti) in
-	 let outtype = Termops.refresh_universes (type_of default) in
+	 let intype = (* Termops.refresh_universes *) (type_of ti) in
+	 let outtype = (* Termops.refresh_universes *) (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
          let proj =
            Tacmach.New.of_old (build_projection intype outtype cstr special default) gl
          in
 	 let injt=
-	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf)
+           app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let refute_tac c t1 t2 p =
   Proofview.Goal.enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let intype =
-    Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) gl
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl
   in
-  let neweq=
-    mkApp(Lazy.force _eq,
-	  [|intype;tt1;tt2|]) in
+  let neweq= new_app_global _eq [|intype;tt1;tt2|] in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
-    Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
+    Tacticals.New.tclTHENS (neweq (assert_tac (Name hid)))
       [proof_tac p; simplest_elim false_t]
   end
 
+let refine_exact_check c gl =
+  let evm, _ = pf_apply e_type_of gl c in
+    Tacticals.tclTHEN (Refiner.tclEVARS evm) (exact_check c) gl
+
 let convert_to_goal_tac c t1 t2 p = 
   Proofview.Goal.enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let sort =
-    Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) gl
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl
   in
-  let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
+  let neweq= new_app_global _eq [|sort;tt1;tt2|] in
   let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
   let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
   let identity=mkLambda (Name x,sort,mkRel 1) in
-  let endt=mkApp (Lazy.force _eq_rect,
-		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
-    Tacticals.New.tclTHENS (assert_tac (Name e) neweq)
-      [proof_tac p; Proofview.V82.tactic (exact_check endt)]
+  let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+    Tacticals.New.tclTHENS (neweq (assert_tac (Name e)))
+      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
   end
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -357,29 +366,36 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
        simplest_elim false_t]
   end
 
-let discriminate_tac cstr p =
+let discriminate_tac (cstr,u as cstru) p =
   Proofview.Goal.enter begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
     let intype =
-      Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) gl
+      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl
     in
     let concl = Proofview.Goal.concl gl in
-    let outsort = mkType (Termops.new_univ ()) in
+    (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
+    (* let outsort = mkSort outsort in *)
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-    let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in
-    let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
-    let trivial = Tacmach.New.of_old (fun gls -> pf_type_of gls identity) gl in
-    let outtype = mkType (Termops.new_univ ()) in
+    (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
+    (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
+    let identity = Universes.constr_of_global _I in
+    (* let trivial=pf_type_of gls identity in *)
+    let trivial = Universes.constr_of_global _True in
+    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
+    let outtype = mkSort outtype in
     let pred=mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
-    let proj = Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) gl in
-    let injt=mkApp (Lazy.force _f_equal,
-		    [|intype;outtype;proj;t1;t2;mkVar hid|]) in
-    let endt=mkApp (Lazy.force _eq_rect,
-		    [|outtype;trivial;pred;identity;concl;injt|]) in
-    let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
-    Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
-      [proof_tac p; Proofview.V82.tactic (exact_check endt)]
+    let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in
+    let injt=app_global _f_equal
+                    [|intype;outtype;proj;t1;t2;mkVar hid|] in
+    let endt k =
+      injt (fun injt ->
+        app_global _eq_rect
+          [|outtype;trivial;pred;identity;concl;injt|] k) in
+    let neweq=new_app_global _eq [|intype;t1;t2|] in
+    Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evm)
+      (Tacticals.New.tclTHENS (neweq (assert_tac (Name hid)))
+        [proof_tac p; Proofview.V82.tactic (endt exact_check)])
   end
 
 (* wrap everything *)
@@ -389,7 +405,7 @@ let build_term_to_complete uf meta pac =
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
   let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
-    applistc (mkConstruct cinfo.ci_constr) all_args
+    applistc (mkConstructU cinfo.ci_constr) all_args
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter begin fun gl ->
@@ -457,7 +473,7 @@ let congruence_tac depth l =
    might be slow now, let's rather do something equivalent
    to a "simple apply refl_equal" *)
 
-let simple_reflexivity () = apply (Lazy.force _refl_equal)
+let simple_reflexivity () = apply (Universes.constr_of_global _refl_equal)
 
 (* The [f_equal] tactic.
 
@@ -472,15 +488,17 @@ let f_equal =
     let type_of = Tacmach.New.pf_type_of gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
-        let ty = Termops.refresh_universes (type_of c1) in
-        Tacticals.New.tclTRY (Tacticals.New.tclTHEN
-          (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
-          (Tacticals.New.tclTRY (Proofview.V82.tactic (simple_reflexivity ()))))
+        let ty = (* Termops.refresh_universes *) (type_of c1) in
+        if eq_constr_nounivs c1 c2 then Proofview.tclUNIT ()
+        else
+          Tacticals.New.tclTRY (Tacticals.New.tclTHEN
+          ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
+          (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) (fun c -> Proofview.V82.tactic (apply c)))))
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
       begin match kind_of_term concl with
-      | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
+      | App (r,[|_;t;t'|]) when Globnames.is_global _eq r ->
 	  begin match kind_of_term t, kind_of_term t' with
 	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index a022a07da..7c1d9f1c0 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -1,3 +1,4 @@
+
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 505d7dba5..e0aee15e6 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -144,26 +144,26 @@ let intern_proof_instr globs instr=
 (* INTERP *)
 
 let interp_justification_items sigma env =
-    Option.map (List.map (fun c ->understand sigma env (fst c)))
+    Option.map (List.map (fun c -> fst (*FIXME*)(understand sigma env (fst c))))
 
 let interp_constr check_sort sigma env c =
   if check_sort then
-    understand sigma env ~expected_type:IsType (fst c)
+    fst (understand sigma env ~expected_type:IsType (fst c) (* FIXME *))
   else
-    understand sigma env (fst c)
+    fst (understand sigma env (fst c))
 
 let special_whd env =
   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
-let _eq = Globnames.constr_of_global (Coqlib.glob_eq)
+let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
 
 let decompose_eq env id =
   let typ = Environ.named_type id env in
   let whd = special_whd env typ in
     match kind_of_term whd with
 	App (f,args)->
-	  if eq_constr f _eq && Int.equal (Array.length args) 3
+	  if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
 	  then args.(0)
 	  else error "Previous step is not an equality."
       | _ -> error "Previous step is not an equality."
@@ -173,7 +173,7 @@ let get_eq_typ info env =
     typ
 
 let interp_constr_in_type typ sigma env c =
-  understand sigma env (fst c) ~expected_type:(OfType typ)
+  fst (understand sigma env (fst c) ~expected_type:(OfType typ))(*FIXME*)
 
 let interp_statement interp_it sigma env st =
   {st_label=st.st_label;
@@ -213,7 +213,7 @@ let rec match_hyps blend names constr = function
 	qhyp::rhyps,head
 
 let interp_hyps_gen inject blend sigma env hyps head =
-  let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in
+  let constr= fst(*FIXME*) (understand sigma env (glob_constr_of_hyps inject hyps head)) in
     match_hyps blend [] constr hyps
 
 let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop)
@@ -246,7 +246,7 @@ let rec glob_of_pat =
 	    add_params (pred n) (GHole(Loc.ghost,
 				       Evar_kinds.TomatchTypeParameter(ind,n), None)::q) in
 	    let args = List.map glob_of_pat lpat in
-	      glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr),
+	      glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None),
 		   add_params mind.Declarations.mind_nparams args)
 
 let prod_one_hyp = function
@@ -333,7 +333,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	     (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
   let app_ind =
-    let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in
+    let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in
     let rparams = List.map detype_ground pinfo.per_params in
     let rparams_rec =
       List.map
@@ -365,7 +365,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
-  let constr = understand  sigma env term5 in
+  let constr = fst (understand  sigma env term5)(*FIXME*) in
   let tparams,nam4,rest4 = match_args destProd [] constr params in
   let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
   let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
@@ -409,7 +409,7 @@ let interp_suffices_clause sigma env (hyps,cot)=
     nenv,res
 
 let interp_casee sigma env = function
-    Real c -> Real (understand sigma env (fst c))
+    Real c -> Real (fst (understand sigma env (fst c)))(*FIXME*)
   | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut)
 
 let abstract_one_arg = function
@@ -425,7 +425,7 @@ let glob_constr_of_fun args body =
   List.fold_right abstract_one_arg args (fst body)
 
 let interp_fun sigma env args body =
-  let constr=understand sigma env (glob_constr_of_fun args body) in
+  let constr=fst (*FIXME*) (understand sigma env (glob_constr_of_fun args body)) in
     match_args destLambda [] constr args
 
 let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function
@@ -448,7 +448,7 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu
       let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in
 	Pcase (tparams,tpat,thyps)
   | Ptake witl ->
-      Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
+      Ptake (List.map (fun c -> fst (*FIXME*) (understand sigma env (fst c))) witl)
   | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c,
 				     interp_hyps sigma env hyps)
   | Pper (et,c) -> Pper (et,interp_casee sigma env c)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index de57330ec..8647ca676 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -292,13 +292,13 @@ let rec replace_in_list m l = function
 let enstack_subsubgoals env se stack gls=
   let hd,params = decompose_app (special_whd gls se.se_type) in
     match kind_of_term hd with
-	Ind ind when is_good_inductive env ind ->
+	Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *)
 	  let mib,oib=
 	    Inductive.lookup_mind_specif env ind in
           let gentypes=
-            Inductive.arities_of_constructors ind (mib,oib) in
+            Inductive.arities_of_constructors indu (mib,oib) in
 	  let process i gentyp =
-	    let constructor = mkConstruct(ind,succ i)
+	    let constructor = mkConstructU ((ind,succ i),u)
 	      (* constructors numbering*) in
 	    let appterm = applist (constructor,params) in
 	    let apptype = prod_applist gentyp params in
@@ -357,7 +357,7 @@ let find_subsubgoal c ctyp skip submetas gls =
       try
 	let unifier =
 	  Unification.w_unify env se.se_evd Reduction.CUMUL
-	    ~flags:Unification.elim_flags ctyp se.se_type in
+	    ~flags:(Unification.elim_flags ()) ctyp se.se_type in
 	  if n <= 0 then
 	      {se with
 		 se_evd=meta_assign se.se_meta
@@ -488,14 +488,14 @@ let instr_cut mkstat _thus _then cut gls0 =
 
 
 (* iterated equality *)
-let _eq = Globnames.constr_of_global (Coqlib.glob_eq)
+let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
 
 let decompose_eq id gls =
   let typ = pf_get_hyp_typ gls id in
   let whd =  (special_whd gls typ) in
     match kind_of_term whd with
 	App (f,args)->
-	  if eq_constr f _eq && Int.equal (Array.length args) 3
+	  if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
 	  then (args.(0),
 		args.(1),
 		args.(2))
@@ -530,14 +530,14 @@ let instr_rew _thus rew_side cut gls0 =
     else tclIDTAC gls in
     match rew_side with
 	Lhs ->
-	  let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
+	  let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in
 	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
 	      [tclTHEN tcl_erase_info
 		 (tclTHENS (Proofview.V82.of_tactic (transitivity lhs))
 		    [just_tac;exact_check (mkVar last_id)]);
 	       thus_tac new_eq] gls0
       | Rhs ->
-	  let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
+	  let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
 	    tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
 	      [tclTHEN tcl_erase_info
 		 (tclTHENS (Proofview.V82.of_tactic (transitivity rhs))
@@ -663,11 +663,11 @@ let conjunction_arity id gls =
   let hd,params = decompose_app (special_whd gls typ) in
   let env =pf_env gls in
     match kind_of_term hd with
-	Ind ind when is_good_inductive env ind ->
+	Ind (ind,u as indu) when is_good_inductive env ind ->
 	  let mib,oib=
 	    Inductive.lookup_mind_specif env ind in
           let gentypes=
-            Inductive.arities_of_constructors ind (mib,oib) in
+            Inductive.arities_of_constructors indu (mib,oib) in
 	  let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in
 	  let apptype = prod_applist gentypes.(0) params in
 	  let rc,_ = Reduction.dest_prod env apptype in
@@ -832,7 +832,7 @@ let build_per_info etype casee gls =
   let ctyp=pf_type_of gls casee in
   let is_dep = dependent casee concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
-  let ind =
+  let (ind,u as indu) =
     try
       destInd hd
     with DestKO ->
@@ -1031,7 +1031,7 @@ let rec st_assoc id = function
 let thesis_for obj typ per_info env=
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
-  let ind = destInd cind in
+  let ind,u = destInd cind in
   let _ = if not (eq_ind ind per_info.per_ind) then
     errorlabstrm "thesis_for"
       ((Printer.pr_constr_env env obj) ++ spc () ++
@@ -1166,7 +1166,7 @@ let hrec_for fix_id per_info gls obj_id =
   let typ=pf_get_hyp_typ gls obj_id in
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
-  let ind = destInd cind in assert (eq_ind ind per_info.per_ind);
+  let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind);
   let params,args= List.chop per_info.per_nparams all_args in
   assert begin
     try List.for_all2 eq_constr params per_info.per_params with
@@ -1205,7 +1205,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let env=pf_env gls in
 	let ctyp=pf_type_of gls casee in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
-	let _ = assert (eq_ind (destInd hd) ind) in (* just in case *)
+	let ind', u = destInd hd in
+	let _ = assert (eq_ind ind' ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
 	  let typ=pf_type_of gls c in
@@ -1213,7 +1214,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let elim_pred = List.fold_right abstract_obj
 	  real_args (lambda_create env (ctyp,subst_term casee concl)) in
 	let case_info = Inductiveops.make_case_info env ind RegularStyle in
-	let gen_arities = Inductive.arities_of_constructors ind spec in
+	let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
 	let f_ids typ =
 	  let sign =
 	    (prod_assum (prod_applist typ params)) in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 7c9ef3c2a..36abb86cc 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -176,7 +176,7 @@ GLOBAL: proof_instr;
   statement :
     [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
      | i=ident -> {st_label=Anonymous;
-		   st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i))}
+		   st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)}
      | c=constr -> {st_label=Anonymous;st_it=c}
      ]];
   constr_or_thesis :
@@ -189,7 +189,7 @@ GLOBAL: proof_instr;
     |
       [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
       | i=ident -> {st_label=Anonymous;
-		    st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i)))}
+		    st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))}
       | c=constr -> {st_label=Anonymous;st_it=This c}
       ]
     ];
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 791294902..74de31368 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -131,7 +131,7 @@ end
 exception Impossible
 
 let check_arity env cb =
-  let t = Typeops.type_of_constant_type env cb.const_type in
+  let t = cb.const_type in
   if Reduction.is_arity env t then raise Impossible
 
 let check_fix env cb i =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3927ad328..5b79f6d78 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -203,27 +203,28 @@ let oib_equal o1 o2 =
   Id.equal o1.mind_typename o2.mind_typename &&
   List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
   begin match o1.mind_arity, o2.mind_arity with
-  | Monomorphic {mind_user_arity=c1; mind_sort=s1},
-    Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
+  (* | Monomorphic {mind_user_arity=c1; mind_sort=s1}, *)
+  (*   Monomorphic {mind_user_arity=c2; mind_sort=s2} -> *)
+  (*     eq_constr c1 c2 && Sorts.equal s1 s2 *)
+  (* | ma1, ma2 -> Pervasives.(=) ma1 ma2 (\** FIXME: this one is surely wrong *\) end && *)
+  (*   Array.equal Id.equal o1.mind_consnames o2.mind_consnames *)
+  | {mind_user_arity=c1; mind_sort=s1},
+    {mind_user_arity=c2; mind_sort=s2} ->
       eq_constr c1 c2 && Sorts.equal s1 s2
-  | Polymorphic p1, Polymorphic p2 ->
-    let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in
-    List.equal eq p1.poly_param_levels p2.poly_param_levels &&
-    Univ.Universe.equal p1.poly_level p2.poly_level
-  | Monomorphic _, Polymorphic _ | Polymorphic _, Monomorphic _ -> false
   end &&
   Array.equal Id.equal o1.mind_consnames o2.mind_consnames
 
 let mib_equal m1 m2 =
   Array.equal oib_equal m1.mind_packets m1.mind_packets &&
-  (m1.mind_record : bool) == m2.mind_record &&
+  (m1.mind_record) = m2.mind_record && (*FIXME*)
   (m1.mind_finite : bool) == m2.mind_finite &&
   Int.equal m1.mind_ntypes m2.mind_ntypes &&
   List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
   Int.equal m1.mind_nparams m2.mind_nparams &&
   Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
   List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
-  Univ.eq_constraint m1.mind_constraints m2.mind_constraints
+  Pervasives.(=) m1.mind_universes m2.mind_universes (** FIXME *)
+  (* m1.mind_universes = m2.mind_universes *)
 
 (*S Extraction of a type. *)
 
@@ -278,10 +279,10 @@ let rec extract_type env db j c args =
 	       if n > List.length db then Tunknown
 	       else let n' = List.nth db (n-1) in
 	       if Int.equal n' 0 then Tunknown else Tvar n')
-    | Const kn ->
+    | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-	let typ = Typeops.type_of_constant_type env cb.const_type in
+	let typ,_ = Typeops.type_of_constant env c in
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
@@ -306,7 +307,7 @@ let rec extract_type env db j c args =
 		      (* We try to reduce. *)
 		      let newc = applist (Mod_subst.force_constr lbody, args) in
 		      extract_type env db j newc []))
-    | Ind (kn,i) ->
+    | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
@@ -388,8 +389,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     let packets =
       Array.mapi
 	(fun i mip ->
-	   let ar = Inductive.type_of_inductive env (mib,mip) in
-	   let info = (fst (flag_of_type env ar) == Info) in
+	   let (ind,u), ctx = 
+	     Universes.fresh_inductive_instance env (kn,i) in
+	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
+	   let info = (fst (flag_of_type env ar) = Info) in
 	   let s,v = if info then type_sign_vl env ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
 	   { ip_typename = mip.mind_typename;
@@ -397,21 +400,21 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ip_logical = not info;
 	     ip_sign = s;
 	     ip_vars = v;
-	     ip_types = t })
+	     ip_types = t }, u)
 	mib.mind_packets
     in
 
     add_ind kn mib
       {ind_kind = Standard;
        ind_nparams = npar;
-       ind_packets = packets;
+       ind_packets = Array.map fst packets;
        ind_equiv = equiv
       };
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let p = packets.(i) in
+      let p,u = packets.(i) in
       if not p.ip_logical then
-	let types = arities_of_constructors env (kn,i) in
+	let types = arities_of_constructors env ((kn,i),u) in
 	for j = 0 to Array.length types - 1 do
 	  let t = snd (decompose_prod_n npar types.(j)) in
 	  let prods,head = dest_prod epar t in
@@ -433,7 +436,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	if is_custom r then raise (I Standard);
 	if not mib.mind_finite then raise (I Coinductive);
 	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
-	let p = packets.(0) in
+	let p,u = packets.(0) in
 	if p.ip_logical then raise (I Standard);
 	if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard);
 	let typ = p.ip_types.(0) in
@@ -442,7 +445,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	    Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
 	then raise (I Singleton);
 	if List.is_empty l then raise (I Standard);
-	if not mib.mind_record then raise (I Standard);
+	if Option.is_empty mib.mind_record then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
 	let rec names_prod t = match kind_of_term t with
@@ -476,7 +479,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	(* If so, we use this information. *)
 	begin try
 	  let n = nb_default_params env
-            (Inductive.type_of_inductive env (mib,mip0))
+            (Inductive.type_of_inductive env ((mib,mip0),u))
 	  in
 	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn in
 	  List.iter (Option.iter check_proj) (lookup_projections ip)
@@ -487,7 +490,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     in
     let i = {ind_kind = ind_info;
 	     ind_nparams = npar;
-	     ind_packets = packets;
+	     ind_packets = Array.map fst packets;
 	     ind_equiv = equiv }
     in
     add_ind kn mib i;
@@ -522,7 +525,7 @@ and mlt_env env r = match r with
 	   | _ -> None
        with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
-	 let typ = Typeops.type_of_constant_type env cb.const_type in
+	 let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in
 	 match cb.const_body with
 	   | Undef _ | OpaqueDef _ -> None
 	   | Def l_body ->
@@ -550,7 +553,7 @@ let record_constant_type env kn opt_typ =
     lookup_type kn
   with Not_found ->
     let typ = match opt_typ with
-      | None -> Typeops.type_of_constant env kn
+      | None -> (lookup_constant kn env).const_type
       | Some typ -> typ
     in let mlt = extract_type env [] 1 typ []
     in let schema = (type_maxvar mlt, mlt)
@@ -605,10 +608,12 @@ let rec extract_term env mle mlt c args =
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
-    | Const kn ->
-	extract_cst_app env mle mlt kn args
-    | Construct cp ->
-	extract_cons_app env mle mlt cp args
+    | Const (kn,u) ->
+	extract_cst_app env mle mlt kn u args
+    | Construct (cp,u) ->
+	extract_cons_app env mle mlt cp u args
+    | Proj (p, c) ->
+        extract_cst_app env mle mlt p Univ.Instance.empty (c :: args)
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
@@ -656,7 +661,7 @@ and make_mlargs env e s args typs =
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn args =
+and extract_cst_app env mle mlt kn u args =
   (* First, the [ml_schema] of the constant, in expanded version. *)
   let nb,t = record_constant_type env kn None in
   let schema = nb, expand env t in
@@ -729,7 +734,7 @@ and extract_cst_app env mle mlt kn args =
    they are fixed, and thus are not used for the computation.
    \end{itemize} *)
 
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
   (* First, we build the type of the constructor, stored in small pieces. *)
   let mi = extract_ind env kn in
   let params_nb = mi.ind_nparams in
@@ -971,7 +976,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 
 let extract_constant env kn cb =
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = cb.const_type in
   let warn_info () = if not (is_custom r) then add_info_axiom r in
   let warn_log () = if not (constant_has_body cb) then add_log_axiom r
   in
@@ -1018,7 +1023,7 @@ let extract_constant env kn cb =
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = cb.const_type in
   match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
     | (Logic, Default) -> Sval (r, Tdummy Kother)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ba21c6cbf..133f4ada9 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -645,7 +645,7 @@ let implicits_of_global r =
  try Refmap'.find r !implicits_table with Not_found -> []
 
 let add_implicits r l =
-  let typ = Global.type_of_global r in
+  let typ = Global.type_of_global_unsafe r in
   let rels,_ =
     decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
   let names = List.rev_map fst rels in
@@ -816,7 +816,7 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ = Typeops.type_of_constant env kn in
+	let typ = (Environ.lookup_constant kn env).const_type in
 	let typ = Reduction.whd_betadeltaiota env typ in
 	if Reduction.is_arity env typ
 	  then begin
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 03a832e90..430b549d9 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -43,7 +43,7 @@ let rec nb_prod_after n c=
     | _ -> 0
 
 let construct_nhyps ind gls =
-  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+  let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in
   let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
   let hyp = nb_prod_after nparams in
     Array.map hyp constr_types
@@ -67,10 +67,10 @@ let special_whd gl=
 
 type kind_of_formula=
     Arrow of constr*constr
-  | False of inductive*constr list
-  | And of inductive*constr list*bool
-  | Or of inductive*constr list*bool
-  | Exists of inductive*constr list
+  | False of pinductive*constr list
+  | And of pinductive*constr list*bool
+  | Or of pinductive*constr list*bool
+  | Exists of pinductive*constr list
   | Forall of constr*constr
   | Atom of constr
 
@@ -85,11 +85,11 @@ let kind_of_formula gl term =
 	   |_->
 	      match match_with_nodep_ind cciterm with
 		  Some (i,l,n)->
-		    let ind=destInd i in
+		    let ind,u=destInd i in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
 		      if Int.equal nconstr 0 then
-			False(ind,l)
+			False((ind,u),l)
 		      else
 			let has_realargs=(n>0) in
 			let is_trivial=
@@ -102,9 +102,9 @@ let kind_of_formula gl term =
 			    Atom cciterm
 			  else
 			    if Int.equal nconstr 1 then
-			      And(ind,l,is_trivial)
+			      And((ind,u),l,is_trivial)
 			    else
-			      Or(ind,l,is_trivial)
+			      Or((ind,u),l,is_trivial)
 		| _ ->
 		    match match_with_sigma_type cciterm with
 			Some (i,l)-> Exists((destInd i),l)
@@ -186,19 +186,19 @@ type right_pattern =
 
 type left_arrow_pattern=
     LLatom
-  | LLfalse of inductive*constr list
-  | LLand of inductive*constr list
-  | LLor of inductive*constr list
+  | LLfalse of pinductive*constr list
+  | LLand of pinductive*constr list
+  | LLor of pinductive*constr list
   | LLforall of constr
-  | LLexists of inductive*constr list
+  | LLexists of pinductive*constr list
   | LLarrow of constr*constr*constr
 
 type left_pattern=
     Lfalse
-  | Land of inductive
-  | Lor of inductive
+  | Land of pinductive
+  | Lor of pinductive
   | Lforall of metavariable*constr*bool
-  | Lexists of inductive
+  | Lexists of pinductive
   | LA of constr*left_arrow_pattern
 
 type t={id:global_reference;
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 59b363393..d12b106cc 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -25,9 +25,9 @@ type ('a,'b) sum = Left of 'a | Right of 'b
 
 type counter = bool -> metavariable
 
-val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
+val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
 
-val ind_hyps : int -> inductive -> constr list ->
+val ind_hyps : int -> pinductive -> constr list ->
   Proof_type.goal Tacmach.sigma -> rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
@@ -49,19 +49,19 @@ type right_pattern =
 
 type left_arrow_pattern=
     LLatom
-  | LLfalse of inductive*constr list
-  | LLand of inductive*constr list
-  | LLor of inductive*constr list
+  | LLfalse of pinductive*constr list
+  | LLand of pinductive*constr list
+  | LLor of pinductive*constr list
   | LLforall of constr
-  | LLexists of inductive*constr list
+  | LLexists of pinductive*constr list
   | LLarrow of constr*constr*constr
 
 type left_pattern=
     Lfalse
-  | Land of inductive
-  | Lor of inductive
+  | Land of pinductive
+  | Lor of pinductive
   | Lforall of metavariable*constr*bool
-  | Lexists of inductive
+  | Lexists of pinductive
   | LA of constr*left_arrow_pattern
 
 type t={id: global_reference;
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 6c1709140..e0f4fa95f 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -18,7 +18,7 @@ let update_flags ()=
   let predref=ref Names.Cpred.empty in
   let f coe=
     try
-      let kn=destConst (Classops.get_coercion_value coe) in
+      let kn= fst (destConst (Classops.get_coercion_value coe)) in
 	predref:=Names.Cpred.add kn !predref
     with DestKO -> ()
   in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index fe22708a0..c6db6a49f 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -101,6 +101,8 @@ let dummy_constr=mkMeta (-1)
 
 let dummy_bvid=Id.of_string "x"
 
+let constr_of_global = Universes.constr_of_global
+
 let mk_open_instance id gl m t=
   let env=pf_env gl in
   let evmap=Refiner.project gl in
@@ -128,7 +130,7 @@ let mk_open_instance id gl m t=
 	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1)
 	| _-> anomaly (Pp.str "can't happen") in
   let ntt=try
-    Pretyping.understand evmap env (raux m rawt)
+    fst (Pretyping.understand evmap env (raux m rawt))(*FIXME*)
   with e when Errors.noncritical e ->
     error "Untypable instance, maybe higher-order non-prenex quantification" in
     decompose_lam_n_assum m ntt
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 6d9af2bbf..31a1e6cb0 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -53,7 +53,7 @@ let clear_global=function
     VarRef id->clear [id]
   | _->tclIDTAC
 
-
+let constr_of_global = Universes.constr_of_global
 (* connection rules *)
 
 let axiom_tac t seq=
@@ -117,14 +117,14 @@ let left_false_tac id=
 
 (* We use this function for false, and, or, exists *)
 
-let ll_ind_tac ind largs backtrack id continue seq gl=
-     let rcs=ind_hyps 0 ind largs gl in
+let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
+     let rcs=ind_hyps 0 indu largs gl in
      let vargs=Array.of_list largs in
 	     (* construire le terme  H->B, le generaliser etc *)
      let myterm i=
        let rc=rcs.(i) in
        let p=List.length rc in
-       let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
+       let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
        let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
@@ -204,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq=
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [AllOccurrences,EvalConstRef (destConst (constant "not"));
-   AllOccurrences,EvalConstRef (destConst (constant "iff"))]
+  [AllOccurrences,EvalConstRef (fst (destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))]
 
 let normalize_evaluables=
   onAllHypsAndConcl
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index bfebbaaf8..180f6f5da 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -33,19 +33,19 @@ val or_tac : seqtac with_backtracking
 
 val arrow_tac : seqtac with_backtracking
 
-val left_and_tac : inductive -> lseqtac with_backtracking
+val left_and_tac : pinductive -> lseqtac with_backtracking
 
-val left_or_tac : inductive -> lseqtac with_backtracking
+val left_or_tac : pinductive -> lseqtac with_backtracking
 
 val left_false_tac : global_reference -> tactic
 
-val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking
+val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking
 
 val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
 
 val forall_tac : seqtac with_backtracking
 
-val left_exists_tac : inductive -> lseqtac with_backtracking
+val left_exists_tac : pinductive -> lseqtac with_backtracking
 
 val ll_forall_tac : types -> lseqtac with_backtracking
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 72bde18f4..c0e5c7e58 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -199,7 +199,7 @@ let expand_constructor_hints =
 let extend_with_ref_list l seq gl=
   let l = expand_constructor_hints l in
   let f gr seq=
-    let c=constr_of_global gr in
+    let c=Universes.constr_of_global gr in
     let typ=(pf_type_of gl c) in
       add_formula Hyp gr typ seq gl in
     List.fold_right f l seq
@@ -210,10 +210,10 @@ let extend_with_auto_hints l seq gl=
   let seqref=ref seq in
   let f p_a_t =
     match p_a_t.code with
-	Res_pf (c,_) | Give_exact c
+	Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
 	  (try
-	     let gr=global_of_constr c in
+	     let gr = global_of_constr c in
 	     let typ=(pf_type_of gl c) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 2556460f5..f7ee9fdad 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -78,7 +78,7 @@ let unif t1 t2=
 		  for i=0 to l-1 do
 		    Queue.add (va.(i),vb.(i)) bige
 		  done
-	  | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
+	  | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2))
     done;
       assert false
 	(* this place is unreachable but needed for the sake of typing *)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index aeb07fc3a..d34d50364 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -87,7 +87,7 @@ let string_of_R_constant kn =
 let rec string_of_R_constr c =
  match kind_of_term c with
    Cast (c,_,_) -> string_of_R_constr c
-  |Const c -> string_of_R_constant c
+  |Const (c,_) -> string_of_R_constant c
   | _ -> "not_of_constant"
 
 exception NoRational
@@ -114,7 +114,7 @@ let rec rational_of_constr c =
 	     rminus (rational_of_constr args.(0))
                     (rational_of_constr args.(1))
 	 | _ -> raise NoRational)
-  | Const kn ->
+  | Const (kn,_) ->
       (match (string_of_R_constant kn) with
 	       "R1" -> r1
               |"R0" -> r0
@@ -160,7 +160,7 @@ let rec flin_of_constr c =
 	      with NoRational ->
                 flin_add (flin_zero()) args.(0) (rinv b))
          |_-> raise NoLinear)
-  | Const c ->
+  | Const (c,_) ->
         (match (string_of_R_constant c) with
 	       "R1" -> flin_one ()
               |"R0" -> flin_zero ()
@@ -194,7 +194,7 @@ let ineq1_of_constr (h,t) =
     match (kind_of_term t) with
       | App (f,args) ->
         (match kind_of_term f with
-          | Const c when Array.length args = 2 ->
+          | Const (c,_) when Array.length args = 2 ->
             let t1= args.(0) in
             let t2= args.(1) in
             (match (string_of_R_constant c) with
@@ -227,13 +227,13 @@ let ineq1_of_constr (h,t) =
                                              (flin_of_constr t1);
 			   hstrict=false}]
               |_-> raise NoIneq)
-          | Ind (kn,i) ->
+          | Ind ((kn,i),_) ->
             if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq;
             let t0= args.(0) in
             let t1= args.(1) in
             let t2= args.(2) in
 	    (match (kind_of_term t0) with
-              | Const c ->
+              | Const (c,_) ->
 		(match (string_of_R_constant c) with
 		  | "R"->
                          [{hname=h;
@@ -609,8 +609,9 @@ let rec fourier gl=
       			        [tclORELSE
                                    (* TODO : Ring.polynom []*) tclIDTAC
                                    tclIDTAC;
-					  (tclTHEN (apply (get coq_sym_eqT))
-						(apply (get coq_Rinv_1)))]
+				 pf_constr_of_global (get coq_sym_eqT) (fun symeq ->
+					  (tclTHEN (apply symeq)
+						(apply (get coq_Rinv_1))))]
 
 					 )
 				]));
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f06d8fa53..a3af23dcd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -124,11 +124,13 @@ let finish_proof dynamic_infos g =
 
 
 let refine c =
-  Tacmach.refine_no_check c
+  Tacmach.refine c
 
 let thin l =
   Tacmach.thin_no_check l
 
+let eq_constr u v = eq_constr_nounivs u v
+
 let is_trivial_eq t =
   let res =   try
     begin
@@ -205,7 +207,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
 
 
 let find_rectype env c =
-  let (t, l) = decompose_app (Reduction.whd_betaiotazeta c) in
+  let (t, l) = decompose_app (Reduction.whd_betaiotazeta env c) in
   match kind_of_term t with
   | Ind ind -> (t, l)
   | Construct _ -> (t,l)
@@ -233,7 +235,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       failwith "NoChange";
     end
   in
-  let eq_constr = Reductionops.is_conv env sigma in
+  let eq_constr = Evarconv.e_conv env (ref sigma) in
   if not (noccurn 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp t) then nochange "not an equality";
@@ -325,7 +327,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
 	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
-	   refine to_refine g
+	   let evm, _ = pf_apply Typing.e_type_of g to_refine in
+	     tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
 	)
     in
     let simpl_eq_tac =
@@ -633,8 +636,11 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
       ( (* we instanciate the hyp if possible  *)
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
+	  let c = mkApp(mkVar hid,args) in
+	  let evm, _ = pf_apply Typing.e_type_of g c in
 	  tclTHENLIST[
-	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args)));
+            Refiner.tclEVARS evm;
+	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
 	    thin [hid];
 	    rename_hyp [prov_hid,hid]
 	  ] g
@@ -757,6 +763,7 @@ let build_proof
 	      begin
 		match kind_of_term f with
 		  | App _ -> assert false (* we have collected all the app in decompose_app *)
+		  | Proj _ -> assert false (*FIXME*)
 		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
 		      let new_infos =
 			{ dyn_infos with
@@ -764,7 +771,7 @@ let build_proof
 			}
 		      in
 		      build_proof_args do_finalize new_infos  g
-		  | Const c when not (List.mem_f Constant.equal c fnames) ->
+		  | Const (c,_) when not (List.mem_f Constant.equal c fnames) ->
 		      let new_infos =
 			{ dyn_infos with
 			    info = (f,args)
@@ -809,6 +816,7 @@ let build_proof
 	  | Fix _ | CoFix _ ->
 	      error ( "Anonymous local (co)fixpoints are not handled yet")
 
+	  | Proj _ -> error "Prod"
 	  | Prod _ -> error "Prod"
 	  | LetIn _ ->
 	      let new_infos =
@@ -938,7 +946,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 (*   observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
 (*   observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
-  let f_def = Global.lookup_constant (destConst f) in
+  let f_def = Global.lookup_constant (fst (destConst f)) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body = Option.get (body_of_constant f_def)
   in
@@ -956,10 +964,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
 (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
-    (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
+    ((*FIXME*)f_def.const_type) in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
-  let f_id = Label.to_id (con_label (destConst f)) in
+  let f_id = Label.to_id (con_label (fst (destConst f))) in
   let prove_replacement =
     tclTHENSEQ
       [
@@ -978,8 +986,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
-    lemma_type
+    (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+    (lemma_type, (*FIXME*) Univ.ContextSet.empty)
     (fun _ _ -> ());
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_proof (Vernacexpr.Proved(false,None))
@@ -990,10 +998,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma =
     try
-      let finfos = find_Function_infos (destConst f) in
+      let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in
       mkConst (Option.get finfos.equation_lemma)
     with (Not_found | Option.IsNone as e) ->
-      let f_id = Label.to_id (con_label (destConst f)) in
+      let f_id = Label.to_id (con_label (fst (destConst f))) in
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
 	i*)
@@ -1002,7 +1010,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
       let _ =
 	match e with
 	  | Option.IsNone ->
-	      let finfos = find_Function_infos (destConst f) in
+	      let finfos = find_Function_infos (fst (destConst f)) in
 	      update_Function
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
@@ -1306,7 +1314,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 in
 		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
 		 tclTHENSEQ
-		   [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef fname)];
+		   [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))];
 		    let do_prove =
 		      build_proof
 			interactive_proof
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d6f21fb86..2adc82505 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -106,14 +106,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
     match kind_of_term c with
-      | Ind((u,_)) -> MutInd.equal u rel_as_kn
-      | Construct((u,_),_) -> MutInd.equal u rel_as_kn
+      | Ind((u,_),_) -> MutInd.equal u rel_as_kn
+      | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn
       | _ -> false
   in
   let get_fun_num c =
     match kind_of_term c with
-      | Ind(_,num) -> num
-      | Construct((_,num),_) -> num
+      | Ind((_,num),_) -> num
+      | Construct(((_,num),_),_) -> num
       | _ -> assert false
   in
   let dummy_var = mkVar (Id.of_string "________") in
@@ -251,8 +251,10 @@ let change_property_sort toSort princ princName =
   let princ_info = compute_elim_sig princ in
   let change_sort_in_predicate (x,v,t) =
     (x,None,
-     let args,_ = decompose_prod t in
-     compose_prod args (mkSort toSort)
+     let args,ty = decompose_prod t in
+     let s = destSort ty in
+       Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
+       compose_prod args (mkSort toSort)
     )
   in
   let princName_as_constr = Constrintern.global_reference princName in
@@ -292,8 +294,8 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   begin
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
-      new_principle_type
+      (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+      (new_principle_type, (*FIXME*) Univ.ContextSet.empty)
       hook
     ;
     (*       let _tim1 = System.get_time ()  in *)
@@ -315,7 +317,7 @@ let generate_functional_principle
   try
 
   let f = funs.(i) in
-  let type_sort = Termops.new_sort_in_family InType in
+  let type_sort = Universes.new_sort_in_family InType in
   let new_sorts =
     match sorts with
       | None -> Array.make (Array.length funs) (type_sort)
@@ -334,18 +336,23 @@ let generate_functional_principle
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
-	let s = Termops.new_sort_in_family fam_sort in
+	let s = Universes.new_sort_in_family fam_sort in
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = {
-          const_entry_body = Future.from_val (value,Declareops.no_seff);
-          const_entry_secctx = None;
-          const_entry_type = None;
-          const_entry_opaque = false;
-          const_entry_inline_code = false;
-          const_entry_feedback = None;
-	} in
+	let ce =
+          { const_entry_body =
+              Future.from_val (value,Declareops.no_seff);
+            const_entry_secctx = None;
+	    const_entry_type = None;	
+	    const_entry_polymorphic = false;
+	    const_entry_universes = Univ.UContext.empty (*FIXME*);
+	    const_entry_proj = None;
+	    const_entry_opaque = false;
+            const_entry_feedback = None;
+	    const_entry_inline_code = false
+	  }
+	in
 	ignore(
 	  Declare.declare_constant
 	    name
@@ -488,19 +495,20 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
     List.map
       (fun (idx) ->
 	 let ind = first_fun_kn,idx in
-	 ind,true,prop_sort
+	   (ind,Univ.Instance.empty)(*FIXME*),true,prop_sort
       )
       funs_indexes
   in
+  let sigma, schemes = 
+    Indrec.build_mutual_induction_scheme env sigma ind_list
+  in
   let l_schemes =
-    List.map
-      (Typing.type_of env sigma)
-      (Indrec.build_mutual_induction_scheme env sigma ind_list)
+    List.map (Typing.type_of env sigma) schemes
   in
   let i = ref (-1) in
   let sorts =
     List.rev_map (fun (_,x) ->
-		Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+		Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
 	     )
       fas
   in
@@ -649,10 +657,10 @@ let build_case_scheme fa =
 (*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
-		 try Globnames.constr_of_global (Nametab.global f)
+		 try Universes.constr_of_global (Nametab.global f)
 		 with Not_found ->
 		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
-  let first_fun = destConst  funs in
+  let first_fun,u = destConst  funs in
 
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
@@ -664,16 +672,18 @@ let build_case_scheme fa =
   let prop_sort = InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc_f Constant.equal (destConst funs) this_block_funs_indexes
+    List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
   in
   let ind_fun =
 	 let ind = first_fun_kn,funs_indexes in
-	 ind,prop_sort
+	   (ind,Univ.Instance.empty)(*FIXME*),prop_sort
   in
-  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun) in
+  let sigma, scheme = 
+    (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun in
+  let scheme_type =  (Typing.type_of env sigma ) scheme in
   let sorts =
     (fun (_,_,x) ->
-       Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
+       Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
     )
       fa
   in
@@ -690,6 +700,6 @@ let build_case_scheme fa =
       (Some princ_name)
       this_block_funs
       0
-      (prove_princ_for_struct false 0 [|destConst funs|])
+      (prove_princ_for_struct false 0 [|fst (destConst funs)|])
   in
   ()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2dd78d890..3802aa365 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -307,8 +307,11 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
     max_rel = max_rel; onlyvars = List.for_all isVar args }
     ::subres
 
+let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+
 let mkEq typ c1 c2 =
-  mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|])
+  mkApp (make_eq(),[| typ; c1; c2|])
 
 
 let poseq_unsafe idunsafe cstr gl =
@@ -463,10 +466,10 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
   [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
       "with" "(" ident(id2) ne_ident_list(cl2)  ")" "using" ident(id) ] ->
      [
-       let f1 = Constrintern.interp_constr Evd.empty (Global.env())
-	 (CRef (Libnames.Ident (Loc.ghost,id1))) in
-       let f2 = Constrintern.interp_constr Evd.empty (Global.env())
-	 (CRef (Libnames.Ident (Loc.ghost,id2))) in
+       let f1,ctx = Constrintern.interp_constr Evd.empty (Global.env())
+	 (CRef (Libnames.Ident (Loc.ghost,id1),None)) in
+       let f2,ctx' = Constrintern.interp_constr Evd.empty (Global.env())
+	 (CRef (Libnames.Ident (Loc.ghost,id2),None)) in
        let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
        let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
        let ar1 = List.length (fst (decompose_prod f1type)) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index dd02dfe8d..4544f736c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -333,8 +333,8 @@ let raw_push_named (na,raw_value,raw_typ) env =
   match na with
     | Anonymous -> env
     | Name id ->
-	let value = Option.map (Pretyping.understand Evd.empty env) raw_value in
-	let typ = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
+	let value = Option.map (fun x-> fst (Pretyping.understand Evd.empty env x)) raw_value in
+	let typ,ctx = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in
 	Environ.push_named (id,value,typ) env
 
 
@@ -350,7 +350,7 @@ let add_pat_variables pat typ env : Environ.env =
 	    with Not_found -> assert false
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
-	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c cs.Inductiveops.cs_cstr) (Array.to_list constructors) in
+	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
 	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
 	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
@@ -397,7 +397,7 @@ let rec pattern_to_term_and_type env typ  = function
 	with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
-      let constructor  = List.find (fun cs -> eq_constructor cs.Inductiveops.cs_cstr constr) (Array.to_list constructors) in
+      let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
       let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
       let _,cstl = Inductiveops.dest_ind_family indf in
       let csta = Array.of_list cstl in
@@ -486,7 +486,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		   a pseudo value "v1 ... vn".
 		   The "value" of this branch is then simply [res]
 		*)
-		let rt_as_constr = Pretyping.understand Evd.empty env rt in
+		let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in
 		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
 		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
@@ -559,6 +559,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		build_entry_lc env funnames avoid (mkGApp(b,args))
 	    | GRec _ -> error "Not handled GRec"
+            | GProj _ -> error "Not handled GProj"
 	    | GProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *)
 
@@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	   and combine the two result
 	*)
 	let v_res = build_entry_lc env funnames avoid v in
-	let v_as_constr = Pretyping.understand Evd.empty env v in
+	let v_as_constr,ctx = Pretyping.understand Evd.empty env v in
 	let v_type = Typing.type_of env Evd.empty v_as_constr in
 	let new_env =
 	  match n with
@@ -610,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let make_discr = make_discr_match brl in
 	build_entry_lc_from_case env funnames make_discr el brl avoid
     | GIf(_,b,(na,e_option),lhs,rhs) ->
-	let b_as_constr = Pretyping.understand Evd.empty env b in
+	let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
 	let b_typ = Typing.type_of env Evd.empty b_as_constr in
 	let (ind,_) =
 	  try Inductiveops.find_inductive env Evd.empty b_typ
@@ -619,7 +620,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			       Printer.pr_glob_constr b ++ str " in " ++
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
-	let case_pats = build_constructors_of_type ind [] in
+	let case_pats = build_constructors_of_type (fst ind) [] in
 	assert (Int.equal (Array.length case_pats) 2);
 	let brl =
 	  List.map_i
@@ -642,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	      )
 	      nal
 	  in
-	  let b_as_constr = Pretyping.understand Evd.empty env b in
+	  let b_as_constr,ctx = Pretyping.understand Evd.empty env b in
 	  let b_typ = Typing.type_of env Evd.empty b_as_constr in
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env Evd.empty b_typ
@@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 				 Printer.pr_glob_constr b ++ str " in " ++
 				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	  in
-	  let case_pats = build_constructors_of_type ind nal_as_glob_constr in
+	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
 	  assert (Int.equal (Array.length case_pats) 1);
 	  let br =
 	    (Loc.ghost,[],[case_pats.(0)],e)
@@ -661,6 +662,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 
 	end
     | GRec _ -> error "Not handled GRec"
+    | GProj _ -> error "Not handled GProj"
     | GCast(_,b,_) ->
 	build_entry_lc env funnames  avoid b
 and build_entry_lc_from_case env funname make_discr
@@ -689,7 +691,7 @@ and build_entry_lc_from_case env funname make_discr
 	in
 	let types =
 	  List.map (fun (case_arg,_) ->
-		      let case_arg_as_constr = Pretyping.understand Evd.empty env case_arg in
+		      let case_arg_as_constr,ctx = Pretyping.understand Evd.empty env case_arg in
 		      Typing.type_of env Evd.empty case_arg_as_constr
 		   ) el
 	in
@@ -844,7 +846,7 @@ let is_res id =
 
 let same_raw_term rt1 rt2 = 
   match rt1,rt2 with 
-    | GRef(_,r1), GRef (_,r2) -> Globnames.eq_gr r1 r2
+    | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
 let decompose_raw_eq lhs rhs = 
@@ -894,7 +896,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			let new_t =
 			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
 			in
-			let t' = Pretyping.understand Evd.empty env new_t in
+			let t',ctx = Pretyping.understand Evd.empty env new_t in
 			let new_env = Environ.push_rel (n,None,t') env in
 			let new_b,id_to_exclude =
 			  rebuild_cons new_env
@@ -907,14 +909,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
-	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt])
+	    | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt])
 		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
 		  ->
 		begin
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
-		      try Pretyping.understand Evd.empty env t
+		      try fst (Pretyping.understand Evd.empty env t)(*FIXME*)
                       with e when Errors.noncritical e -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
@@ -936,17 +938,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
-		    let jmeq = Globnames.IndRef (destInd (jmeq ())) in
-		    let ty' = Pretyping.understand Evd.empty env ty in
+		    let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
+		    let ty',ctx = Pretyping.understand Evd.empty env ty in
 		    let ind,args' = Inductive.find_inductive env ty' in
-		    let mib,_ = Global.lookup_inductive ind in
+		    let mib,_ = Global.lookup_inductive (fst ind) in
 		    let nparam = mib.Declarations.mind_nparams in
 		    let params,arg' =
 		      ((Util.List.chop nparam args'))
 		    in
 		    let rt_typ =
 		       GApp(Loc.ghost,
-			    GRef (Loc.ghost,Globnames.IndRef ind),
+			    GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 (Termops.names_of_rel_context env)
@@ -956,10 +958,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 					 (mkGHole ()))))
 		    in
 		    let eq' =
-		      GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt])
+		      GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
-		    let eq'_as_constr = Pretyping.understand Evd.empty env eq' in
+		    let eq'_as_constr,ctx = Pretyping.understand Evd.empty env eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
 		      match kind_of_term eq'_as_constr with
@@ -1007,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     if is_in_b then b else  replace_var_by_term id rt b
 		    in
 		    let new_env =
-		      let t' = Pretyping.understand Evd.empty env eq' in
+		      let t',ctx = Pretyping.understand Evd.empty env eq' in
 		      Environ.push_rel (n,None,t') env
 		    in
 		    let new_b,id_to_exclude =
@@ -1024,7 +1026,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     mkGProd(n,t,new_b),id_to_exclude
 		     else new_b, Id.Set.add id id_to_exclude
 		  *)
-	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
+	    | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2])
 		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
 		  ->
 	      begin
@@ -1045,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  else raise Continue
 	      with Continue -> 
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t' = Pretyping.understand Evd.empty env t in
+		let t',ctx = Pretyping.understand Evd.empty env t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1061,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
-		let t' = Pretyping.understand Evd.empty env t in
+		let t',ctx = Pretyping.understand Evd.empty env t in
 		let new_env = Environ.push_rel (n,None,t') env in
 		let new_b,id_to_exclude =
 		  rebuild_cons new_env
@@ -1080,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
 	  observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
-	  let t' = Pretyping.understand Evd.empty env t in
+	  let t',ctx = Pretyping.understand Evd.empty env t in
 	  match n with
 	    | Name id ->
 		let new_env = Environ.push_rel (n,None,t') env in
@@ -1102,7 +1104,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | GLetIn(_,n,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
-	  let t' = Pretyping.understand Evd.empty env t in
+	  let t',ctx = Pretyping.understand Evd.empty env t in
 	  let type_t' = Typing.type_of env Evd.empty t' in
 	  let new_env = Environ.push_rel (n,Some t',type_t') env in
 	  let new_b,id_to_exclude =
@@ -1127,7 +1129,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (crossed_types)
 	      depth t
 	  in
-	  let t' = Pretyping.understand Evd.empty env new_t in
+	  let t',ctx = Pretyping.understand Evd.empty env new_t in
 	  let new_env = Environ.push_rel (na,None,t') env in
 	  let new_b,id_to_exclude =
 	    rebuild_cons new_env
@@ -1179,7 +1181,7 @@ let rec compute_cst_params relnames params = function
 		 discriminitation ones *)
   | GSort _ -> params
   | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ ->
+  | GIf _ | GRec _ | GCast _ | GProj _->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
@@ -1267,12 +1269,12 @@ let do_build_inductive
 	(fun (n,t,is_defined) acc ->
 	   if is_defined
 	   then
-	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
 			      acc)
 	   else
 	     Constrexpr.CProdN
 	       (Loc.ghost,
-		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 		acc
 	       )
 	)
@@ -1285,7 +1287,8 @@ let do_build_inductive
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
     Util.Array.fold_left2 (fun env rel_name rel_ar ->
-			     Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
+			     Environ.push_named (rel_name,None, 
+						 fst (with_full_print (Constrintern.interp_constr Evd.empty env) rel_ar)) env) env relnames rel_arities
   in
   (* and of the real constructors*)
   let constr i res =
@@ -1333,12 +1336,12 @@ let do_build_inductive
       (fun (n,t,is_defined) acc ->
 	 if is_defined
 	 then
-	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
+	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
 			    acc)
 	 else
 	   Constrexpr.CProdN
 	   (Loc.ghost,
-	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
+	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 	    acc
 	   )
       )
@@ -1366,8 +1369,7 @@ let do_build_inductive
     Array.map (List.map
       (fun (id,t) ->
 	 false,((Loc.ghost,id),
-		Flags.with_option
-		  Flags.raw_print
+		with_full_print
 		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t)
 	       )
       ))
@@ -1403,7 +1405,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 6a7f326e6..5efaf7954 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -10,7 +10,7 @@ open Misctypes
    Some basic functions to rebuild glob_constr
    In each of them the location is Loc.ghost
 *)
-let mkGRef ref = GRef(Loc.ghost,ref)
+let mkGRef ref = GRef(Loc.ghost,ref,None)
 let mkGVar id = GVar(Loc.ghost,id)
 let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl)
 let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b)
@@ -180,6 +180,7 @@ let change_vars =
       | GRec _ -> error "Local (co)fixes are not supported"
       | GSort _ -> rt
       | GHole _ -> rt
+      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GCast(loc,b,c) ->
 	  GCast(loc,change_vars mapping b,
 		Miscops.map_cast_type (change_vars mapping) c)
@@ -357,6 +358,7 @@ let rec alpha_rt excluded rt =
 	    alpha_rt excluded rhs
 	   )
     | GRec _ -> error "Not handled GRec"
+    | GProj _ -> error "Native projections are not supported" (** FIXME *)
     | GSort _ -> rt
     | GHole _ -> rt
     | GCast (loc,b,c) ->
@@ -407,6 +409,7 @@ let is_free_in id =
     | GIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
     | GRec _ -> raise (UserError("",str "Not handled GRec"))
+    | GProj _ -> error "Native projections are not supported" (** FIXME *)
     | GSort _ -> false
     | GHole _ -> false
     | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -503,6 +506,7 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern rhs
 	     )
       | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
@@ -598,6 +602,7 @@ let ids_of_glob_constr c =
       | GCases (loc,sty,rtntypopt,tml,brchl) ->
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
       | GRec _ -> failwith "Fix inside a constructor branch"
+      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
   in
   (* build the set *)
@@ -656,6 +661,7 @@ let zeta_normalize =
 	      zeta_normalize_term rhs
 	     )
       | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
@@ -698,6 +704,7 @@ let expand_as =
 	  GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | GRec _ ->  error "Not handled GRec"
+      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GCast(loc,b,c) ->
 	  GCast(loc,expand_as map b,
 		Miscops.map_cast_type (expand_as map) c)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 661e5e486..d98f824e8 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -38,7 +38,7 @@ let functional_induction with_clean c princl pat =
 	| None -> (* No principle is given let's find the good one *)
 	    begin
 	      match kind_of_term f with
-		| Const c' ->
+		| Const (c',u) ->
 		    let princ_option =
 		      let finfo = (* we first try to find out a graph on f *)
 			try find_Function_infos c'
@@ -148,7 +148,7 @@ let build_newrecursive
     List.fold_left
       (fun (env,impls) ((_,recname),bl,arityc,_) ->
         let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
-        let arity = Constrintern.interp_type sigma env0 arityc in
+        let arity,ctx = Constrintern.interp_type sigma env0 arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
         (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
@@ -182,6 +182,7 @@ let is_rec names =
     | GVar(_,id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
     | GCast(_,b,_) -> lookup names b
+    | GProj _ -> error "GProj not handled"
     | GRec _ -> error "GRec not handled"
     | GIf(_,b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
@@ -222,7 +223,7 @@ let derive_inversion fix_names =
   try
     (* we first transform the fix_names identifier into their corresponding constant *)
     let fix_names_as_constant =
-      List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names
+      List.map (fun id -> fst (destConst (Constrintern.global_reference id))) fix_names
     in
     (*
        Then we check that the graphs have been defined
@@ -239,7 +240,7 @@ let derive_inversion fix_names =
 	  Ensures by : register_built
 	  i*)
 	(List.map
-	   (fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
+	   (fun id -> fst (destInd (Constrintern.global_reference (mk_rel_id id))))
 	   fix_names
 	)
     with e when Errors.noncritical e ->
@@ -326,9 +327,8 @@ let generate_principle  on_error
 	let _ =
 	  List.map_i
 	    (fun i x ->
-	       let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
-	       let princ_type = Typeops.type_of_constant (Global.env()) princ
-	       in
+	       let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
+	       let princ_type = Global.type_of_global_unsafe princ in
 	       Functional_principles_types.generate_functional_principle
 		 interactive_proof
 		 princ_type
@@ -351,10 +351,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
-	Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
+	Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
 	  bl None body (Some ret_type) (fun _ _ -> ())
     | _ ->
-	Command.do_fixpoint Global fixpoint_exprl
+	Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -385,7 +385,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     let f_app_args =
       Constrexpr.CAppExpl
 	(Loc.ghost,
-	 (None,(Ident (Loc.ghost,fname))) ,
+	 (None,(Ident (Loc.ghost,fname)),None) ,
 	 (List.map
 	    (function
 	       | _,Anonymous -> assert false
@@ -399,7 +399,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
-  let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
+  let hook (f_ref,_) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
       nb_args relation =
     try
       pre_hook
@@ -536,7 +536,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
 
 let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = 
   let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
-  let ((_,_,typel),_) = Command.interp_fixpoint fixl ntns in
+  let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in
   let constr_expr_typel = 
     with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in 
   let fixpoint_exprl_with_new_bl = 
@@ -631,10 +631,10 @@ let do_generate_principle on_error register_built interactive_proof
 
 let rec add_args id new_args b =
   match b with
-  | CRef r ->
+  | CRef (r,_) ->
       begin      match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
-	    CAppExpl(Loc.ghost,(None,r),new_args)
+	    CAppExpl(Loc.ghost,(None,r,None),new_args)
 	| _ -> b
       end
   | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
@@ -648,12 +648,12 @@ let rec add_args id new_args b =
 	       add_args id new_args  b1)
   | CLetIn(loc,na,b1,b2) ->
       CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
-  | CAppExpl(loc,(pf,r),exprl) ->
+  | CAppExpl(loc,(pf,r,us),exprl) ->
       begin
 	match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
-	    CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
-	| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
+	    CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl))
+	| _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl)
       end
   | CApp(loc,(pf,b),bl) ->
       CApp(loc,(pf,add_args id new_args b),
@@ -767,11 +767,10 @@ let make_graph (f_ref:global_reference) =
      | Some body ->
 	 let env = Global.env () in
 	 let extern_body,extern_type =
-	   with_full_print
-	     (fun () ->
+	   with_full_print (fun () ->
 		(Constrextern.extern_constr false env body,
 		 Constrextern.extern_type false env
-                   (Typeops.type_of_constant_type env c_body.const_type)
+                   ((*FIXNE*) c_body.const_type)
 		)
 	     )
 	     ()
@@ -792,7 +791,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.LocalRawAssum (nal,_,_) ->
 				      List.map
 					(fun (loc,n) ->
-					   CRef(Libnames.Ident(loc, Nameops.out_name n)))
+					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
 			       )
 			       nal_tas
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5c37dcec3..8cccb0bed 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -114,7 +114,7 @@ let const_of_id id =
 let def_of_const t =
    match (Term.kind_of_term t) with
     Term.Const sp ->
-      (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
+      (try (match Environ.constant_opt_value_in (Global.env()) sp with
              | Some c -> c
 	     | _ -> assert false)
        with Not_found -> assert false)
@@ -146,7 +146,7 @@ let get_locality = function
 | Local -> true
 | Global -> false
 
-let save with_clean id const (locality,kind) hook =
+let save with_clean id const (locality,_,kind) hook =
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
         let k = Kindops.logical_kind_of_goal_kind kind in
@@ -177,7 +177,8 @@ let get_proof_clean do_reduce =
 let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
-  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () 
+  in
   let old_rawprint = !Flags.raw_print in
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
@@ -259,8 +260,8 @@ let cache_Function (_,finfos) =
 
 let load_Function _  = cache_Function
 let subst_Function (subst,finfos) =
-  let do_subst_con c = fst (Mod_subst.subst_con subst c)
-  and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
+  let do_subst_con c = Mod_subst.subst_constant subst c
+  and do_subst_ind i = Mod_subst.subst_ind subst i
   in
   let function_constant' = do_subst_con finfos.function_constant in
   let graph_ind' = do_subst_ind finfos.graph_ind in
@@ -336,7 +337,7 @@ let pr_info f_info =
   str "function_constant_type := " ++
   (try
      Printer.pr_lconstr
-       (Global.type_of_global (ConstRef f_info.function_constant))
+       (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
    with e when Errors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0e8b22deb..6e8b79a6b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -58,7 +58,7 @@ val get_proof_clean : bool ->
 
 
 
-(* [with_full_print f a] applies [f] to [a] in full printing environment
+(* [with_full_print f a] applies [f] to [a] in full printing environment.
 
    This function preserves the print settings
 *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 7c8f5714e..897c8765b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -112,7 +112,9 @@ let id_to_constr id =
 
 let generate_type g_to_f f graph i =
   (*i we deduce the number of arguments of the function and its returned type from the graph i*)
-  let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph))  in
+  let gr,u = destInd graph in
+  let graph_arity = Inductive.type_of_inductive (Global.env()) 
+    (Global.lookup_inductive gr, u) in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -138,8 +140,11 @@ let generate_type g_to_f f graph i =
     the hypothesis [res = fv] can then be computed
     We will need to lift it by one in order to use it as a conclusion
     i*)
+  let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+  in
   let res_eq_f_of_args =
-    mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
+    mkApp(make_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|])
   in
   (*i
     The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed
@@ -166,7 +171,7 @@ let generate_type g_to_f f graph i =
    WARNING: while convertible, [type_of body] and [type] can be non equal
 *)
 let find_induction_principle f =
-  let f_as_constant =  match kind_of_term f with
+  let f_as_constant,u =  match kind_of_term f with
     | Const c' -> c'
     | _ -> error "Must be used with a function"
   in
@@ -205,6 +210,11 @@ let rec generate_fresh_id x avoid i =
     let id = Namegen.next_ident_away_in_goal x avoid in
     id::(generate_fresh_id x (id::avoid) (pred i))
 
+let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+let make_eq_refl () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+
 
 (* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ]
    is the tactic used to prove correctness lemma.
@@ -237,7 +247,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
        \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun  fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
     *)
     (* we the get the definition of the graphs block *)
-    let graph_ind = destInd graphs_constr.(i) in
+    let graph_ind,u = destInd graphs_constr.(i) in
     let kn = fst graph_ind in
     let mib,_ = Global.lookup_inductive graph_ind in
     (* and the principle to use in this lemma in $\zeta$ normal form *)
@@ -267,8 +277,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	branches
     in
     (* before building the full intro pattern for the principle *)
-    let eq_ind = Coqlib.build_coq_eq () in
-    let eq_construct = mkConstruct((destInd eq_ind),1) in
+    let eq_ind = make_eq () in
+    let eq_construct = mkConstructUi (destInd eq_ind, 1) in
     (* The next to referencies will be used to find out which constructor to apply in each branch *)
     let ind_number = ref 0
     and min_constr_number = ref 0 in
@@ -731,7 +741,7 @@ let  rec intros_with_rewrite g =
   observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
 and intros_with_rewrite_aux : tactic =
   fun g ->
-    let eq_ind = Coqlib.build_coq_eq () in
+    let eq_ind = make_eq () in
     match kind_of_term (pf_concl g) with
 	  | Prod(_,t,t') ->
 	      begin
@@ -830,7 +840,7 @@ let rec reflexivity_with_destruct_cases g =
         | _ -> Proofview.V82.of_tactic reflexivity
     with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
   in
-  let eq_ind =     Coqlib.build_coq_eq () in
+  let eq_ind = make_eq () in
   let discr_inject =
     Tacticals.onAllHypsAndConcl (
        fun sc g ->
@@ -936,7 +946,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let rewrite_tac j ids : tactic =
       let graph_def = graphs.(j) in
       let infos =
-        try find_Function_infos (destConst funcs.(j))
+        try find_Function_infos (fst (destConst funcs.(j)))
         with Not_found ->  error "No graph found"
       in
       if infos.is_general
@@ -962,7 +972,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  thin ids
 	]
       else
-        unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))]
+        unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in
@@ -1026,7 +1036,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     let lemmas_types_infos =
       Util.Array.map2_i
 	(fun i f_constr graph ->
-	   let const_of_f = destConst f_constr in
+	   let const_of_f,u = destConst f_constr in
 	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
 	     generate_type false const_of_f graph i
 	   in
@@ -1065,22 +1075,22 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 i*)
 	 let lem_id = mk_correct_id f_id in
 	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
-	   (fst lemmas_types_infos.(i))
+	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
+           (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
            (fun _ _ -> ());
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
 	      (proving_tac i))));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
-	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
+	 let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in
 	 update_Function {finfo with correctness_lemma = Some lem_cst}
       )
       funs;
     let lemmas_types_infos =
       Util.Array.map2_i
 	(fun i f_constr graph ->
-	   let const_of_f = destConst f_constr in
+	   let const_of_f = fst (destConst f_constr) in
 	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
 	     generate_type true  const_of_f graph i
 	   in
@@ -1092,19 +1102,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	funs_constr
 	graphs_constr
     in
-    let kn,_ as graph_ind  = destInd graphs_constr.(0) in
+    let kn,_ as graph_ind  = fst (destInd graphs_constr.(0)) in
     let  mib,mip = Global.lookup_inductive graph_ind in
-    let schemes =
-      Array.of_list
+    let sigma, scheme = 
 	(Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i _ -> (kn,i),true,InType)
+		 (fun i _ -> ((kn,i),Univ.Instance.empty)(*FIXME*),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
 	)
     in
+    let schemes =
+      Array.of_list scheme
+    in
     let proving_tac =
       prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos
     in
@@ -1116,15 +1128,12 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   i*)
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
-	   (fst lemmas_types_infos.(i))
+	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
+           (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
            (fun _ _ -> ());
-	 ignore (Pfedit.by
-	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-	      (proving_tac i))));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
-	 let lem_cst = destConst (Constrintern.global_reference lem_id) in
+	 let lem_cst,u = destConst (Constrintern.global_reference lem_id) in
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs)
@@ -1142,7 +1151,7 @@ let revert_graph kn post_tac hid g =
     let typ = pf_type_of g (mkVar hid) in
     match kind_of_term typ with
       | App(i,args) when isInd i ->
-	  let ((kn',num) as ind') = destInd i in
+	  let ((kn',num) as ind'),u = destInd i in
 	  if MutInd.equal kn kn'
 	  then (* We have generated a graph hypothesis so that we must change it if we can *)
 	    let info =
@@ -1192,7 +1201,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let type_of_h = pf_type_of g (mkVar hid) in
     match kind_of_term type_of_h with
-      | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ())  ->
+      | App(eq,args) when eq_constr eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
 	    match kind_of_term args.(1),kind_of_term args.(2) with
 	      | App(f,f_args),_ when eq_constr f fconst ->
@@ -1244,12 +1253,12 @@ let invfun qhyp f g =
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
 	     let hyp_typ = pf_type_of g (mkVar hid)  in
 	     match kind_of_term hyp_typ with
-	       | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) ->
+	       | App(eq,args) when eq_constr eq (make_eq ()) ->
 		   begin
 		     let f1,_ = decompose_app args.(1) in
 		     try
 		       if not (isConst f1) then failwith "";
-		       let finfos = find_Function_infos (destConst f1) in
+		       let finfos = find_Function_infos (fst (destConst f1)) in
 		       let f_correct = mkConst(Option.get finfos.correctness_lemma)
 		       and kn = fst finfos.graph_ind
 		       in
@@ -1258,7 +1267,7 @@ let invfun qhyp f g =
 		       try
 			 let f2,_ = decompose_app args.(2) in
 			 if not (isConst f2) then failwith "";
-			 let finfos = find_Function_infos (destConst f2) in
+			 let finfos = find_Function_infos (fst (destConst f2)) in
 			 let f_correct = mkConst(Option.get finfos.correctness_lemma)
 			 and kn = fst finfos.graph_ind
 			 in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ac54e44cc..d0497f6f6 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -70,7 +70,7 @@ let isVarf f x =
     in global environment. *)
 let ident_global_exist id =
   try
-    let ans = CRef (Libnames.Ident (Loc.ghost,id)) in
+    let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
     let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
   with e when Errors.noncritical e -> false
@@ -134,16 +134,12 @@ let prNamedRLDecl s lc =
 let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
   let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
-  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
+  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
   List.iter (fun (nm, optcstr, tp) ->
     print_string (string_of_name nm^":");
     prconstr tp; print_string "\n")
     ib1.mind_arity_ctxt;
-  (match ib1.mind_arity with
-    | Monomorphic x ->
-        Printf.printf "arity :"; prconstr x.mind_user_arity
-    | Polymorphic x ->
-        Printf.printf "arity : universe?");
+    Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity;
   Array.iteri
     (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
     ib1.mind_user_lc
@@ -888,7 +884,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
+  let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
 
@@ -961,7 +957,7 @@ let funify_branches relinfo nfuns branch =
       | _ -> assert false in
   let is_dom c =
     match kind_of_term c with
-      | Ind((u,_)) | Construct((u,_),_) -> MutInd.equal u mut_induct
+      | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
       | _ -> false in
   let _dom_i c =
     assert (is_dom c);
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 614886073..96bf4c921 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -52,29 +52,21 @@ let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
   locate (make_qualid dp (Id.of_string s))
 
-let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
-  fun f_id kind value ->
-    let ce = {const_entry_body = Future.from_val
-                (value, Declareops.no_seff);
-              const_entry_secctx = None;
-	      const_entry_type = None;
-          const_entry_opaque = false;
-          const_entry_inline_code = false;
-          const_entry_feedback = None;
-    } in
-      ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
+  let ce = definition_entry ~univs:ctx value (*FIXME *) in
+    ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
 let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
 
 let def_of_const t =
    match (kind_of_term t) with
     Const sp ->
-      (try (match body_of_constant (Global.lookup_constant sp) with
+      (try (match constant_opt_value_in (Global.env ()) sp with
              | Some c -> c
 	     | _ -> raise Not_found)
        with Not_found ->
 	 anomaly (str "Cannot find definition of constant " ++
-		    (Id.print (Label.to_id (con_label sp))))
+		    (Id.print (Label.to_id (con_label (fst sp)))))
       )
      |_ -> assert false
 
@@ -83,6 +75,7 @@ let type_of_const t =
     Const sp -> Typeops.type_of_constant (Global.env()) sp
     |_ -> assert false
 
+let constr_of_global = Universes.constr_of_global
 
 let constant sl s = constr_of_global (find_reference sl s)
 
@@ -188,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) =
     let glob_body =
       GCases
 	(d0,RegularStyle,None,
-	 [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
+	 [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
 	  (Anonymous,None)],
 	 [d0, [v_id], [PatCstr(d0,(destIndRef
 				     (delayed_force coq_sig_ref),1),
@@ -197,7 +190,7 @@ let (value_f:constr list -> global_reference -> constr) =
 			       Anonymous)],
 	  GVar(d0,v_id)])
     in
-    let body = understand Evd.empty env glob_body in
+    let body = fst (understand Evd.empty env glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
 
 let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
@@ -302,6 +295,7 @@ let check_not_nested forbidden e =
       | Lambda(_,t,b) -> check_not_nested t;check_not_nested b
       | LetIn(_,v,t,b) -> check_not_nested t;check_not_nested b;check_not_nested v
       | App(f,l) -> check_not_nested f;Array.iter check_not_nested l
+      | Proj (p,c) -> check_not_nested c
       | Const _ -> ()
       | Ind _ -> ()
       | Construct _ -> ()
@@ -412,6 +406,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
   match kind_of_term expr_info.info with 
     | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint"
+    | Proj _ -> error "Function cannot treat projections"
     | LetIn(na,b,t,e) -> 
       begin
 	let new_continuation_tac = 
@@ -640,7 +635,16 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   in
   continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} 
 
+let pf_type c tac gl = 
+  let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in
+    tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
 
+let pf_typel l tac =
+  let rec aux tys l =
+    match l with
+    | [] -> tac (List.rev tys)
+    | hd :: tl -> pf_type hd (fun ty -> aux (ty::tys) tl)
+  in aux [] l
 
 (* This is like the previous one except that it also rewrite on all
   hypotheses except the ones given in the first argument.  All the
@@ -660,12 +664,13 @@ let mkDestructEq :
   let type_of_expr = pf_type_of g expr in
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
+    pf_typel new_hyps (fun _ ->
     tclTHENLIST
      [Simple.generalize new_hyps;
       (fun g2 ->
 	change_in_concl None
 	  (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
-      Proofview.V82.of_tactic (simplest_case expr)], to_revert
+      Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
@@ -1167,7 +1172,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 let get_current_subgoals_types () =
   let p = Proof_global.give_me_the_proof () in
   let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
-  List.map (Goal.V82.abstract_type sigma) sgs
+    sigma, List.map (Goal.V82.abstract_type sigma) sgs
 
 let build_and_l l =
   let and_constr =  Coqlib.build_coq_and () in
@@ -1225,12 +1230,12 @@ let clear_goals =
 
 
 let build_new_goal_type () =
-  let sub_gls_types = get_current_subgoals_types () in
-  (* Pp.msgnl (str "sub_gls_types1 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
+  let sigma, sub_gls_types = get_current_subgoals_types () in
+  (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
   let sub_gls_types = clear_goals sub_gls_types in
   (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
   let res = build_and_l sub_gls_types in
-  res
+    sigma, res
 
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
@@ -1239,7 +1244,7 @@ let is_opaque_constant c =
     | Declarations.Undef _ -> true
     | Declarations.Def _ -> false
 
-let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
+let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
   let current_proof_name = get_current_proof_name () in
   let name = match goal_name with
@@ -1265,7 +1270,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     let lid = ref [] in
     let h_num = ref (-1) in
     Proof_global.discard_all ();
-    build_proof
+    build_proof (Univ.ContextSet.empty)
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   tclTHENSEQ
@@ -1312,8 +1317,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
   in
   Lemmas.start_proof
     na
-    (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
-    gls_type
+    (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
+    (gls_type, ctx)
     hook;
   if Indfun_common.is_strict_tcc  ()
   then
@@ -1330,7 +1335,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	 	     (fun c ->
 	 		tclTHENSEQ
 	 		  [Proofview.V82.of_tactic intros;
-	 		   Simple.apply (interp_constr Evd.empty (Global.env()) c);
+	 		   Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*);
 	 		   tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto)
 	 		  ]
 	 	     )
@@ -1354,22 +1359,24 @@ let com_terminate
     relation
     rec_arg_num
     thm_name using_lemmas
-    nb_args
+    nb_args ctx
     hook =
-  let start_proof (tac_start:tactic) (tac_end:tactic) =
+  let ctx = Univ.ContextSet.of_context ctx in
+  let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
     let (evmap, env) = Lemmas.get_current_context() in
     Lemmas.start_proof thm_name
-      (Global, Proof Lemma) ~sign:(Environ.named_context_val env)
-      (compute_terminate_type nb_args fonctional_ref) hook;
+      (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
+      (compute_terminate_type nb_args fonctional_ref, ctx) hook;
 
     ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
     ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
     				   input_type relation rec_arg_num ))))
   in
-  start_proof tclIDTAC tclIDTAC;
+  start_proof ctx tclIDTAC tclIDTAC;
   try
-    let new_goal_type = build_new_goal_type () in
-    open_new_goal start_proof using_lemmas tcc_lemma_ref
+    let sigma, new_goal_type = build_new_goal_type () in
+    open_new_goal start_proof (Evd.get_universe_context_set sigma)
+      using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type);
   with Failure "empty list of subgoals!" ->
@@ -1384,7 +1391,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
   (cont_tactic:Id.t list -> tactic) g =
   let ids = pf_ids_of_hyps g in
   let terminate_constr = constr_of_global term_f in
-  let nargs = nb_prod (type_of_const terminate_constr) in
+  let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in
   let x = n_x_id ids nargs in
   tclTHENLIST [
     h_intros x;
@@ -1406,8 +1413,8 @@ let (com_eqn : int -> Id.t ->
     let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    (Lemmas.start_proof eq_name (Global, Proof Lemma)
-       ~sign:(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+    (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
+       ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ());
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
@@ -1445,13 +1452,15 @@ let (com_eqn : int -> Id.t ->
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
-  let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
-  let env = push_named (function_name,None,function_type) (Global.env()) in
+  let env = Global.env() in
+  let evd = ref (Evd.from_env env) in
+  let function_type = interp_type_evars evd env type_of_f in
+  let env = push_named (function_name,None,function_type) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
-  let equation_lemma_type = 
-    nf_betaiotazeta
-      (interp_constr Evd.empty env ~impls:rec_impls eq)
-  in
+  let ty = interp_type_evars evd env ~impls:rec_impls eq in
+  let evm, nf = Evarutil.nf_evars_and_universes !evd in
+  let equation_lemma_type = nf_betaiotazeta (nf ty) in
+  let function_type = nf function_type in
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
@@ -1471,13 +1480,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in
+  let ctx = Evd.universe_context evm in
+  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
-    interp_constr
+    fst (*FIXME*)(interp_constr
       Evd.empty
       env_with_pre_rec_args
-      r
+      r)
   in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref None in
@@ -1524,6 +1534,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
-      hook)
+      ctx hook)
     ()
-
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 2ef685203..f60eedbe6 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -12,9 +12,9 @@ bool ->
            Constrintern.internalization_env ->
            Constrexpr.constr_expr ->
            Constrexpr.constr_expr ->
-           int -> Constrexpr.constr_expr -> (Names.constant ->
+           int -> Constrexpr.constr_expr -> (Term.pconstant ->
             Term.constr option ref ->
-            Names.constant ->
-            Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+            Term.pconstant ->
+            Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
 
 
diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index b260feab1..2246af64d 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -85,9 +85,9 @@ Notation "x < y" := (rlt x y).
 
 
 Add Relation R req
-  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ )
-  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ )
-  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ )
+  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
+  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
+  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
 as sor_setoid.
 
 
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 68add5b3d..fb16c55c2 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -57,7 +57,7 @@ Variables ceqb cleb : C -> C -> bool.
 Variable phi : C -> R.
 
 (* Power coefficients *)
-Variable E : Set. (* the type of exponents *)
+Variable E : Type. (* the type of exponents *)
 Variable pow_phi : N -> E.
 Variable rpow : R -> E -> R.
 
@@ -78,9 +78,9 @@ Record SORaddon := mk_SOR_addon {
 Variable addon : SORaddon.
 
 Add Relation R req
-  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ )
-  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ )
-  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ )
+  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
+  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
+  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
 as micomega_sor_setoid.
 
 Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
@@ -414,7 +414,7 @@ Proof.
   simpl ; intros.
   destruct (nth_in_or_default n l (Pc cO, Equal)).
   (* index is in bounds *)
-  apply H ; congruence.
+  apply H. congruence.
   (* index is out-of-bounds *)
   inversion H0.
   rewrite e. simpl.
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index d8ab6fd30..78837d4cd 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -317,7 +317,7 @@ Qed.
 
 Require Import QArith.
 
-Inductive ZArithProof : Type :=
+Inductive ZArithProof :=
 | DoneProof
 | RatProof : ZWitness -> ZArithProof -> ZArithProof
 | CutProof : ZWitness -> ZArithProof -> ZArithProof
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 9515c5de9..d11454b27 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -536,10 +536,10 @@ struct
 
   let get_left_construct term =
    match Term.kind_of_term term with
-    | Term.Construct(_,i) -> (i,[| |])
+    | Term.Construct((_,i),_) -> (i,[| |])
     | Term.App(l,rst) ->
        (match Term.kind_of_term l with
-        | Term.Construct(_,i) -> (i,rst)
+        | Term.Construct((_,i),_) -> (i,rst)
         |   _     -> raise ParseError
        )
     | _ ->   raise ParseError
@@ -833,8 +833,8 @@ struct
 
   let parse_zop (op,args) =
    match kind_of_term op with
-    | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
-    |  Ind(n,0) ->
+    | Const (x,_) -> (assoc_const op zop_table, args.(0) , args.(1))
+    | Ind((n,0),_) ->
         if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_Z)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
@@ -842,8 +842,8 @@ struct
 
   let parse_rop (op,args) =
     match kind_of_term op with
-     | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
-     |  Ind(n,0) ->
+     | Const (x,_) -> (assoc_const op rop_table, args.(0) , args.(1))
+     | Ind((n,0),_) ->
         if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_R)
         then (Mc.OpEq, args.(1), args.(2))
         else raise ParseError
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 9b851447c..9b12c5eb3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -170,7 +170,7 @@ let hide_constr,find_constr,clear_constr_tables,dump_tables =
   let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
   (fun h ->
-    try List.assoc_f Constr.equal h !l with Not_found -> failwith "find_contr"),
+    try List.assoc_f eq_constr_nounivs h !l with Not_found -> failwith "find_contr"),
   (fun () -> l := []),
   (fun () -> !l)
 
@@ -350,7 +350,7 @@ let coq_iff = lazy (constant "iff")
 
 (* For unfold *)
 let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
-  | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+  | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
       EvalConstRef kn
   | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant"))
 
@@ -367,15 +367,16 @@ let mk_var v = mkVar (Id.of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
 let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
 let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = mkApp (build_coq_eq (), [| Lazy.force coq_Z; t1; t2 |])
+let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()),
+			 [| Lazy.force coq_Z; t1; t2 |])
 let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
 let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
 let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
 let mk_and t1 t2 =  mkApp (build_coq_and (), [| t1; t2 |])
 let mk_or t1 t2 =  mkApp (build_coq_or (), [| t1; t2 |])
 let mk_not t = mkApp (build_coq_not (), [| t |])
-let mk_eq_rel t1 t2 = mkApp (build_coq_eq (),
-			      [| Lazy.force coq_comparison; t1; t2 |])
+let mk_eq_rel t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()),
+			     [| Lazy.force coq_comparison; t1; t2 |])
 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
 
 let mk_integer n =
@@ -419,7 +420,7 @@ type result =
 let destructurate_prop t =
   let c, args = decompose_app t in
   match kind_of_term c, args with
-    | _, [_;_;_] when eq_constr c (build_coq_eq ()) -> Kapp (Eq,args)
+    | _, [_;_;_] when eq_constr c (Universes.constr_of_global (build_coq_eq ())) -> Kapp (Eq,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args)
@@ -436,11 +437,11 @@ let destructurate_prop t =
     | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args)
-    | Const sp, args ->
+    | Const (sp,_), args ->
 	Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args)
-    | Construct csp , args ->
+    | Construct (csp,_) , args ->
 	Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args)
-    | Ind isp, args ->
+    | Ind (isp,_), args ->
 	Kapp (Other (string_of_path (path_of_global (IndRef isp))),args)
     | Var id,[] -> Kvar id
     | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
@@ -1081,7 +1082,8 @@ let replay_history tactic_normalisation =
 	  let p_initial = [P_APP 2;P_TYPE] in
 	  let tac = shuffle_cancel p_initial e1.body in
 	  let solve_le =
-            let not_sup_sup = mkApp (build_coq_eq (), [|
+            let not_sup_sup = mkApp (Universes.constr_of_global (build_coq_eq ()),
+				     [|
 					Lazy.force coq_comparison;
 					Lazy.force coq_Gt;
 					Lazy.force coq_Gt |])
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 9ee16a582..ea459e551 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -196,9 +196,9 @@ let coerce_meta_in n =
 
 let compute_lhs typ i nargsi =
   match kind_of_term typ with
-    | Ind(sp,0) ->
+    | Ind((sp,0),u) ->
         let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
-        mkApp (mkConstruct ((sp,0),i+1), argsi)
+        mkApp (mkConstructU (((sp,0),i+1),u), argsi)
     | _ -> i_can't_do_that ()
 
 (*s This function builds the pattern from the RHS. Recursive calls are
@@ -221,7 +221,7 @@ let compute_rhs bodyi index_of_f =
 
 let compute_ivs f cs gl =
   let cst = try destConst f with DestKO -> i_can't_do_that () in
-  let body = Environ.constant_value (Global.env()) cst in
+  let body = Environ.constant_value_in (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index ab424c223..7e4475d40 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1284,7 +1284,7 @@ Qed.
 
 (* Extraire une hypothèse de la liste *)
 Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm.
-
+Unset Printing Notations.
 Theorem nth_valid :
  forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
  interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5416e936c..689462704 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -30,11 +30,11 @@ let string_of_global r =
 let destructurate t =
   let c, args = Term.decompose_app t in
   match Term.kind_of_term c, args with
-    | Term.Const sp, args ->
+    | Term.Const (sp,_), args ->
 	Kapp (string_of_global (Globnames.ConstRef sp), args)
-    | Term.Construct csp , args ->
+    | Term.Construct (csp,_) , args ->
 	Kapp (string_of_global (Globnames.ConstructRef csp), args)
-    | Term.Ind isp, args ->
+    | Term.Ind (isp,_), args ->
 	Kapp (string_of_global (Globnames.IndRef isp), args)
     | Term.Var id,[] -> Kvar(Names.Id.to_string id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
@@ -48,9 +48,9 @@ let dest_const_apply t =
   let f,args = Term.decompose_app t in
   let ref =
   match Term.kind_of_term f with
-    | Term.Const sp      -> Globnames.ConstRef sp
-    | Term.Construct csp -> Globnames.ConstructRef csp
-    | Term.Ind isp       -> Globnames.IndRef isp
+    | Term.Const (sp,_)      -> Globnames.ConstRef sp
+    | Term.Construct (csp,_) -> Globnames.ConstructRef csp
+    | Term.Ind (isp,_)       -> Globnames.IndRef isp
     | _ -> raise Destruct
   in  Nametab.basename_of_global ref, args
 
@@ -210,19 +210,26 @@ let rec mk_nat = function
 
 (* Lists *)
 
-let coq_cons =  lazy (constant "cons")
-let coq_nil =  lazy (constant "nil")
+let mkListConst c u = 
+  Term.mkConstructU (Globnames.destConstructRef 
+		     (Coqlib.gen_reference "" ["Init";"Datatypes"] c),
+		     Univ.Instance.of_array [|u|])
 
-let mk_list typ l =
+let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|])
+let coq_nil univ typ =  Term.mkApp (mkListConst "nil" univ, [|typ|])
+
+let mk_list univ typ l =
   let rec loop = function
-    | [] ->
-	Term.mkApp (Lazy.force coq_nil, [|typ|])
+    | [] -> coq_nil univ typ
     | (step :: l) ->
-	Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in
+	Term.mkApp (coq_cons univ typ, [| step; loop l |]) in
   loop l
 
-let mk_plist l = mk_list Term.mkProp l
+let mk_plist = 
+  let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in
+    fun l -> mk_list type1lev Term.mkProp l
 
+let mk_list = mk_list Univ.Level.set
 let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
 
 
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index b8db71e40..4ae1cb94c 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -117,6 +117,7 @@ val do_seq : Term.constr -> Term.constr -> Term.constr
 val do_list : Term.constr list -> Term.constr
 
 val mk_nat : int -> Term.constr
+(** Precondition: the type of the list is in Set *)
 val mk_list : Term.constr -> Term.constr list -> Term.constr
 val mk_plist : Term.types list -> Term.types
 val mk_shuffle_list : Term.constr list -> Term.constr
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 98dd257d5..16081ffe1 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -198,7 +198,7 @@ Theorem get_Full_Gt : forall S, Full S ->
 Proof.
 intros S W;induction W.
 unfold empty,index,get,contents;intros;apply Tget_Tempty.
-unfold index,get,push;simpl contents.
+unfold index,get,push. simpl @contents.
 intros i e;rewrite Tget_Tadd.
 rewrite (Gt_Psucc _ _ e).
 unfold get in IHW.
@@ -209,7 +209,7 @@ Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone.
 intros [index0 contents0] F.
 case F.
 unfold empty,index,get,contents;intros;apply Tget_Tempty.
-unfold index,get,push;simpl contents.
+unfold push,index,get;simpl @contents.
 intros a S.
 rewrite Tget_Tadd.
 rewrite Psucc_Gt.
@@ -231,12 +231,12 @@ Proof.
 intros i a S F.
 case_eq (i ?= index S).
 intro e;rewrite (Pos.compare_eq _ _ e).
-destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
+destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd.
 rewrite Pos.compare_refl;reflexivity.
-intros;destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd.
-simpl index in H;rewrite H;reflexivity.
+intros;destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd.
+simpl @index in H;rewrite H;reflexivity.
 intro H;generalize H;clear H.
-unfold get,push;simpl index;simpl contents.
+unfold get,push;simpl.
 rewrite Tget_Tadd;intro e;rewrite e.
 change (get i S=PNone).
 apply get_Full_Gt;auto.
@@ -260,7 +260,7 @@ Qed.
 Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty.
 intros [ind cont] F one; inversion F.
 reflexivity.
-simpl index in one;assert (h:=Pos.succ_not_1 (index S)).
+simpl @index in one;assert (h:=Pos.succ_not_1 (index S)).
 congruence.
 Qed.
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 96758788a..bff574a06 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -104,20 +104,20 @@ let rec make_form atom_env gls term =
 	    make_atom atom_env (normalize term)
       | Cast(a,_,_) ->
 	  make_form atom_env gls a
-      | Ind ind ->
-	  if Names.eq_ind ind (Lazy.force li_False) then
+      | Ind (ind, _) ->
+	  if Names.eq_ind ind (fst (Lazy.force li_False)) then
 	    Bot
 	  else
 	    make_atom atom_env (normalize term)
       | App(hd,argv) when Int.equal (Array.length argv) 2 ->
 	  begin
 	    try
-	      let ind = destInd hd in
-		if Names.eq_ind ind (Lazy.force li_and) then
+	      let ind, _ = destInd hd in
+		if Names.eq_ind ind (fst (Lazy.force li_and)) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
 		    Conjunct (fa,fb)
-		else if Names.eq_ind ind (Lazy.force li_or) then
+		else if Names.eq_ind ind (fst (Lazy.force li_or)) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
 		    Disjunct (fa,fb)
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 3622c7fe9..2b9dce1b0 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -10,6 +10,7 @@ Require Ring.
 Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms.
 Require Import ZArith_base.
 Set Implicit Arguments.
+(* Set Universe Polymorphism. *)
 
 Section MakeFieldPol.
 
@@ -278,6 +279,21 @@ apply radd_ext.
   [ ring | now rewrite rdiv_simpl ].
 Qed.
 
+Theorem rdiv3 r1 r2 r3 r4 :
+ ~ r2 == 0 ->
+ ~ r4 == 0 ->
+ r1 / r2 - r3 / r4 == (r1 * r4 -  r3 * r2) / (r2 * r4).
+Proof.
+intros H2 H4.
+assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
+transitivity (r1 / r2 + - (r3 / r4)); auto.
+transitivity (r1 / r2 + - r3 / r4); auto.
+transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)).
+apply rdiv2; auto.
+f_equiv.
+transitivity (r1 * r4 + - (r3 * r2)); auto.
+Qed.
+
 Theorem rdiv5 a b : - (a / b) == - a / b.
 Proof.
 now rewrite !rdiv_def, ropp_mul_l.
@@ -696,6 +712,7 @@ Fixpoint PEsimp (e : PExpr C) : PExpr C :=
   | _ => e
  end%poly.
 
+<<<<<<< .merge_file_5Z3Qpn
 Theorem PEsimp_ok e : (PEsimp e === e)%poly.
 Proof.
 induction e; simpl.
@@ -708,6 +725,32 @@ induction e; simpl.
 - rewrite NPEmul_ok. now f_equiv.
 - rewrite NPEopp_ok. now f_equiv.
 - rewrite NPEpow_ok. now f_equiv.
+=======
+Theorem PExpr_simp_correct:
+ forall l e,  NPEeval l (PExpr_simp e) == NPEeval l e.
+clear eq_sym.
+intros l e; elim e; simpl; auto.
+intros e1 He1 e2 He2.
+transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto.
+apply NPEadd_correct.
+simpl; auto.
+intros e1 He1 e2 He2.
+transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))). auto.
+apply NPEsub_correct.
+simpl; auto.
+intros e1 He1 e2 He2.
+transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto.
+apply NPEmul_correct.
+simpl; auto.
+intros e1 He1.
+transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto.
+apply NPEopp_correct.
+simpl; auto.
+intros e1 He1 n;simpl.
+rewrite NPEpow_correct;simpl.
+repeat rewrite pow_th.(rpow_pow_N).
+rewrite He1;auto.
+>>>>>>> .merge_file_U4r9lJ
 Qed.
 
 
@@ -961,6 +1004,7 @@ Fixpoint split_aux e1 p e2 {struct e1}: rsplit :=
        end
   end%poly.
 
+<<<<<<< .merge_file_5Z3Qpn
 Lemma split_aux_ok1 e1 p e2 :
   (let res := match isIn e1 p e2 1 with
        | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3
@@ -971,6 +1015,20 @@ Lemma split_aux_ok1 e1 p e2 :
   e1 ^ Npos p === left res * common res
   /\ e2 === right res * common res)%poly.
 Proof.
+=======
+Lemma split_aux_correct_1 : forall l e1 p e2,
+  let res :=  match isIn e1 p e2 xH with
+       | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
+       | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
+       | None => mk_rsplit (NPEpow e1  (Npos p)) (PEc cI) e2
+       end in
+       NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res))
+   /\
+       NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)).
+Proof.
+ intros. unfold res. clear res; generalize (isIn_correct l e1 p e2 xH).
+ destruct (isIn e1 p e2 1). destruct p0.
+>>>>>>> .merge_file_U4r9lJ
  Opaque NPEpow NPEmul.
  intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH).
  destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl.
@@ -1090,6 +1148,7 @@ Eval compute
 Theorem Pcond_Fnorm l e :
  PCond l (condition (Fnorm e)) ->  ~ (denum (Fnorm e))@l == 0.
 Proof.
+<<<<<<< .merge_file_5Z3Qpn
 induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
  simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok.
 - simpl. rewrite phi_1; exact rI_neq_rO.
@@ -1112,6 +1171,93 @@ induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
   + apply split_nz_r, Hc1.
 - rewrite NPEpow_ok. apply PEpow_nz, IHe, Hc.
 Qed.
+=======
+ induction p;simpl.
+  intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
+  apply IHp.
+  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
+  reflexivity.
+  rewrite H1. ring. rewrite Hp;ring.
+  intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
+  reflexivity. rewrite Hp;ring. trivial.
+Qed.
+
+Theorem Pcond_Fnorm:
+ forall l e,
+ PCond l (condition (Fnorm e)) ->  ~ NPEeval l ((Fnorm e).(denum)) == 0.
+intros l e; elim e.
+ simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
+ simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl in Hcond.
+   simpl @denum.
+   rewrite NPEmul_correct.
+   simpl.
+   apply field_is_integral_domain.
+   intros HH; case Hrec1; auto.
+     apply PCond_app_inv_l with (1 := Hcond).
+   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
+   rewrite NPEmul_correct; simpl; rewrite HH; ring.
+   intros HH; case Hrec2; auto.
+     apply PCond_app_inv_r with (1 := Hcond).
+   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl @condition in Hcond.
+   simpl @denum.
+   rewrite NPEmul_correct.
+   simpl.
+   apply field_is_integral_domain.
+   intros HH; case Hrec1; auto.
+     apply PCond_app_inv_l with (1 := Hcond).
+   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
+   rewrite NPEmul_correct; simpl; rewrite HH; ring.
+   intros HH; case Hrec2; auto.
+     apply PCond_app_inv_r with (1 := Hcond).
+   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl in Hcond.
+   simpl @denum.
+   rewrite NPEmul_correct.
+   simpl.
+   apply field_is_integral_domain.
+  intros HH; apply Hrec1.
+    apply PCond_app_inv_l with (1 := Hcond).
+    rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
+    rewrite NPEmul_correct; simpl; rewrite HH; ring.
+  intros HH; apply Hrec2.
+    apply PCond_app_inv_r with (1 := Hcond).
+    rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))).
+    rewrite NPEmul_correct; simpl; rewrite HH; ring.
+ intros e1 Hrec1 Hcond.
+   simpl in Hcond.
+   simpl @denum.
+   auto.
+ intros e1 Hrec1 Hcond.
+   simpl in Hcond.
+   simpl @denum.
+   apply PCond_cons_inv_l with (1:=Hcond).
+ intros e1 Hrec1 e2 Hrec2 Hcond.
+   simpl in Hcond.
+   simpl @denum.
+   rewrite NPEmul_correct.
+   simpl.
+   apply field_is_integral_domain.
+    intros HH; apply Hrec1.
+    specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
+    apply PCond_app_inv_l with (1 := Hcond1).
+    rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
+    rewrite NPEmul_correct; simpl; rewrite HH; ring.
+    intros HH; apply PCond_cons_inv_l with (1:=Hcond).
+    rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))).
+    rewrite NPEmul_correct; simpl; rewrite HH; ring.
+ simpl;intros e1 Hrec1 n Hcond.
+  rewrite NPEpow_correct.
+  simpl;rewrite pow_th.(rpow_pow_N).
+  destruct n;simpl;intros.
+  apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto.
+Qed.
+Hint Resolve Pcond_Fnorm.
+>>>>>>> .merge_file_U4r9lJ
 
 
 (***************************************************************************
@@ -1502,11 +1648,21 @@ Hypothesis ceqb_complete : forall c1 c2, [c1] == [c2] -> ceqb c1 c2 = true.
 
 Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2).
 Proof.
+<<<<<<< .merge_file_5Z3Qpn
 assert (H := morph_eq CRmorph c1 c2).
 assert (H' := @ceqb_complete c1 c2).
 destruct (ceqb c1 c2); constructor.
 - now apply H.
 - intro E. specialize (H' E). discriminate.
+=======
+intros.
+generalize (fun h => X (morph_eq CRmorph _ _ h)).
+generalize (@ceqb_complete c1 c2).
+case (c1 ?=! c2); auto; intros.
+apply X0.
+red; intro.
+absurd (false = true); auto;  discriminate.
+>>>>>>> .merge_file_U4r9lJ
 Qed.
 
 Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
@@ -1766,4 +1922,4 @@ End Field.
 End Complete.
 
 Arguments FEO [C].
-Arguments FEI [C].
\ No newline at end of file
+Arguments FEI [C].
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index ca178dd38..07f49cc4f 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -15,6 +15,7 @@ Require Import Ring_polynom.
 Import List.
 
 Set Implicit Arguments.
+(* Set Universe Polymorphism. *)
 
 Import RingSyntax.
 
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 6ffa54866..5ec73950b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -6,12 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+
 Set Implicit Arguments.
-Require Import Setoid Morphisms BinList BinPos BinNat BinInt.
+Require Import Setoid Morphisms. 
+Require Import BinList BinPos BinNat BinInt.
 Require Export Ring_theory.
-
 Local Open Scope positive_scope.
 Import RingSyntax.
+(* Set Universe Polymorphism. *)
 
 Section MakeRingPol.
 
@@ -678,7 +680,7 @@ Section MakeRingPol.
   - add_permut.
   - destruct p; simpl;
     rewrite ?jump_pred_double; add_permut.
-  - destr_pos_sub; intros ->;Esimpl.
+  - destr_pos_sub; intros ->; Esimpl.
     + rewrite IHP';rsimpl. add_permut.
     + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut.
     + rewrite IHP1, pow_pos_add;rsimpl. add_permut.
@@ -796,9 +798,9 @@ Section MakeRingPol.
      P@l == Q@l + [c] * R@l.
  Proof.
  revert l.
- induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl.
- - assert (H := div_th.(div_eucl_th) c0 c).
-   destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
+ induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. 
+ - assert (H := div_th.(div_eucl_th) c0 c). 
+   destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. 
  - destr_factor. Esimpl.
  - destr_factor. Esimpl. add_permut.
  Qed.
@@ -807,11 +809,12 @@ Section MakeRingPol.
    let (c,M) := cM in
    let (Q,R) := MFactor P c M in
      P@l == Q@l + [c] * M@@l * R@l.
- Proof.
+ Proof. 
  destruct cM as (c,M). revert M l.
- induction P; destruct M; intros l; simpl; auto;
+ induction P; destruct M; intros l; simpl; auto; 
  try (case ceqb_spec; intro He);
-  try (case Pos.compare_spec; intros He); rewrite ?He;
+  try (case Pos.compare_spec; intros He);
+  rewrite ?He;
    destr_factor; simpl; Esimpl.
  - assert (H := div_th.(div_eucl_th) c0 c).
    destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
@@ -869,9 +872,9 @@ Section MakeRingPol.
  Lemma PSubstL1_ok n LM1 P1 l :
    MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l.
  Proof.
- revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros.
- - reflexivity.
- - rewrite <- IH by intuition. now apply PNSubst1_ok.
+ revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. 
+ - reflexivity. 
+ - rewrite <- IH by intuition; now apply PNSubst1_ok.
  Qed.
 
  Lemma PSubstL_ok n LM1 P1 P2 l :
@@ -1483,4 +1486,4 @@ Qed.
 End MakeRingPol.
 
 Arguments PEO [C].
-Arguments PEI [C].
\ No newline at end of file
+Arguments PEI [C].
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 42ce4edca..d56f50bec 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -28,6 +28,8 @@ Reserved Notation "x == y" (at level 70, no associativity).
 End RingSyntax.
 Import RingSyntax.
 
+(* Set Universe Polymorphism. *)
+
 Section Power.
  Variable R:Type.
  Variable rI : R.
@@ -252,6 +254,7 @@ Section ALMOST_RING.
 
  Section SEMI_RING.
  Variable SReqe : sring_eq_ext radd rmul req.
+
    Add Morphism radd : radd_ext1.  exact (SRadd_ext SReqe). Qed.
    Add Morphism rmul : rmul_ext1.  exact (SRmul_ext SReqe). Qed.
  Variable SRth : semi_ring_theory 0 1 radd rmul req.
@@ -503,7 +506,6 @@ Qed.
 
 End ALMOST_RING.
 
-
 Section AddRing.
 
 (* Variable R : Type.
@@ -528,7 +530,6 @@ Inductive ring_kind : Type :=
     (_ : ring_morph rO rI radd rmul rsub ropp req
                     cO cI cadd cmul csub copp ceqb phi).
 
-
 End AddRing.
 
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 235ee8d72..7ed8e03a9 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -74,7 +74,7 @@ and mk_clos_app_but f_map subs f args n =
       | None -> mk_clos_app_but f_map subs f args (n+1)
 
 let interp_map l t =
-  try Some(List.assoc_f eq_constr t l) with Not_found -> None
+  try Some(List.assoc_f eq_constr_nounivs t l) with Not_found -> None
 
 let protect_maps = ref String.Map.empty
 let add_map s m = protect_maps := String.Map.add s m !protect_maps
@@ -104,7 +104,7 @@ END;;
 (****************************************************************************)
 
 let closed_term t l =
-  let l = List.map constr_of_global l in
+  let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
   if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt())
 ;;
@@ -141,15 +141,24 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 
 let ic c =
   let env = Global.env() and sigma = Evd.empty in
-  Constrintern.interp_constr sigma env c
+  Constrintern.interp_open_constr sigma env c
+
+let ic_unsafe c = (*FIXME remove *)
+  let env = Global.env() and sigma = Evd.empty in
+    fst (Constrintern.interp_constr sigma env c)
 
 let ty c = Typing.type_of (Global.env()) Evd.empty c
 
-let decl_constant na c =
+let decl_constant na ctx c =
+  let vars = Universes.universes_of_constr c in
+  let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
   mkConst(declare_constant (Id.of_string na) (DefinitionEntry
-    { const_entry_body = c;
+    { const_entry_body = Future.from_val (c, Declareops.no_seff);
       const_entry_secctx = None;
       const_entry_type = None;
+      const_entry_polymorphic = false;
+      const_entry_universes = Univ.ContextSet.to_context ctx;
+      const_entry_proj = None;
       const_entry_opaque = true;
       const_entry_inline_code = false;
       const_entry_feedback = None;
@@ -182,7 +191,11 @@ let dummy_goal env =
     Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
   {Evd.it = gl; Evd.sigma = sigma}
 
-let exec_tactic env n f args =
+let constr_of v = match Value.to_constr v with
+  | Some c -> c
+  | None -> failwith "Ring.exec_tactic: anomaly"
+
+let exec_tactic env evd n f args =
   let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
   let res = ref [||] in
   let get_res ist =
@@ -192,13 +205,14 @@ let exec_tactic env n f args =
   let getter =
     Tacexp(TacFun(List.map(fun id -> Some id) lid,
                   Tacintern.glob_tactic(tacticIn get_res))) in
-  let _ =
-    Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) (dummy_goal env) in
-  !res
-
-let constr_of v = match Value.to_constr v with
-  | Some c -> c
-  | None -> failwith "Ring.exec_tactic: anomaly"
+  let gls =
+    (fun gl -> 
+      let sigma = gl.Evd.sigma in
+	tclTHEN (Refiner.tclEVARS (Evd.merge sigma evd))
+	  (Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter])))) gl)
+      (dummy_goal env) in
+  let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
+    Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
@@ -209,6 +223,8 @@ let stdlib_modules =
 
 let coq_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)
+let coq_reference c =
+  lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
 let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
 let coq_cons = coq_constant "cons"
@@ -217,8 +233,15 @@ let coq_None = coq_constant "None"
 let coq_Some = coq_constant "Some"
 let coq_eq = coq_constant "eq"
 
+let coq_pcons = coq_reference "cons"
+let coq_pnil = coq_reference "nil"
+
 let lapp f args = mkApp(Lazy.force f,args)
 
+let plapp evd f args = 
+  let fc = Evarutil.e_new_global evd (Lazy.force f) in
+    mkApp(fc,args)
+
 let dest_rel0 t =
   match kind_of_term t with
   | App(f,args) when Array.length args >= 2 ->
@@ -247,6 +270,8 @@ let plugin_modules =
 
 let my_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
+let my_reference c =
+  lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
 let new_ring_path =
   DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
@@ -266,9 +291,9 @@ let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 let coq_almost_ring_theory = my_constant "almost_ring_theory"
 
 (* setoid and morphism utilities *)
-let coq_eq_setoid = my_constant "Eqsth"
-let coq_eq_morph = my_constant "Eq_ext"
-let coq_eq_smorph = my_constant "Eq_s_ext"
+let coq_eq_setoid = my_reference "Eqsth"
+let coq_eq_morph = my_reference "Eq_ext"
+let coq_eq_smorph = my_reference "Eq_s_ext"
 
 (* ring -> almost_ring utilities *)
 let coq_ring_theory = my_constant "ring_theory"
@@ -295,8 +320,8 @@ let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
 let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
 
 (* hypothesis *)
-let coq_mkhypo = my_constant "mkhypo"
-let coq_hypo = my_constant "hypo"
+let coq_mkhypo = my_reference "mkhypo"
+let coq_hypo = my_reference "hypo"
 
 (* Equality: do not evaluate but make recursive call on both sides *)
 let map_with_eq arg_map c =
@@ -415,14 +440,14 @@ let theory_to_obj : ring_info -> obj =
       classify_function = (fun x -> Substitute x)}
 
 
-let setoid_of_relation env a r =
-  let evm = Evd.empty in
+let setoid_of_relation env evd a r =
   try
-    lapp coq_mk_Setoid
-      [|a ; r ;
-	Rewrite.get_reflexive_proof env evm a r ;
-	Rewrite.get_symmetric_proof env evm a r ;
-	Rewrite.get_transitive_proof env evm a r |]
+    let evm = !evd, Int.Set.empty in
+    let evm, refl = Rewrite.PropGlobal.get_reflexive_proof env evm a r in
+    let evm, sym = Rewrite.PropGlobal.get_symmetric_proof env evm a r in
+    let evm, trans = Rewrite.PropGlobal.get_transitive_proof env evm a r in
+      evd := fst evm;
+      lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
   with Not_found ->
     error "cannot find setoid relation"
 
@@ -435,7 +460,7 @@ let op_smorph r add mul req m1 m2 =
 (* let default_ring_equality (r,add,mul,opp,req) = *)
 (*   let is_setoid = function *)
 (*       {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
-(*         eq_constr req rel (\* Qu: use conversion ? *\) *)
+(*         eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *)
 (*     | _ -> false in *)
 (*   match default_relation_for_carrier ~filter:is_setoid r with *)
 (*       Leibniz _ -> *)
@@ -450,7 +475,7 @@ let op_smorph r add mul req m1 m2 =
 (*         let is_endomorphism = function *)
 (*             { args=args } -> List.for_all *)
 (*                 (function (var,Relation rel) -> *)
-(*                   var=None && eq_constr req rel *)
+(*                   var=None && eq_constr_nounivs req rel *)
 (*                   | _ -> false) args in *)
 (*         let add_m = *)
 (*           try default_morphism ~filter:is_endomorphism add *)
@@ -485,17 +510,19 @@ let op_smorph r add mul req m1 m2 =
 (*             op_smorph r add mul req add_m.lem mul_m.lem) in *)
 (*         (setoid,op_morph) *)
 
-let ring_equality (r,add,mul,opp,req) =
+let ring_equality env evd (r,add,mul,opp,req) =
   match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
-	let setoid = lapp coq_eq_setoid [|r|] in
+    | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) ->
+	let setoid = plapp evd coq_eq_setoid [|r|] in
 	let op_morph =
 	  match opp with
-              Some opp -> lapp coq_eq_morph [|r;add;mul;opp|]
-            | None -> lapp coq_eq_smorph [|r;add;mul|] in
+              Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
+            | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+	let setoid = Typing.solve_evars env evd setoid in
+	let op_morph = Typing.solve_evars env evd op_morph in
 	  (setoid,op_morph)
     | _ ->
-	let setoid = setoid_of_relation (Global.env ()) r req in
+	let setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
 	let add_m, add_m_lem =
 	  try Rewrite.default_morphism signature add
@@ -532,22 +559,22 @@ let ring_equality (r,add,mul,opp,req) =
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 
-let build_setoid_params r add mul opp req eqth =
+let build_setoid_params env evd r add mul opp req eqth =
   match eqth with
       Some th -> th
-    | None -> ring_equality (r,add,mul,opp,req)
+    | None -> ring_equality env evd (r,add,mul,opp,req)
 
 let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
   match kind_of_term th_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when eq_constr f (Lazy.force coq_almost_ring_theory) ->
+        when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) ->
           (None,r,zero,one,add,mul,Some sub,Some opp,req)
     | App(f,[|r;zero;one;add;mul;req|])
-        when eq_constr f (Lazy.force coq_semi_ring_theory) ->
+        when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) ->
         (Some true,r,zero,one,add,mul,None,None,req)
     | App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when eq_constr f (Lazy.force coq_ring_theory) ->
+        when eq_constr_nounivs f (Lazy.force coq_ring_theory) ->
         (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
     | _ -> error "bad ring structure"
 
@@ -557,10 +584,10 @@ let dest_morph env sigma m_spec =
   match kind_of_term m_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req;
               c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-        when eq_constr f (Lazy.force coq_ring_morph) ->
+        when eq_constr_nounivs f (Lazy.force coq_ring_morph) ->
           (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
     | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when eq_constr f (Lazy.force coq_semi_morph) ->
+        when eq_constr_nounivs f (Lazy.force coq_semi_morph) ->
         (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
     | _ -> error "bad morphism structure"
 
@@ -591,18 +618,22 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
         let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in
               TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
 
-let make_hyp env c =
-  let t = Retyping.get_type_of env Evd.empty c in
-  lapp coq_mkhypo [|t;c|]
-
-let make_hyp_list env lH =
-  let carrier = Lazy.force coq_hypo in
-  List.fold_right
-    (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH
-    (lapp coq_nil [|carrier|])
-
-let interp_power env pow =
-  let carrier = Lazy.force coq_hypo in
+let make_hyp env evd c =
+  let t = Retyping.get_type_of env !evd c in
+   plapp evd coq_mkhypo [|t;c|]
+
+let make_hyp_list env evd lH =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+  let l = 
+    List.fold_right
+      (fun c l -> plapp evd coq_pcons [|carrier; (make_hyp env evd c); l|]) lH
+      (plapp evd coq_pnil [|carrier|])
+  in 
+  let l' = Typing.solve_evars env evd l in
+    Evarutil.nf_evars_universes !evd l'
+
+let interp_power env evd pow =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match pow with
   | None ->
       let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
@@ -613,47 +644,47 @@ let interp_power env pow =
         | CstTac t -> Tacintern.glob_tactic t
         | Closed lc ->
             closed_term_ast (List.map Smartlocate.global_with_alias lc) in
-      let spec = make_hyp env (ic spec) in
+      let spec = make_hyp env evd (ic_unsafe spec) in
       (tac, lapp coq_Some [|carrier; spec|])
 
-let interp_sign env sign =
-  let carrier = Lazy.force coq_hypo in
+let interp_sign env evd sign =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match sign with
   | None -> lapp coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env (ic spec) in
+      let spec = make_hyp env evd (ic_unsafe spec) in
       lapp coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let interp_div env div =
-  let carrier = Lazy.force coq_hypo in
+let interp_div env evd div =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match div with
   | None -> lapp coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env (ic spec) in
+      let spec = make_hyp env evd (ic_unsafe spec) in
       lapp coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
+let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
   check_required_library (cdir@["Ring_base"]);
   let env = Global.env() in
-  let sigma = Evd.empty in
   let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
-  let (sth,ext) = build_setoid_params r add mul opp req eqth in
-  let (pow_tac, pspec) = interp_power env power in
-  let sspec = interp_sign env sign in
-  let dspec = interp_div env div in
+  let evd = ref sigma in
+  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
+  let (pow_tac, pspec) = interp_power env evd power in
+  let sspec = interp_sign env evd sign in
+  let dspec = interp_div env evd div in
   let rk = reflect_coeff morphth in
-  let params =
-    exec_tactic env 5 (zltac "ring_lemmas")
+  let params,ctx =
+    exec_tactic env !evd 5 (zltac "ring_lemmas")
       (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in
-  let lemma1 = constr_of params.(3) in
-  let lemma2 = constr_of params.(4) in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
 
   let lemma1 =
-    decl_constant (Id.to_string name^"_ring_lemma1") (Future.from_val ( lemma1,Declareops.no_seff)) in
+    decl_constant (Id.to_string name^"_ring_lemma1") ctx (Future.from_val ( lemma1,Declareops.no_seff)) in
   let lemma2 =
-    decl_constant (Id.to_string name^"_ring_lemma2") (Future.from_val ( lemma2,Declareops.no_seff)) in
+    decl_constant (Id.to_string name^"_ring_lemma2") ctx (Future.from_val ( lemma2,Declareops.no_seff)) in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -670,9 +701,9 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
         { ring_carrier = r;
           ring_req = req;
           ring_setoid = sth;
-          ring_ext = constr_of params.(1);
-          ring_morph = constr_of params.(2);
-          ring_th = constr_of params.(0);
+          ring_ext = params.(1);
+          ring_morph = params.(2);
+          ring_th = params.(0);
           ring_cst_tac = cst_tac;
 	  ring_pow_tac = pow_tac;
           ring_lemma1 = lemma1;
@@ -692,16 +723,11 @@ type 'constr ring_mod =
   | Sign_spec of Constrexpr.constr_expr
   | Div_spec of Constrexpr.constr_expr
 
-let ic_coeff_spec = function
-  | Computational t -> Computational (ic t)
-  | Morphism t -> Morphism (ic t)
-  | Abstract -> Abstract
-
 
 VERNAC ARGUMENT EXTEND ring_mod
-  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
+  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic_unsafe eq_test)) ]
   | [ "abstract" ] -> [ Ring_kind Abstract ]
-  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
+  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic_unsafe morph)) ]
   | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
   | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
   | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
@@ -732,11 +758,11 @@ let process_ring_mods l =
     | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
     | Pre_tac t -> set_once "preprocess tactic" pre t
     | Post_tac t -> set_once "postprocess tactic" post t
-    | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext)
+    | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
     | Pow_spec(t,spec) -> set_once "power" power (t,spec)
     | Sign_spec t -> set_once "sign" sign t
     | Div_spec t -> set_once "div" div t) l;
-  let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in
+  let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
 VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
@@ -762,10 +788,11 @@ let make_args_list rl t =
   | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2]
   | _ -> rl
 
-let make_term_list carrier rl =
-  List.fold_right
-    (fun x l -> lapp coq_cons [|carrier;x;l|]) rl
-    (lapp coq_nil [|carrier|])
+let make_term_list env evd carrier rl =
+  let l = List.fold_right
+    (fun x l -> plapp evd coq_pcons [|carrier;x;l|]) rl
+    (plapp evd coq_pnil [|carrier|])
+  in Typing.solve_evars env evd l
 
 let ltac_ring_structure e =
   let req = carg e.ring_req in
@@ -786,12 +813,15 @@ let ring_lookup (f:glob_tactic_expr) lH rl t =
   Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let rl = make_args_list rl t in
-    let e = find_ring_structure env sigma rl in
-    let rl = carg (make_term_list e.ring_carrier rl) in
-    let lH = carg (make_hyp_list env lH) in
-    let ring = ltac_ring_structure e in
-    ltac_apply f (ring@[lH;rl])
+    try (* find_ring_strucure can raise an exception *)
+      let evdref = ref sigma in
+      let rl = make_args_list rl t in
+      let e = find_ring_structure env sigma rl in
+      let rl = carg (make_term_list env evdref e.ring_carrier rl) in
+      let lH = carg (make_hyp_list env evdref lH) in
+      let ring = ltac_ring_structure e in
+      Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 TACTIC EXTEND ring_lookup
@@ -850,26 +880,26 @@ let _ = Redexpr.declare_reduction "simpl_field_expr"
 let afield_theory = my_constant "almost_field_theory"
 let field_theory = my_constant "field_theory"
 let sfield_theory = my_constant "semi_field_theory"
-let af_ar = my_constant"AF_AR"
-let f_r = my_constant"F_R"
-let sf_sr = my_constant"SF_SR"
-let dest_field env sigma th_spec =
-  let th_typ = Retyping.get_type_of env sigma th_spec in
+let af_ar = my_reference"AF_AR"
+let f_r = my_reference"F_R"
+let sf_sr = my_reference"SF_SR"
+let dest_field env evd th_spec =
+  let th_typ = Retyping.get_type_of env !evd th_spec in
   match kind_of_term th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when eq_constr f (Lazy.force afield_theory) ->
-        let rth = lapp af_ar
+        when eq_constr_nounivs f (Lazy.force afield_theory) ->
+        let rth = plapp evd af_ar
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when eq_constr f (Lazy.force field_theory) ->
+        when eq_constr_nounivs f (Lazy.force field_theory) ->
         let rth =
-          lapp f_r
+          plapp evd f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
-        when eq_constr f (Lazy.force sfield_theory) ->
-        let rth = lapp sf_sr
+        when eq_constr_nounivs f (Lazy.force sfield_theory) ->
+        let rth = plapp evd sf_sr
           [|r;zero;one;add;mul;div;inv;req;th_spec|] in
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
     | _ -> error "bad field structure"
@@ -960,12 +990,12 @@ let ftheory_to_obj : field_info -> obj =
       subst_function = subst_th;
       classify_function = (fun x -> Substitute x) }
 
-let field_equality r inv req =
+let field_equality evd r inv req =
   match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
-        mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
+    | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) ->
+        mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
     | _ ->
-	let _setoid = setoid_of_relation (Global.env ()) r req in
+	let _setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req)],Some(r,Some req) in
 	let inv_m, inv_m_lem =
 	  try Rewrite.default_morphism signature inv
@@ -973,36 +1003,41 @@ let field_equality r inv req =
             error "field inverse should be declared as a morphism" in
 	  inv_m_lem
 
-let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
+let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv =
   check_required_library (cdir@["Field_tac"]);
   let env = Global.env() in
-  let sigma = Evd.empty in
+  let evd = ref sigma in
   let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
-    dest_field env sigma fth in
-  let (sth,ext) = build_setoid_params r add mul opp req eqth in
+    dest_field env evd fth in
+  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
   let eqth = Some(sth,ext) in
-  let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign odiv in
-  let (pow_tac, pspec) = interp_power env power in
-  let sspec = interp_sign env sign in
-  let dspec = interp_div env odiv in
-  let inv_m = field_equality r inv req in
+  let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in
+  let (pow_tac, pspec) = interp_power env evd power in
+  let sspec = interp_sign env evd sign in
+  let dspec = interp_div env evd odiv in
+  let inv_m = field_equality evd r inv req in
   let rk = reflect_coeff morphth in
-  let params =
-    exec_tactic env 9 (field_ltac"field_lemmas")
+  let params,ctx =
+    exec_tactic env !evd 9 (field_ltac"field_lemmas")
       (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in
-  let lemma1 = constr_of params.(3) in
-  let lemma2 = constr_of params.(4) in
-  let lemma3 = constr_of params.(5) in
-  let lemma4 = constr_of params.(6) in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
+  let lemma3 = params.(5) in
+  let lemma4 = params.(6) in
   let cond_lemma =
     match inj with
       | Some thm -> mkApp(constr_of params.(8),[|thm|])
       | None -> constr_of params.(7) in
-  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") (Future.from_val (lemma1,Declareops.no_seff)) in
-  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") (Future.from_val (lemma2,Declareops.no_seff)) in
-  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") (Future.from_val (lemma3,Declareops.no_seff)) in
-  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") (Future.from_val (lemma4,Declareops.no_seff)) in
-  let cond_lemma = decl_constant (Id.to_string name^"_lemma5") (Future.from_val (cond_lemma,Declareops.no_seff)) in
+  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1")
+    ctx (Future.from_val (lemma1,Declareops.no_seff)) in
+  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") 
+    ctx (Future.from_val (lemma2,Declareops.no_seff)) in
+  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") 
+    ctx (Future.from_val (lemma3,Declareops.no_seff)) in
+  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") 
+    ctx (Future.from_val (lemma4,Declareops.no_seff)) in
+  let cond_lemma = decl_constant (Id.to_string name^"_lemma5") 
+    ctx (Future.from_val (cond_lemma,Declareops.no_seff)) in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -1053,12 +1088,12 @@ let process_field_mods l =
         set_once "tactic recognizing constants" cst_tac t
     | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
     | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
-    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext)
+    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
     | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
     | Ring_mod(Sign_spec t) -> set_once "sign" sign t
     | Ring_mod(Div_spec t) -> set_once "div" div t
-    | Inject i -> set_once "infinite property" inj (ic i)) l;
-  let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in
+    | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l;
+  let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
 VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
@@ -1094,12 +1129,15 @@ let field_lookup (f:glob_tactic_expr) lH rl t =
   Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let rl = make_args_list rl t in
-    let e = find_field_structure env sigma rl in
-    let rl = carg (make_term_list e.field_carrier rl) in
-    let lH = carg (make_hyp_list env lH) in
-    let field = ltac_field_structure e in
-    ltac_apply f (field@[lH;rl])
+    try
+      let evdref = ref sigma in
+      let rl = make_args_list rl t in
+      let e = find_field_structure env sigma rl in
+      let rl = carg (make_term_list env evdref e.field_carrier rl) in
+      let lH = carg (make_hyp_list env evdref lH) in
+      let field = ltac_field_structure e in
+      Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 790e1970b..5c060c3d6 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -37,9 +37,9 @@ let interp_ascii dloc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,if Int.equal mp 0 then glob_false else glob_true)
+     GRef (dloc,if Int.equal mp 0 then glob_false else glob_true,None)
      :: (aux (n-1) (p/2)) in
-  GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
+  GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p)
 
 let interp_ascii_string dloc s =
   let p =
@@ -55,12 +55,12 @@ let interp_ascii_string dloc s =
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] when Int.equal n 0 -> 0
-    | GRef (_,k)::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | GRef (_,k)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | GRef (_,k,_)::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
     let aux = function
-    | GApp (_,GRef (_,k),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
+    | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -76,4 +76,4 @@ let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([GRef (Loc.ghost,static_glob_Ascii)], uninterp_ascii_string, true)
+    ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index c3dad0a10..bad099d4f 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -30,8 +30,8 @@ let nat_of_int dloc n =
 	   strbrk "working with large numbers in nat (observed threshold " ++
 	   strbrk "may vary from 5000 to 70000 depending on your system " ++
 	   strbrk "limits and on the command executed).");
-      let ref_O = GRef (dloc, glob_O) in
-      let ref_S = GRef (dloc, glob_S) in
+      let ref_O = GRef (dloc, glob_O, None) in
+      let ref_S = GRef (dloc, glob_S, None) in
       let rec mk_nat acc n =
 	if n <> zero then
 	  mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n)
@@ -50,8 +50,8 @@ let nat_of_int dloc n =
 exception Non_closed_number
 
 let rec int_of_nat = function
-  | GApp (_,GRef (_,s),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
-  | GRef (_,z) when Globnames.eq_gr z glob_O -> zero
+  | GApp (_,GRef (_,s,_),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+  | GRef (_,z,_) when Globnames.eq_gr z glob_O -> zero
   | _ -> raise Non_closed_number
 
 let uninterp_nat p =
@@ -67,4 +67,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,datatypes_module_name)
     nat_of_int
-    ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true)
+    ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 8e09c974a..a6b3d9038 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -83,9 +83,9 @@ exception Non_closed
 (* parses a *non-negative* integer (from bigint.ml) into an int31
    wraps modulo 2^31 *)
 let int31_of_pos_bigint dloc n =
-  let ref_construct = GRef (dloc, int31_construct) in
-  let ref_0 = GRef (dloc, int31_0) in
-  let ref_1 = GRef (dloc, int31_1) in
+  let ref_construct = GRef (dloc, int31_construct, None) in
+  let ref_0 = GRef (dloc, int31_0, None) in
+  let ref_1 = GRef (dloc, int31_1, None) in
   let rec args counter n =
     if counter <= 0 then
       []
@@ -110,12 +110,12 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> cur
-      | (GRef (_,b))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
-      | (GRef (_,b))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
+      | (GRef (_,b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+      | (GRef (_,b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
       | _ -> raise Non_closed
   in
   function
-  | GApp (_, GRef (_, c), args) when eq_gr c int31_construct -> args_parsing args zero
+  | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
 let uninterp_int31 i =
@@ -128,7 +128,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([GRef (Loc.ghost, int31_construct)],
+  ([GRef (Loc.ghost, int31_construct, None)],
    uninterp_int31,
    true)
 
@@ -159,8 +159,8 @@ let height bi =
 
 (* n must be a non-negative integer (from bigint.ml) *)
 let word_of_pos_bigint dloc hght n =
-  let ref_W0 = GRef (dloc, zn2z_W0) in
-  let ref_WW = GRef (dloc, zn2z_WW) in
+  let ref_W0 = GRef (dloc, zn2z_W0, None) in
+  let ref_WW = GRef (dloc, zn2z_WW, None) in
   let rec decomp hgt n =
     if hgt <= 0 then
       int31_of_pos_bigint dloc n
@@ -176,7 +176,7 @@ let word_of_pos_bigint dloc hght n =
 
 let bigN_of_pos_bigint dloc n =
   let h = height n in
-  let ref_constructor = GRef (dloc, bigN_constructor h) in
+  let ref_constructor = GRef (dloc, bigN_constructor h, None) in
   let word = word_of_pos_bigint dloc h n in
   let args =
     if h < n_inlined then [word]
@@ -199,14 +199,14 @@ let interp_bigN dloc n =
 let bigint_of_word =
   let rec get_height rc =
     match rc with
-    | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW ->
+    | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW ->
       1+max (get_height lft) (get_height rght)
     | _ -> 0
   in
   let rec transform hght rc =
     match rc with
-    | GApp (_,GRef(_,c),_) when eq_gr c zn2z_W0-> zero
-    | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW->
+    | GApp (_,GRef(_,c,_),_) when eq_gr c zn2z_W0-> zero
+    | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW->
       let new_hght = hght-1 in
       add (mult (rank new_hght)
              (transform new_hght lft))
@@ -236,7 +236,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if i < n_inlined+1 then
-      GRef (Loc.ghost, bigN_constructor i)::(build (i+1))
+      GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1))
     else
       []
   in
@@ -253,8 +253,8 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
 
 (*** Parsing for bigZ in digital notation ***)
 let interp_bigZ dloc n =
-  let ref_pos = GRef (dloc, bigZ_pos) in
-  let ref_neg = GRef (dloc, bigZ_neg) in
+  let ref_pos = GRef (dloc, bigZ_pos, None) in
+  let ref_neg = GRef (dloc, bigZ_neg, None) in
   if is_pos_or_zero n then
     GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
   else
@@ -262,8 +262,8 @@ let interp_bigZ dloc n =
 
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
-  | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
-  | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_neg ->
+  | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+  | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_neg ->
       let opp_val = bigint_of_bigN one_arg in
       if equal opp_val zero then
 	raise Non_closed
@@ -282,19 +282,19 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([GRef (Loc.ghost, bigZ_pos);
-    GRef (Loc.ghost, bigZ_neg)],
+  ([GRef (Loc.ghost, bigZ_pos, None);
+    GRef (Loc.ghost, bigZ_neg, None)],
    uninterp_bigZ,
    true)
 
 (*** Parsing for bigQ in digital notation ***)
 let interp_bigQ dloc n =
-  let ref_z = GRef (dloc, bigQ_z) in
+  let ref_z = GRef (dloc, bigQ_z, None) in
   GApp (dloc, ref_z, [interp_bigZ dloc n])
 
 let uninterp_bigQ rc =
   try match rc with
-    | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigQ_z ->
+    | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigQ_z ->
 	Some (bigint_of_bigZ one_arg)
     | _ -> None (* we don't pretty-print yet fractions *)
   with Non_closed -> None
@@ -303,5 +303,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([GRef (Loc.ghost, bigQ_z)], uninterp_bigQ,
+  ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ,
    true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 545f205db..dac70c673 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -42,24 +42,24 @@ let four = mult_2 two
 
 (* Unary representation of strictly positive numbers *)
 let rec small_r dloc n =
-  if equal one n then GRef (dloc, glob_R1)
-  else GApp(dloc,GRef (dloc,glob_Rplus),
-            [GRef (dloc, glob_R1);small_r dloc (sub_1 n)])
+  if equal one n then GRef (dloc, glob_R1, None)
+  else GApp(dloc,GRef (dloc,glob_Rplus, None),
+            [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)])
 
 let r_of_posint dloc n =
-  let r1 = GRef (dloc, glob_R1) in
+  let r1 = GRef (dloc, glob_R1, None) in
   let r2 = small_r dloc two in
   let rec r_of_pos n =
     if less_than n four then small_r dloc n
     else
       let (q,r) = div2_with_rest n in
-      let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
-      if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in
-  if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0)
+      let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in
+      if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in
+  if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None)
 
 let r_of_int dloc z =
   if is_strictly_neg z then
-    GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)])
+    GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)])
   else
     r_of_posint dloc z
 
@@ -71,33 +71,33 @@ let bignat_of_r =
 (* for numbers > 1 *)
 let rec bignat_of_pos = function
   (* 1+1 *)
-  | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)])
+  | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)])
       when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two
   (* 1+(1+1) *)
-  | GApp (_,GRef (_,p1), [GRef (_,o1);
-      GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])])
+  | GApp (_,GRef (_,p1,_), [GRef (_,o1,_);
+      GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])])
       when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus &&
            Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three
   (* (1+1)*b *)
-  | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult ->
+  | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult ->
       if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
       mult_2 (bignat_of_pos b)
   (* 1+(1+1)*b *)
-  | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])])
+  | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])])
       when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1  ->
       if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
         add_1 (mult_2 (bignat_of_pos b))
   | _ -> raise Non_closed_number
 in
 let bignat_of_r = function
-  | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero
-  | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one
+  | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero
+  | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one
   | r -> bignat_of_pos r
 in
 bignat_of_r
 
 let bigint_of_r = function
-  | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp ->
+  | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp ->
       let n = bignat_of_r a in
       if Bigint.equal n zero then raise Non_closed_number;
       neg n
@@ -109,11 +109,12 @@ let uninterp_r p =
   with Non_closed_number ->
     None
 
+let mkGRef gr = GRef (Loc.ghost,gr,None)
+
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([GRef(Loc.ghost,glob_Ropp);GRef(Loc.ghost,glob_R0);
-    GRef(Loc.ghost,glob_Rplus);GRef(Loc.ghost,glob_Rmult);
-    GRef(Loc.ghost,glob_R1)],
+  (List.map mkGRef 
+    [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 54206b453..2e696f391 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -32,8 +32,8 @@ open Lazy
 let interp_string dloc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then GRef (dloc, force glob_EmptyString) else
-     GApp (dloc,GRef (dloc, force glob_String),
+     if n = le then GRef (dloc, force glob_EmptyString, None) else
+     GApp (dloc,GRef (dloc, force glob_String, None),
        [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
@@ -41,11 +41,11 @@ let uninterp_string r =
   try
     let b = Buffer.create 16 in
     let rec aux = function
-    | GApp (_,GRef (_,k),[a;s]) when eq_gr k (force glob_String) ->
+    | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) ->
 	(match uninterp_ascii a with
 	  | Some c -> Buffer.add_char b (Char.chr c); aux s
 	  | _ -> raise Non_closed_string)
-    | GRef (_,z) when eq_gr z (force glob_EmptyString) ->
+    | GRef (_,z,_) when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -57,6 +57,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([GRef (Loc.ghost,static_glob_String);
-      GRef (Loc.ghost,static_glob_EmptyString)],
+    ([GRef (Loc.ghost,static_glob_String,None);
+      GRef (Loc.ghost,static_glob_EmptyString,None)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 67e54c017..5131a5f38 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -41,9 +41,9 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat dloc x =
-  let ref_xI = GRef (dloc, glob_xI) in
-  let ref_xH = GRef (dloc, glob_xH) in
-  let ref_xO = GRef (dloc, glob_xO) in
+  let ref_xI = GRef (dloc, glob_xI, None) in
+  let ref_xH = GRef (dloc, glob_xH, None) in
+  let ref_xO = GRef (dloc, glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
       | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
@@ -65,9 +65,9 @@ let interp_positive dloc n =
 (**********************************************************************)
 
 let rec bignat_of_pos = function
-  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (_, a) when Globnames.eq_gr a glob_xH -> Bigint.one
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 let uninterp_positive p =
@@ -83,9 +83,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,binnums)
   interp_positive
-  ([GRef (Loc.ghost, glob_xI);
-    GRef (Loc.ghost, glob_xO);
-    GRef (Loc.ghost, glob_xH)],
+  ([GRef (Loc.ghost, glob_xI, None);
+    GRef (Loc.ghost, glob_xO, None);
+    GRef (Loc.ghost, glob_xH, None)],
    uninterp_positive,
    true)
 
@@ -104,9 +104,9 @@ let n_path = make_path binnums "N"
 
 let n_of_binnat dloc pos_or_neg n =
   if not (Bigint.equal n zero) then
-    GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
+    GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n])
   else
-    GRef (dloc, glob_N0)
+    GRef (dloc, glob_N0, None)
 
 let error_negative dloc =
   user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
@@ -120,8 +120,8 @@ let n_of_int dloc n =
 (**********************************************************************)
 
 let bignat_of_n = function
-  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
-  | GRef (_, a) when Globnames.eq_gr a glob_N0 -> Bigint.zero
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+  | GRef (_, a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_n p =
@@ -134,8 +134,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnums)
   n_of_int
-  ([GRef (Loc.ghost, glob_N0);
-    GRef (Loc.ghost, glob_Npos)],
+  ([GRef (Loc.ghost, glob_N0, None);
+    GRef (Loc.ghost, glob_Npos, None)],
   uninterp_n,
   true)
 
@@ -157,18 +157,18 @@ let z_of_int dloc n =
   if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
+    GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n])
   else
-    GRef (dloc, glob_ZERO)
+    GRef (dloc, glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_z = function
-  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
-  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (_, a) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_z p =
@@ -182,8 +182,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([GRef (Loc.ghost, glob_ZERO);
-    GRef (Loc.ghost, glob_POS);
-    GRef (Loc.ghost, glob_NEG)],
+  ([GRef (Loc.ghost, glob_ZERO, None, None);
+    GRef (Loc.ghost, glob_POS, None, None);
+    GRef (Loc.ghost, glob_NEG, None, None)],
   uninterp_z,
   true)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index bf46065d0..bbaef1e70 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -190,6 +190,7 @@ module CPropRetyping =
 let typeur sigma metamap =
   let rec type_of env cstr=
     match Term.kind_of_term cstr with
+    | T.Proj _ -> assert false
     | T.Meta n ->
           (try T.strip_outer_cast (Int.List.assoc n metamap)
            with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
@@ -202,9 +203,7 @@ let typeur sigma metamap =
           ty
         with Not_found ->
           Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound"))
-    | T.Const c ->
-        let cb = Environ.lookup_constant c env in
-        Typeops.type_of_constant_type env (cb.Declarations.const_type)
+    | T.Const c -> Typeops.type_of_constant_in env c
     | T.Evar ev -> Evd.existential_type sigma ev
     | T.Ind ind -> Inductiveops.type_of_inductive env ind
     | T.Construct cstr -> Inductiveops.type_of_constructor env cstr
@@ -355,7 +354,7 @@ Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the doub
           {DoubleTypeInference.synthesized =
             Reductionops.nf_beta evar_map
              (CPropRetyping.get_type_of env evar_map
-              (Termops.refresh_universes tt)) ;
+              ((* Termops.refresh_universes *) tt)) ;
            DoubleTypeInference.expected = None}
         in
          let innersort =
@@ -484,7 +483,8 @@ print_endline "PASSATO" ; flush stdout ;
           (* Now that we have all the auxiliary functions we  *)
           (* can finally proceed with the main case analysis. *)
           match Term.kind_of_term tt with
-             Term.Rel n ->
+          | Term.Proj _ -> assert false
+          | Term.Rel n ->
               let id =
                match List.nth (Environ.rel_context env) (n - 1) with
                   (Names.Name id,_,_)   -> id
@@ -670,7 +670,7 @@ print_endline "PASSATO" ; flush stdout ;
                 explicit_substitute_and_eta_expand_if_required h
                  (Array.to_list t) t'
                  compute_result_if_eta_expansion_not_required
-           | Term.Const kn ->
+           | Term.Const (kn,u) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
@@ -681,7 +681,7 @@ print_endline "PASSATO" ; flush stdout ;
                 explicit_substitute_and_eta_expand_if_required tt []
                  (List.map snd subst')
                  compute_result_if_eta_expansion_not_required
-           | Term.Ind (kn,i) ->
+           | Term.Ind ((kn,i),u) ->
               let compute_result_if_eta_expansion_not_required _ _ =
                Acic.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i)
               in
@@ -689,7 +689,7 @@ print_endline "PASSATO" ; flush stdout ;
                 explicit_substitute_and_eta_expand_if_required tt []
                  (List.map snd subst')
                  compute_result_if_eta_expansion_not_required
-           | Term.Construct ((kn,i),j) ->
+           | Term.Construct (((kn,i),j),u) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index d54308165..c8717e008 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -64,7 +64,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
        T.Meta n ->
         Errors.error
          "DoubleTypeInference.double_type_of: found a non-instanciated goal"
-
+    | T.Proj _ -> assert false
      | T.Evar ((n,l) as ev) ->
         let ty = Unshare.unshare (Evd.existential_type sigma ev) in
         let jty = execute env sigma ty None in
@@ -99,7 +99,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         Typeops.judge_of_variable env id
 
      | T.Const c ->
-        E.make_judge cstr (Typeops.type_of_constant env c)
+        E.make_judge cstr (fst (Typeops.type_of_constant env c))
 
      | T.Ind ind ->
         E.make_judge cstr (Inductiveops.type_of_inductive env ind)
@@ -112,15 +112,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
          Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in
         let cj = execute env sigma c (Some expectedtype) in
         let pj = execute env sigma p None in
-        let (expectedtypes,_,_) =
+        let (expectedtypes,_) =
          let indspec = Inductive.find_rectype env cj.Environ.uj_type in
           Inductive.type_case_branches env indspec pj cj.Environ.uj_val
         in
         let lfj =
          execute_array env sigma lf
           (Array.map (function x -> Some x) expectedtypes) in
-        let (j,_) = Typeops.judge_of_case env ci pj cj lfj in
-         j
+          Typeops.judge_of_case env ci pj cj lfj 
 
      | T.Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env sigma recdef in
@@ -141,10 +140,10 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 (*CSC: again once Judicael will introduce his non-bugged algebraic       *)
 (*CSC: universes.                                                        *)
 (try
-        Typeops.judge_of_type u
+         (*FIXME*) (Typeops.judge_of_type u)
  with _ -> (* Successor of a non universe-variable universe anomaly *)
   Pp.msg_warning (Pp.str "Universe refresh performed!!!");
-  Typeops.judge_of_type (Termops.new_univ ())
+   (*FIXME*) (Typeops.judge_of_type (Universes.new_univ Names.empty_dirpath))
 )
 
      | T.App (f,args) ->
@@ -165,7 +164,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
           Array.of_list (aux j.Environ.uj_type (Array.to_list args))
         in
         let jl = execute_array env sigma args expected_args in
-        let (j,_) = Typeops.judge_of_apply env j jl in
+        let j = Typeops.judge_of_apply env j jl in
          j
 
      | T.Lambda (name,c1,c2) ->
@@ -212,7 +211,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
         let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
         let tj = execute env sigma t None in
 	let tj = type_judgment env sigma tj in
-        let j, _ = Typeops.judge_of_cast env cj k tj in
+        let j = Typeops.judge_of_cast env cj k tj in
 	 j
     in
      let synthesized = E.j_type judgement in
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 5f26e2bac..3d655920b 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -175,16 +175,17 @@ let find_hyps t =
     | Term.Meta _
     | Term.Evar _
     | Term.Sort _ -> l
+    | Term.Proj _ -> ignore(Errors.todo "Proj in find_hyps"); assert false
     | Term.Cast (te,_, ty) -> aux (aux l te) ty
     | Term.Prod (_,s,t) -> aux (aux l s) t
     | Term.Lambda (_,s,t) -> aux (aux l s) t
     | Term.LetIn (_,s,_,t) -> aux (aux l s) t
     | Term.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
-    | Term.Const con ->
+    | Term.Const (con, _) ->
        let hyps = (Global.lookup_constant con).Declarations.const_hyps in
         map_and_filter l hyps @ l
-    | Term.Ind ind
-    | Term.Construct (ind,_) ->
+    | Term.Ind (ind,_)
+    | Term.Construct ((ind,_),_) ->
        let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in
         map_and_filter l hyps @ l
     | Term.Case (_,t1,t2,b) ->
@@ -243,8 +244,8 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
        let {Declarations.mind_consnames=consnames ;
             Declarations.mind_typename=typename } = p
        in
-        let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in
-        let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
+        let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),Univ.Instance.empty)(*FIXME*) in
+        let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),Univ.Instance.empty)(*FIXME*) in
         let cons =
          (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
           (Array.mapi
@@ -379,7 +380,7 @@ let print internal glob_ref kind xml_library_root =
        let val0 = Declareops.body_of_constant cb in
        let typ = cb.Declarations.const_type in
        let hyps = cb.Declarations.const_hyps in
-       let typ = Typeops.type_of_constant_type (Global.env()) typ in
+       let typ = (* Typeops.type_of_constant_type (Global.env()) *) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Globnames.IndRef (kn,_) ->
        let mib = Global.lookup_mind kn in