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.

75 files changed, 2260 insertions, 919 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index a90a9ce99..76132aed0 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -201,7 +201,7 @@ Qed.
 Lemma nat_compare_spec :
   forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
 Proof.
- intros.
+ intros. 
  destruct (nat_compare x y) eqn:?; constructor.
  apply nat_compare_eq; auto.
  apply <- nat_compare_lt; auto.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 1febb76b6..c3386787d 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -54,7 +54,7 @@ Hint Resolve le_0_n le_Sn_0: arith v62.
 
 Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n.
 Proof.
-  induction n; auto with arith.
+  induction n. auto with arith.  idtac. auto with arith.
   intro; contradiction le_Sn_0 with n.
 Qed.
 Hint Immediate le_n_0_eq: arith v62.
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
new file mode 100644
index 000000000..68a6dcd63
--- /dev/null
+++ b/theories/Classes/CEquivalence.v
@@ -0,0 +1,139 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Typeclass-based setoids. Definitions on [Equivalence].
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+
+Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
+Require Export Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Generalizable Variables A R eqA B S eqB.
+Local Obligation Tactic := try solve [simpl_crelation].
+
+Local Open Scope signature_scope.
+
+Definition equiv `{Equivalence A R} : crelation A := R.
+
+(** Overloaded notations for setoid equivalence and inequivalence.
+    Not to be confused with [eq] and [=]. *)
+
+Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
+
+Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
+
+Local Open Scope equiv_scope.
+
+(** Overloading for [PER]. *)
+
+Definition pequiv `{PER A R} : crelation A := R.
+
+(** Overloaded notation for partial equivalence. *)
+
+Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
+
+(** Shortcuts to make proof search easier. *)
+
+Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
+
+Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
+
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
+
+  Next Obligation.
+  Proof. intros A R sa x y z Hxy Hyz.
+         now transitivity y.
+  Qed.
+
+(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
+
+Ltac setoid_subst H :=
+  match type of H with
+    ?x === ?y => substitute H ; clear H x
+  end.
+
+Ltac setoid_subst_nofail :=
+  match goal with
+    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
+    | _ => idtac
+  end.
+
+(** [subst*] will try its best at substituting every equality in the goal. *)
+
+Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
+
+(** Simplify the goal w.r.t. equivalence. *)
+
+Ltac equiv_simplify_one :=
+  match goal with
+    | [ H : ?x === ?x |- _ ] => clear H
+    | [ H : ?x === ?y |- _ ] => setoid_subst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+    | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
+  end.
+
+Ltac equiv_simplify := repeat equiv_simplify_one.
+
+(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
+   for easy recognition in tactics. *)
+
+Ltac equivify_tac :=
+  match goal with
+    | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+  end.
+
+Ltac equivify := repeat equivify_tac.
+
+Section Respecting.
+
+  (** Here we build an equivalence instance for functions which relates respectful ones only,
+     we do not export it. *)
+
+  Definition respecting `(eqa : Equivalence A (R : crelation A), 
+                          eqb : Equivalence B (R' : crelation B)) : Type :=
+    { morph : A -> B | respectful R R' morph morph }.
+
+  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
+    Equivalence (fun (f g : respecting eqa eqb) => 
+                   forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+
+  Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl.
+
+  Next Obligation.
+  Proof. 
+    intros. intros f g h H H' x y Rxy.
+    unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
+  Qed.
+
+End Respecting.
+
+(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+
+Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
+  Reflexive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) :
+  Symmetric (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_transitive {A} `(transb : Transitive B eqB) :
+  Transitive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
+  Equivalence (pointwise_relation A eqB) | 9.
+Proof. split; apply _. Qed.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
new file mode 100644
index 000000000..5737c88b5
--- /dev/null
+++ b/theories/Classes/CMorphisms.v
@@ -0,0 +1,799 @@
+(* -*- coding: utf-8 -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Typeclass-based morphism definition and standard, minimal instances
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Export Coq.Classes.RelationClasses.
+
+Generalizable Variables A eqA B C D R RA RB RC m f x y.
+Local Obligation Tactic := simpl_crelation.
+
+Set Universe Polymorphism.
+
+(** * Morphisms.
+
+   We now turn to the definition of [Proper] and declare standard instances.
+   These will be used by the [setoid_rewrite] tactic later. *)
+
+(** A morphism for a relation [R] is a proper element of the relation.
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow
+   type for usual morphisms. *)
+Section Proper.
+  Let U := Type.
+  Context {A B : U}.
+
+  Class Proper (R : crelation A) (m : A) :=
+    proper_prf : R m m.
+
+  (** Every element in the carrier of a reflexive relation is a morphism
+   for this relation.  We use a proxy class for this case which is used
+   internally to discharge reflexivity constraints.  The [Reflexive]
+   instance will almost always be used, but it won't apply in general to
+   any kind of [Proper (A -> B) _ _] goal, making proof-search much
+   slower. A cleaner solution would be to be able to set different
+   priorities in different hint bases and select a particular hint
+   database for resolution of a type class constraint. *)
+
+  Class ProperProxy (R : crelation A) (m : A) :=
+    proper_proxy : R m m.
+
+  Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x.
+  Proof. firstorder. Qed.
+  
+  Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  (** Respectful morphisms. *)
+  
+  (** The fully dependent version, not used yet. *)
+  
+  Definition respectful_hetero
+  (A B : Type)
+  (C : A -> Type) (D : B -> Type)
+  (R : A -> B -> Type)
+  (R' : forall (x : A) (y : B), C x -> D y -> Type) :
+    (forall x : A, C x) -> (forall x : B, D x) -> Type :=
+    fun f g => forall x y, R x y -> R' x y (f x) (g y).
+
+  (** The non-dependent version is an instance where we forget dependencies. *)
+  
+  Definition respectful (R : crelation A) (R' : crelation B) : crelation (A -> B) :=
+    Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
+
+End Proper.
+
+(** We favor the use of Leibniz equality or a declared reflexive crelation 
+  when resolving [ProperProxy], otherwise, if the crelation is given (not an evar),
+  we fall back to [Proper]. *)
+Hint Extern 1 (ProperProxy _ _) => 
+  class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
+
+Hint Extern 2 (ProperProxy ?R _) => 
+  not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
+
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
+Delimit Scope signature_scope with signature.
+
+Module ProperNotations.
+
+  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+
+  Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+
+  Notation " R --> R' " := (@respectful _ _ (flip (R%signature)) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+
+End ProperNotations.
+
+Arguments Proper {A}%type R%signature m.
+Arguments respectful {A B}%type (R R')%signature _ _.
+
+Export ProperNotations.
+
+Local Open Scope signature_scope.
+
+(** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f]
+    by repeated introductions and setoid rewrites. It should work
+    fine when [f] is a combination of already known morphisms and
+    quantifiers. *)
+
+Ltac solve_respectful t :=
+ match goal with
+   | |- respectful _ _ _ _ =>
+     let H := fresh "H" in
+     intros ? ? H; solve_respectful ltac:(setoid_rewrite H; t)
+   | _ => t; reflexivity
+ end.
+
+Ltac solve_proper := unfold Proper; solve_respectful ltac:(idtac).
+
+(** [f_equiv] is a clone of [f_equal] that handles setoid equivalences.
+    For example, if we know that [f] is a morphism for [E1==>E2==>E],
+    then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv]
+    into the subgoals [E1 x x'] and [E2 y y'].
+*)
+
+Ltac f_equiv :=
+ match goal with
+  | |- ?R (?f ?x) (?f' _) =>
+    let T := type of x in
+    let Rx := fresh "R" in
+    evar (Rx : crelation T);
+    let H := fresh in
+    assert (H : (Rx==>R)%signature f f');
+    unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ]
+  | |- ?R ?f ?f' =>
+    solve [change (Proper R f); eauto with typeclass_instances | reflexivity ]
+  | _ => idtac
+ end.
+
+Section Relations.
+  Let U := Type.
+  Context {A B : U}. 
+
+  (** [forall_def] reifies the dependent product as a definition. *)
+  
+  Definition forall_def (P : A -> U) : Type := forall x : A, P x.
+  
+  (** Dependent pointwise lifting of a crelation on the range. *)
+  
+  Definition forall_relation (P : A -> U)
+             (sig : forall a, crelation (P a)) : crelation (forall x, P x) :=
+    fun f g => forall a, sig a (f a) (g a).
+
+  (** Non-dependent pointwise lifting *)
+  Definition pointwise_relation (R : crelation B) : crelation (A -> B) :=
+    fun f g => forall a, R (f a) (g a).
+
+  Lemma pointwise_pointwise (R : crelation B) :
+    relation_equivalence (pointwise_relation R) (@eq A ==> R).
+  Proof. intros. split. simpl_crelation. firstorder. Qed.
+  
+  (** Subcrelations induce a morphism on the identity. *)
+  
+  Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id.
+  Proof. firstorder. Qed.
+
+  (** The subrelation property goes through products as usual. *)
+  
+  Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') :
+    subrelation (RA ==> RB) (RA' ==> RB').
+  Proof. simpl_crelation. Qed.
+
+  (** And of course it is reflexive. *)
+  
+  Lemma subrelation_refl R : @subrelation A R R.
+  Proof. simpl_crelation. Qed.
+
+  (** [Proper] is itself a covariant morphism for [subrelation].
+   We use an unconvertible premise to avoid looping.
+   *)
+  
+  Lemma subrelation_proper `(mor : Proper A R' m) 
+        `(unc : Unconvertible (crelation A) R R')
+        `(sub : subrelation A R' R) : Proper R m.
+  Proof.
+    intros. apply sub. apply mor.
+  Qed.
+
+  Global Instance proper_subrelation_proper :
+    Proper (subrelation ++> eq ==> impl) (@Proper A).
+  Proof. reduce. subst. firstorder. Qed.
+
+  Global Instance proper_subrelation_proper_arrow :
+    Proper (subrelation ++> eq ==> arrow) (@Proper A).
+  Proof. reduce. subst. firstorder. Qed.
+
+  Global Instance pointwise_subrelation `(sub : subrelation B R R') :
+    subrelation (pointwise_relation R) (pointwise_relation R') | 4.
+  Proof. reduce. unfold pointwise_relation in *. apply sub. auto. Qed.
+  
+  (** For dependent function types. *)
+  Lemma forall_subrelation (P : A -> U) (R S : forall x : A, crelation (P x)) :
+    (forall a, subrelation (R a) (S a)) -> 
+    subrelation (forall_relation P R) (forall_relation P S).
+  Proof. reduce. firstorder. Qed.
+End Relations.
+
+Typeclasses Opaque respectful pointwise_relation forall_relation.
+Arguments forall_relation {A P}%type sig%signature _ _.
+Arguments pointwise_relation A%type {B}%type R%signature _ _.
+  
+Hint Unfold Reflexive : core.
+Hint Unfold Symmetric : core.
+Hint Unfold Transitive : core.
+
+(** Resolution with subrelation: favor decomposing products over applying reflexivity
+  for unconstrained goals. *)
+Ltac subrelation_tac T U :=
+  (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
+    class_apply @subrelation_respectful || class_apply @subrelation_refl.
+
+Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
+
+CoInductive apply_subrelation : Prop := do_subrelation.
+
+Ltac proper_subrelation :=
+  match goal with
+    [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
+  end.
+
+Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
+
+(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
+
+Instance iff_impl_subrelation : subrelation iff impl | 2.
+Proof. firstorder. Qed.
+
+Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2.
+Proof. firstorder. Qed.
+
+(** Essential subrelation instances for [iffT] and [arrow]. *)
+
+Instance iffT_arrow_subrelation : subrelation iffT arrow | 2.
+Proof. firstorder. Qed.
+
+Instance iffT_flip_arrow_subrelation : subrelation iffT (flip arrow) | 2.
+Proof. firstorder. Qed.
+
+(** We use an extern hint to help unification. *)
+
+Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
+  apply (@forall_subrelation A B R S) ; intro : typeclass_instances.
+
+Section GenericInstances.
+  (* Share universes *)
+  Let U := Type.
+  Context {A B C : U}.
+
+  (** We can build a PER on the Coq function space if we have PERs on the domain and
+   codomain. *)
+  
+  Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
+
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0).
+    transitivity y0... symmetry...
+    transitivity (y x0)...
+  Qed.
+
+  (** The complement of a crelation conserves its proper elements. *)
+  
+  Program Definition complement_proper
+          `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
+    Proper (RA ==> RA ==> iff) (complement R) := _.
+  
+  Next Obligation.
+  Proof.
+    unfold complement.
+    pose (mR x y X x0 y0 X0).
+    intuition.
+  Qed.
+ 
+  (** The [flip] too, actually the [flip] instance is a bit more general. *)
+
+  Program Definition flip_proper
+          `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
+    Proper (RB ==> RA ==> RC) (flip f) := _.
+  
+  Next Obligation.
+  Proof.
+    apply mor ; auto.
+  Qed.
+
+
+  (** Every Transitive crelation gives rise to a binary morphism on [impl],
+   contravariant in the first argument, covariant in the second. *)
+  
+  Global Program 
+  Instance trans_contra_co_morphism
+    `(Transitive A R) : Proper (R --> R ++> impl) R.
+  
+  Next Obligation.
+  Proof with auto.
+    transitivity x...
+    transitivity x0...
+  Qed.
+
+  Global Program 
+  Instance trans_contra_co_type_morphism
+    `(Transitive A R) : Proper (R --> R ++> arrow) R.
+  
+  Next Obligation.
+  Proof with auto.
+    transitivity x...
+    transitivity x0...
+  Qed.
+
+  (** Proper declarations for partial applications. *)
+
+  Global Program 
+  Instance trans_contra_inv_impl_morphism
+  `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+  Global Program 
+  Instance trans_contra_inv_impl_type_morphism
+  `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+  Global Program 
+  Instance trans_co_impl_morphism
+    `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0...
+  Qed.
+
+  Global Program 
+  Instance trans_co_impl_type_morphism
+    `(Transitive A R) : Proper (R ++> arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0...
+  Qed.
+
+  Global Program 
+  Instance trans_sym_co_inv_impl_morphism
+    `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y... symmetry...
+  Qed.
+
+  Global Program 
+  Instance trans_sym_co_inv_impl_type_morphism
+    `(PER A R) : Proper (R ++> flip arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y... symmetry...
+  Qed.
+
+  Global Program Instance trans_sym_contra_impl_morphism
+    `(PER A R) : Proper (R --> impl) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0... symmetry...
+  Qed.
+
+  Global Program Instance trans_sym_contra_arrow_morphism
+    `(PER A R) : Proper (R --> arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0... symmetry...
+  Qed.
+
+  Global Program Instance per_partial_app_morphism
+  `(PER A R) : Proper (R ==> iff) (R x) | 2.
+
+  Next Obligation.
+  Proof with auto.
+    split. intros ; transitivity x0...
+    intros.
+    transitivity y...
+    symmetry...
+  Qed.
+
+  Global Program Instance per_partial_app_type_morphism
+  `(PER A R) : Proper (R ==> iffT) (R x) | 2.
+
+  Next Obligation.
+  Proof with auto.
+    split. intros ; transitivity x0...
+    intros.
+    transitivity y...
+    symmetry...
+  Qed.
+
+  (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
+
+  Global Program 
+  Instance trans_co_eq_inv_impl_morphism
+  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+  Global Program 
+  Instance trans_co_eq_inv_arrow_morphism
+  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+  (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)
+
+  Global Program 
+  Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    transitivity x0... transitivity x... symmetry...
+
+    transitivity y... transitivity y0... symmetry...
+  Qed.
+
+  (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)
+
+  Global Program 
+  Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    transitivity x0... transitivity x... symmetry...
+
+    transitivity y... transitivity y0... symmetry...
+  Qed.
+
+  Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
+  Proof. firstorder. Qed.
+
+  Global Program Instance compose_proper RA RB RC :
+    Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C).
+
+  Next Obligation.
+  Proof.
+    simpl_crelation.
+    unfold compose. firstorder. 
+  Qed.
+
+  (** Coq functions are morphisms for Leibniz equality,
+     applied only if really needed. *)
+
+  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+    Reflexive (@Logic.eq A ==> R').
+  Proof. simpl_crelation. Qed.
+
+  (** [respectful] is a morphism for crelation equivalence. *)
+  
+  Global Instance respectful_morphism :
+    Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) 
+           (@respectful A B).
+  Proof. 
+    intros R R' HRR' S S' HSS' f g.
+    unfold respectful, relation_equivalence in * ; simpl in *.
+    split ; intros H x y Hxy.
+    setoid_rewrite <- HSS'. apply H. now rewrite HRR'.
+    rewrite HSS'. apply H. now rewrite <- HRR'.
+  Qed.
+
+  (** [R] is Reflexive, hence we can build the needed proof. *)
+
+  Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
+    Proper R' (m x).
+  Proof. simpl_crelation. Qed.
+  
+  Class Params (of : A) (arity : nat).
+    
+  Lemma flip_respectful (R : crelation A) (R' : crelation B) :
+    relation_equivalence (flip (R ==> R')) (flip R ==> flip R').
+  Proof.
+    intros.
+    unfold flip, respectful.
+    split ; intros ; intuition.
+  Qed.
+
+  
+  (** Treating flip: can't make them direct instances as we
+   need at least a [flip] present in the goal. *)
+  
+  Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R.
+  Proof. firstorder. Qed.
+  
+  Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')).
+  Proof. firstorder. Qed.
+  
+  (** That's if and only if *)
+  
+  Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
+  Proof. simpl_crelation. Qed.
+
+  (** Once we have normalized, we will apply this instance to simplify the problem. *)
+  
+  Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor.
+  
+  (** Every reflexive crelation gives rise to a morphism, 
+  only for immediately solving goals without variables. *)
+  
+  Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x.
+  Proof. firstorder. Qed.
+  
+  Lemma proper_eq (x : A) : Proper (@eq A) x.
+  Proof. intros. apply reflexive_proper. Qed.
+  
+End GenericInstances.
+
+Class PartialApplication.
+
+CoInductive normalization_done : Prop := did_normalization.
+
+Ltac partial_application_tactic :=
+  let rec do_partial_apps H m cont := 
+    match m with
+      | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
+        [(do_partial_apps H m' ltac:idtac)|clear H]
+      | _ => cont
+    end
+  in
+  let rec do_partial H ar m := 
+    match ar with
+      | 0%nat => do_partial_apps H m ltac:(fail 1)
+      | S ?n' =>
+        match m with
+          ?m' ?x => do_partial H n' m'
+        end
+    end
+  in
+  let params m sk fk :=
+    (let m' := fresh in head_of_constr m' m ;
+     let n := fresh in evar (n:nat) ;
+     let v := eval compute in n in clear n ;
+      let H := fresh in
+        assert(H:Params m' v) by typeclasses eauto ;
+          let v' := eval compute in v in subst m';
+            (sk H v' || fail 1))
+    || fk
+  in
+  let on_morphism m cont :=
+    params m ltac:(fun H n => do_partial H n m)
+      ltac:(cont)
+  in
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : @Params _ _ _ |- _ ] => fail 1
+    | [ |- @Proper ?T _ (?m ?x) ] =>
+      match goal with
+        | [ H : PartialApplication |- _ ] =>
+          class_apply @Reflexive_partial_app_morphism; [|clear H]
+        | _ => on_morphism (m x)
+          ltac:(class_apply @Reflexive_partial_app_morphism)
+      end
+  end.
+
+(** Bootstrap !!! *)
+
+Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
+Proof.
+  intros A R R' HRR' x y <-. red in HRR'.
+  split ; red ; intros. 
+  now setoid_rewrite <- HRR'.
+  now setoid_rewrite HRR'.
+Qed.
+
+Ltac proper_reflexive :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | _ => class_apply proper_eq || class_apply @reflexive_proper
+  end.
+
+
+Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
+
+Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper 
+  : typeclass_instances.
+Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
+  : typeclass_instances.
+Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
+  : typeclass_instances.
+Hint Extern 4 (@Proper _ _ _) => partial_application_tactic 
+  : typeclass_instances.
+Hint Extern 7 (@Proper _ _ _) => proper_reflexive 
+  : typeclass_instances.
+
+(** Special-purpose class to do normalization of signatures w.r.t. flip. *)
+
+Section Normalize.
+  Context (A : Type).
+
+  Class Normalizes (m : crelation A) (m' : crelation A) : Prop :=
+    normalizes : relation_equivalence m m'.
+  
+  (** Current strategy: add [flip] everywhere and reduce using [subrelation]
+   afterwards. *)
+
+  Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
+  Proof.
+    red in H, H0. red in H.
+    setoid_rewrite H.
+    assumption.
+  Qed.
+
+  Lemma flip_atom R : Normalizes R (flip (flip R)).
+  Proof.
+    firstorder.
+  Qed.
+
+End Normalize.
+
+Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) :
+  Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature).
+Proof. 
+  unfold Normalizes in *. intros.
+  rewrite NA, NB. firstorder. 
+Qed.
+
+Ltac normalizes :=
+  match goal with
+    | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow
+    | _ => class_apply @flip_atom
+  end.
+
+Ltac proper_normalization :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => 
+      let H := fresh "H" in
+      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
+  end.
+
+Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+Hint Extern 6 (@Proper _ _ _) => proper_normalization 
+  : typeclass_instances.
+
+(** When the crelation on the domain is symmetric, we can
+    flip the crelation on the codomain. Same for binary functions. *)
+
+Lemma proper_sym_flip :
+ forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f),
+ Proper (R1==>flip R2) f.
+Proof.
+intros A R1 Sym B R2 f Hf.
+intros x x' Hxx'. apply Hf, Sym, Hxx'.
+Qed.
+
+Lemma proper_sym_flip_2 :
+ forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f),
+ Proper (R1==>R2==>flip R3) f.
+Proof.
+intros A R1 Sym1 B R2 Sym2 C R3 f Hf.
+intros x x' Hxx' y y' Hyy'. apply Hf; auto.
+Qed.
+
+(** When the crelation on the domain is symmetric, a predicate is
+  compatible with [iff] as soon as it is compatible with [impl].
+  Same with a binary crelation. *)
+
+Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R==>impl) f),
+ Proper (R==>iff) f.
+Proof.
+intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto.
+Qed.
+
+Lemma proper_sym_arrow_iffT : forall `(Symmetric A R)`(Proper _ (R==>arrow) f),
+ Proper (R==>iffT) f.
+Proof.
+intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto.
+Qed.
+
+Lemma proper_sym_impl_iff_2 :
+ forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f),
+ Proper (R==>R'==>iff) f.
+Proof.
+intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'.
+repeat red in Hf. split; eauto.
+Qed.
+
+Lemma proper_sym_arrow_iffT_2 :
+ forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>arrow) f),
+ Proper (R==>R'==>iffT) f.
+Proof.
+intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'.
+repeat red in Hf. split; eauto.
+Qed.
+
+(** A [PartialOrder] is compatible with its underlying equivalence. *)
+Require Import Relation_Definitions.
+Instance PartialOrder_proper `(PartialOrder A eqA (R : relation A)) :
+  Proper (eqA==>eqA==>iff) R.
+Proof.
+intros.
+apply proper_sym_impl_iff_2; auto with *.
+intros x x' Hx y y' Hy Hr.
+transitivity x.
+generalize (partial_order_equivalence x x'); compute; intuition.
+transitivity y; auto.
+generalize (partial_order_equivalence y y'); compute; intuition.
+Qed.
+
+Instance PartialOrder_proper_type `(PartialOrder A eqA R) :
+  Proper (eqA==>eqA==>iffT) R.
+Proof.
+intros.
+apply proper_sym_arrow_iffT_2; auto with *.
+intros x x' Hx y y' Hy Hr.
+transitivity x.
+generalize (partial_order_equivalence x x'); compute; intuition.
+transitivity y; auto.
+generalize (partial_order_equivalence y y'); compute; intuition.
+Qed.
+
+(** From a [PartialOrder] to the corresponding [StrictOrder]:
+     [lt = le /\ ~eq].
+    If the order is total, we could also say [gt = ~le]. *)
+
+Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) :
+  StrictOrder (relation_conjunction R (complement eqA)).
+Proof.
+split; compute.
+intros x (_,Hx). apply Hx, Equivalence_Reflexive.
+intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
+apply PreOrder_Transitive with y; assumption.
+intro Hxz.
+apply Hxy'.
+apply partial_order_antisym; auto.
+rewrite Hxz. auto.
+Qed.
+
+(** From a [StrictOrder] to the corresponding [PartialOrder]:
+     [le = lt \/ eq].
+    If the order is total, we could also say [ge = ~lt]. *)
+
+Lemma StrictOrder_PreOrder
+ `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) :
+ PreOrder (relation_disjunction R eqA).
+Proof.
+split.
+intros x. right. reflexivity.
+intros x y z [Hxy|Hxy] [Hyz|Hyz].
+left. transitivity y; auto.
+left. rewrite <- Hyz; auto.
+left. rewrite Hxy; auto.
+right. transitivity y; auto.
+Qed.
+
+Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
+  class_apply StrictOrder_PreOrder : typeclass_instances.
+
+Lemma StrictOrder_PartialOrder
+  `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) :
+  PartialOrder eqA (relation_disjunction R eqA).
+Proof.
+intros. intros x y. compute. intuition.
+elim (StrictOrder_Irreflexive x).
+transitivity y; auto.
+Qed.
+
+Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => 
+  class_apply PartialOrder_StrictOrder : typeclass_instances.
+
+Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => 
+  class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
new file mode 100644
index 000000000..ca38ac5b4
--- /dev/null
+++ b/theories/Classes/CRelationClasses.v
@@ -0,0 +1,354 @@
+(* -*- coding: utf-8 -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Typeclass-based relations, tactics and standard instances
+
+   This is the basic theory needed to formalize morphisms and setoids.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+Require Export Coq.Classes.Init.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
+
+Set Universe Polymorphism.
+
+Definition crelation (A : Type) := A -> A -> Type.
+
+Definition iffT (A B : Type) := ((A -> B) * (B -> A))%type.
+
+(** We allow to unfold the [crelation] definition while doing morphism search. *)
+
+Section Defs.
+  Context {A : Type}.
+
+  (** We rebind crelational properties in separate classes to be able to overload each proof. *)
+
+  Class Reflexive (R : crelation A) :=
+    reflexivity : forall x : A, R x x.
+
+  Definition complement (R : crelation A) : crelation A := 
+    fun x y => R x y -> False.
+
+  (** Opaque for proof-search. *)
+  Typeclasses Opaque complement iffT.
+  
+  (** These are convertible. *)
+  Lemma complement_inverse R : complement (flip R) = flip (complement R).
+  Proof. reflexivity. Qed.
+
+  Class Irreflexive (R : crelation A) :=
+    irreflexivity : Reflexive (complement R).
+
+  Class Symmetric (R : crelation A) :=
+    symmetry : forall {x y}, R x y -> R y x.
+  
+  Class Asymmetric (R : crelation A) :=
+    asymmetry : forall {x y}, R x y -> (complement R y x : Type).
+  
+  Class Transitive (R : crelation A) :=
+    transitivity : forall {x y z}, R x y -> R y z -> R x z.
+
+  (** Various combinations of reflexivity, symmetry and transitivity. *)
+  
+  (** A [PreOrder] is both Reflexive and Transitive. *)
+  
+  Class PreOrder (R : crelation A)  := {
+    PreOrder_Reflexive :> Reflexive R | 2 ;
+    PreOrder_Transitive :> Transitive R | 2 }.
+
+  (** A [StrictOrder] is both Irreflexive and Transitive. *)
+
+  Class StrictOrder (R : crelation A)  := {
+    StrictOrder_Irreflexive :> Irreflexive R ;
+    StrictOrder_Transitive :> Transitive R }.
+
+  (** By definition, a strict order is also asymmetric *)
+  Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R.
+  Proof. firstorder. Qed.
+
+  (** A partial equivalence crelation is Symmetric and Transitive. *)
+  
+  Class PER (R : crelation A)  := {
+    PER_Symmetric :> Symmetric R | 3 ;
+    PER_Transitive :> Transitive R | 3 }.
+
+  (** Equivalence crelations. *)
+
+  Class Equivalence (R : crelation A)  := {
+    Equivalence_Reflexive :> Reflexive R ;
+    Equivalence_Symmetric :> Symmetric R ;
+    Equivalence_Transitive :> Transitive R }.
+
+  (** An Equivalence is a PER plus reflexivity. *)
+  
+  Global Instance Equivalence_PER {R} `(Equivalence R) : PER R | 10 :=
+    { PER_Symmetric := Equivalence_Symmetric ;
+      PER_Transitive := Equivalence_Transitive }.
+
+  (** We can now define antisymmetry w.r.t. an equivalence crelation on the carrier. *)
+  
+  Class Antisymmetric eqA `{equ : Equivalence eqA} (R : crelation A) :=
+    antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
+
+  Class subrelation (R R' : crelation A) :=
+    is_subrelation : forall {x y}, R x y -> R' x y.
+  
+  (** Any symmetric crelation is equal to its inverse. *)
+  
+  Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
+  Proof. hnf. intros x y H'. red in H'. apply symmetry. assumption. Qed.
+
+  Section flip.
+  
+    Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
+    Proof. tauto. Qed.
+    
+    Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
+      irreflexivity (R:=R).
+    
+    Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
+      fun x y H => symmetry (R:=R) H.
+    
+    Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
+      fun x y H H' => asymmetry (R:=R) H H'.
+    
+    Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
+      fun x y z H H' => transitivity (R:=R) H' H.
+
+    Program Definition flip_Antisymmetric `(Antisymmetric eqA R) :
+      Antisymmetric eqA (flip R).
+    Proof. firstorder. Qed.
+
+    (** Inversing the larger structures *)
+
+    Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_PER `(PER R) : PER (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R).
+    Proof. firstorder. Qed.
+
+  End flip.
+
+  Section complement.
+
+    Definition complement_Irreflexive `(Reflexive R)
+      : Irreflexive (complement R).
+    Proof. firstorder. Qed.
+
+    Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R).
+    Proof. firstorder. Qed.
+  End complement.
+
+
+  (** Rewrite crelation on a given support: declares a crelation as a rewrite
+   crelation for use by the generalized rewriting tactic.
+   It helps choosing if a rewrite should be handled
+   by the generalized or the regular rewriting tactic using leibniz equality.
+   Users can declare an [RewriteRelation A RA] anywhere to declare default
+   crelations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+  Class RewriteRelation (RA : crelation A).
+
+  (** Any [Equivalence] declared in the context is automatically considered
+   a rewrite crelation. *)
+    
+  Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA.
+
+  (** Leibniz equality. *)
+  Section Leibniz.
+    Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A.
+    Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A.
+    Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A.
+    
+    (** Leibinz equality [eq] is an equivalence crelation.
+        The instance has low priority as it is always applicable
+        if only the type is constrained. *)
+    
+    Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
+  End Leibniz.
+  
+End Defs.
+
+(** Default rewrite crelations handled by [setoid_rewrite]. *)
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
+
+(** Hints to drive the typeclass resolution avoiding loops
+ due to the use of full unification. *)
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
+
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
+
+Hint Extern 4 (subrelation (flip _) _) => 
+  class_apply @subrelation_symmetric : typeclass_instances.
+
+Hint Resolve irreflexivity : ord.
+
+Unset Implicit Arguments.
+
+(** A HintDb for crelations. *)
+
+Ltac solve_crelation :=
+  match goal with
+  | [ |- ?R ?x ?x ] => reflexivity
+  | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
+  end.
+
+Hint Extern 4 => solve_crelation : crelations.
+
+(** We can already dualize all these properties. *)
+
+(** * Standard instances. *)
+
+Ltac reduce_hyp H :=
+  match type of H with
+    | context [ _ <-> _ ] => fail 1
+    | _ => red in H ; try reduce_hyp H
+  end.
+
+Ltac reduce_goal :=
+  match goal with
+    | [ |- _ <-> _ ] => fail 1
+    | _ => red ; intros ; try reduce_goal
+  end.
+
+Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
+
+Ltac reduce := reduce_goal.
+
+Tactic Notation "apply" "*" constr(t) :=
+  first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
+    refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
+
+Ltac simpl_crelation :=
+  unfold flip, impl, arrow ; try reduce ; program_simpl ;
+    try ( solve [ dintuition ]).
+
+Local Obligation Tactic := simpl_crelation.
+
+(** Logical implication. *)
+
+Program Instance impl_Reflexive : Reflexive impl.
+Program Instance impl_Transitive : Transitive impl.
+
+(** Logical equivalence. *)
+
+Instance iff_Reflexive : Reflexive iff := iff_refl.
+Instance iff_Symmetric : Symmetric iff := iff_sym.
+Instance iff_Transitive : Transitive iff := iff_trans.
+
+(** Logical equivalence [iff] is an equivalence crelation. *)
+
+Program Instance iff_equivalence : Equivalence iff.
+
+Program Instance arrow_Reflexive : Reflexive arrow.
+Program Instance arrow_Transitive : Transitive arrow.
+
+Instance iffT_Reflexive : Reflexive iffT. 
+Proof. firstorder. Defined.
+Instance iffT_Symmetric : Symmetric iffT. 
+Proof. firstorder. Defined. 
+Instance iffT_Transitive : Transitive iffT.
+Proof. firstorder. Defined.
+
+(** We now develop a generalization of results on crelations for arbitrary predicates.
+   The resulting theory can be applied to homogeneous binary crelations but also to
+   arbitrary n-ary predicates. *)
+
+Local Open Scope list_scope.
+
+(** A compact representation of non-dependent arities, with the codomain singled-out. *)
+
+(** We define the various operations which define the algebra on binary crelations *)
+Section Binary.
+  Context {A : Type}.
+
+  Definition relation_equivalence : crelation (crelation A) :=
+    fun R R' => forall x y, iffT (R x y) (R' x y).
+
+  Global Instance: RewriteRelation relation_equivalence.
+  
+  Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A :=
+    fun x y => prod (R x y) (R' x y).
+
+  Definition relation_disjunction (R : crelation A) (R' : crelation A) : crelation A :=
+    fun x y => sum (R x y) (R' x y).
+  
+  (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+  
+  Set Automatic Introduction.
+  
+  Global Instance relation_equivalence_equivalence :
+    Equivalence relation_equivalence.
+  Proof. split; red; unfold relation_equivalence, iffT. firstorder. 
+    firstorder. 
+    intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
+  Qed.
+    
+  Global Instance relation_implication_preorder : PreOrder (@subrelation A).
+  Proof. firstorder. Qed.
+
+  (** *** Partial Order.
+   A partial order is a preorder which is additionally antisymmetric.
+   We give an equivalent definition, up-to an equivalence crelation
+   on the carrier. *)
+
+  Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+    partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
+  
+  (** The equivalence proof is sufficient for proving that [R] must be a
+   morphism for equivalence (see Morphisms).  It is also sufficient to
+   show that [R] is antisymmetric w.r.t. [eqA] *)
+
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Proof with auto.
+    reduce_goal.
+    apply H. firstorder.
+  Qed.
+
+  Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
+  Proof. firstorder. Qed.
+End Binary.
+
+Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
+
+(** The partial order defined by subrelation and crelation equivalence. *)
+
+Program Instance subrelation_partial_order :
+  ! PartialOrder (crelation A) relation_equivalence subrelation.
+
+Next Obligation.
+Proof.
+  unfold relation_equivalence in *. compute; firstorder.
+Qed.
+
+Typeclasses Opaque relation_equivalence.
+
+
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index 6e6ba68a2..3b4ba786a 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.v
@@ -44,7 +44,7 @@ Qed.
 (** The generic function that should be used to program, together with some
   useful tactics. *)
 
-Definition decide P {H : Decidable P} := @Decidable_witness P H.
+Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
 
 Ltac _decide_ P H :=
   let b := fresh "b" in
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 39d7cdaa0..dcaf057b0 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -56,6 +56,7 @@ Local Open Scope program_scope.
 Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := 
           swap_sumbool (x == y).
 
+
 (** Overloaded notation for inequality. *)
 
 Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 233e97c19..db04fbe39 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -24,7 +24,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Generalizable Variables A R eqA B S eqB.
-Local Obligation Tactic := simpl_relation.
+Local Obligation Tactic := try solve [simpl_relation].
 
 Local Open Scope signature_scope.
 
@@ -56,8 +56,8 @@ Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
 Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
 
   Next Obligation.
-  Proof.
-    transitivity y ; auto.
+  Proof. intros A R sa x y z Hxy Hyz.
+         now transitivity y.
   Qed.
 
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
@@ -116,8 +116,9 @@ Section Respecting.
   Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl.
 
   Next Obligation.
-  Proof.
-    unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
+  Proof. 
+    intros. intros f g h H H' x y Rxy.
+    unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
   Qed.
 
 End Respecting.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 617ff1906..921f21233 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -18,7 +18,7 @@ Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
-Generalizable All Variables.
+Generalizable Variables A eqA B C D R RA RB RC m f x y.
 Local Obligation Tactic := simpl_relation.
 
 (** * Morphisms.
@@ -29,15 +29,39 @@ Local Obligation Tactic := simpl_relation.
 (** A morphism for a relation [R] is a proper element of the relation.
    The relation [R] will be instantiated by [respectful] and [A] by an arrow
    type for usual morphisms. *)
-
-Class Proper {A} (R : relation A) (m : A) : Prop :=
-  proper_prf : R m m.
-
-(** Respectful morphisms. *)
-
-(** The fully dependent version, not used yet. *)
-
-Definition respectful_hetero
+Section Proper.
+  Let U := Type.
+  Context {A B : U}.
+
+  Class Proper (R : relation A) (m : A) : Prop :=
+    proper_prf : R m m.
+
+  (** Every element in the carrier of a reflexive relation is a morphism
+   for this relation.  We use a proxy class for this case which is used
+   internally to discharge reflexivity constraints.  The [Reflexive]
+   instance will almost always be used, but it won't apply in general to
+   any kind of [Proper (A -> B) _ _] goal, making proof-search much
+   slower. A cleaner solution would be to be able to set different
+   priorities in different hint bases and select a particular hint
+   database for resolution of a type class constraint. *)
+
+  Class ProperProxy (R : relation A) (m : A) : Prop :=
+    proper_proxy : R m m.
+
+  Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x.
+  Proof. firstorder. Qed.
+  
+  Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  (** Respectful morphisms. *)
+  
+  (** The fully dependent version, not used yet. *)
+  
+  Definition respectful_hetero
   (A B : Type)
   (C : A -> Type) (D : B -> Type)
   (R : A -> B -> Prop)
@@ -45,18 +69,24 @@ Definition respectful_hetero
     (forall x : A, C x) -> (forall x : B, D x) -> Prop :=
     fun f g => forall x y, R x y -> R' x y (f x) (g y).
 
-(** The non-dependent version is an instance where we forget dependencies. *)
+  (** The non-dependent version is an instance where we forget dependencies. *)
+  
+  Definition respectful (R : relation A) (R' : relation B) : relation (A -> B) :=
+    Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
 
-Definition respectful {A B : Type}
-  (R : relation A) (R' : relation B) : relation (A -> B) :=
-  Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
+End Proper.
 
-(** Notations reminiscent of the old syntax for declaring morphisms. *)
+(** We favor the use of Leibniz equality or a declared reflexive relation 
+  when resolving [ProperProxy], otherwise, if the relation is given (not an evar),
+  we fall back to [Proper]. *)
+Hint Extern 1 (ProperProxy _ _) => 
+  class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
 
-Delimit Scope signature_scope with signature.
+Hint Extern 2 (ProperProxy ?R _) => 
+  not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
 
-Arguments Proper {A}%type R%signature m.
-Arguments respectful {A B}%type (R R')%signature _ _.
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
+Delimit Scope signature_scope with signature.
 
 Module ProperNotations.
 
@@ -66,11 +96,14 @@ Module ProperNotations.
   Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
     (right associativity, at level 55) : signature_scope.
 
-  Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+  Notation " R --> R' " := (@respectful _ _ (flip (R%signature)) (R'%signature))
     (right associativity, at level 55) : signature_scope.
 
 End ProperNotations.
 
+Arguments Proper {A}%type R%signature m.
+Arguments respectful {A B}%type (R R')%signature _ _.
+
 Export ProperNotations.
 
 Local Open Scope signature_scope.
@@ -106,80 +139,89 @@ Ltac f_equiv :=
     assert (H : (Rx==>R)%signature f f');
     unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ]
   | |- ?R ?f ?f' =>
-    try reflexivity;
-    change (Proper R f); eauto with typeclass_instances; fail
+    solve [change (Proper R f); eauto with typeclass_instances | reflexivity ]
   | _ => idtac
  end.
 
-(** [forall_def] reifies the dependent product as a definition. *)
-
-Definition forall_def {A : Type} (B : A -> Type) : Type := forall x : A, B x.
-
-(** Dependent pointwise lifting of a relation on the range. *)
-
-Definition forall_relation {A : Type} {B : A -> Type}
- (sig : forall a, relation (B a)) : relation (forall x, B x) :=
- fun f g => forall a, sig a (f a) (g a).
-
-Arguments forall_relation {A B}%type sig%signature _ _.
-
-(** Non-dependent pointwise lifting *)
-
-Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) :=
-  Eval compute in forall_relation (B:=fun _ => B) (fun _ => R).
+Section Relations.
+  Let U := Type.
+  Context {A B : U} (P : A -> U).
+
+  (** [forall_def] reifies the dependent product as a definition. *)
+  
+  Definition forall_def : Type := forall x : A, P x.
+  
+  (** Dependent pointwise lifting of a relation on the range. *)
+  
+  Definition forall_relation 
+             (sig : forall a, relation (P a)) : relation (forall x, P x) :=
+    fun f g => forall a, sig a (f a) (g a).
+
+  (** Non-dependent pointwise lifting *)
+  Definition pointwise_relation (R : relation B) : relation (A -> B) :=
+    fun f g => forall a, R (f a) (g a).
+
+  Lemma pointwise_pointwise (R : relation B) :
+    relation_equivalence (pointwise_relation R) (@eq A ==> R).
+  Proof. intros. split; reduce; subst; firstorder. Qed.
+  
+  (** Subrelations induce a morphism on the identity. *)
+  
+  Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id.
+  Proof. firstorder. Qed.
+
+  (** The subrelation property goes through products as usual. *)
+  
+  Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') :
+    subrelation (RA ==> RB) (RA' ==> RB').
+  Proof. unfold subrelation in *; firstorder. Qed.
+
+  (** And of course it is reflexive. *)
+  
+  Lemma subrelation_refl R : @subrelation A R R.
+  Proof. unfold subrelation; firstorder. Qed.
+
+  (** [Proper] is itself a covariant morphism for [subrelation].
+   We use an unconvertible premise to avoid looping.
+   *)
+  
+  Lemma subrelation_proper `(mor : Proper A R' m) 
+        `(unc : Unconvertible (relation A) R R')
+        `(sub : subrelation A R' R) : Proper R m.
+  Proof.
+    intros. apply sub. apply mor.
+  Qed.
 
-Lemma pointwise_pointwise A B (R : relation B) :
-  relation_equivalence (pointwise_relation A R) (@eq A ==> R).
-Proof. intros. split. simpl_relation. firstorder. Qed.
+  Global Instance proper_subrelation_proper :
+    Proper (subrelation ++> eq ==> impl) (@Proper A).
+  Proof. reduce. subst. firstorder. Qed.
 
-(** We can build a PER on the Coq function space if we have PERs on the domain and
-   codomain. *)
+  Global Instance pointwise_subrelation `(sub : subrelation B R R') :
+    subrelation (pointwise_relation R) (pointwise_relation R') | 4.
+  Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
+  
+  (** For dependent function types. *)
+  Lemma forall_subrelation (R S : forall x : A, relation (P x)) :
+    (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S).
+  Proof. reduce. apply H. apply H0. Qed.
+End Relations.
 
+Typeclasses Opaque respectful pointwise_relation forall_relation.
+Arguments forall_relation {A P}%type sig%signature _ _.
+Arguments pointwise_relation A%type {B}%type R%signature _ _.
+  
 Hint Unfold Reflexive : core.
 Hint Unfold Symmetric : core.
 Hint Unfold Transitive : core.
 
-Typeclasses Opaque respectful pointwise_relation forall_relation.
-
-Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
-
-  Next Obligation.
-  Proof with auto.
-    assert(R x0 x0).
-    transitivity y0... symmetry...
-    transitivity (y x0)...
-  Qed.
-
-(** Subrelations induce a morphism on the identity. *)
-
-Instance subrelation_id_proper `(subrelation A R₁ R₂) : Proper (R₁ ==> R₂) id.
-Proof. firstorder. Qed.
-
-(** The subrelation property goes through products as usual. *)
-
-Lemma subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
-  subrelation (R₁ ==> S₁) (R₂ ==> S₂).
-Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
-
-(** And of course it is reflexive. *)
-
-Lemma subrelation_refl A R : @subrelation A R R.
-Proof. simpl_relation. Qed.
-
+(** Resolution with subrelation: favor decomposing products over applying reflexivity
+  for unconstrained goals. *)
 Ltac subrelation_tac T U :=
   (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
     class_apply @subrelation_respectful || class_apply @subrelation_refl.
 
 Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
 
-(** [Proper] is itself a covariant morphism for [subrelation]. *)
-
-Lemma subrelation_proper `(mor : Proper A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
-  sub : subrelation A R₁ R₂) : Proper R₂ m.
-Proof.
-  intros. apply sub. apply mor.
-Qed.
-
 CoInductive apply_subrelation : Prop := do_subrelation.
 
 Ltac proper_subrelation :=
@@ -189,117 +231,112 @@ Ltac proper_subrelation :=
 
 Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
 
-Instance proper_subrelation_proper :
-  Proper (subrelation ++> eq ==> impl) (@Proper A).
-Proof. reduce. subst. firstorder. Qed.
-
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
 Instance iff_impl_subrelation : subrelation iff impl | 2.
 Proof. firstorder. Qed.
 
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
+Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2.
 Proof. firstorder. Qed.
 
-Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
-  subrelation (pointwise_relation A R) (pointwise_relation A R') | 4.
-Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
-
-(** For dependent function types. *)
-Lemma forall_subrelation A (B : A -> Type) (R S : forall x : A, relation (B x)) :
-  (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S).
-Proof. reduce. apply H. apply H0. Qed.
-
 (** We use an extern hint to help unification. *)
 
 Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
   apply (@forall_subrelation A B R S) ; intro : typeclass_instances.
 
-(** Any symmetric relation is equal to its inverse. *)
+Section GenericInstances.
+  (* Share universes *)
+  Let U := Type.
+  Context {A B C : U}.
 
-Lemma subrelation_symmetric A R `(Symmetric A R) : subrelation (inverse R) R.
-Proof. reduce. red in H0. symmetry. assumption. Qed.
-
-Hint Extern 4 (subrelation (inverse _) _) => 
-  class_apply @subrelation_symmetric : typeclass_instances.
-
-(** The complement of a relation conserves its proper elements. *)
+  (** We can build a PER on the Coq function space if we have PERs on the domain and
+   codomain. *)
+  
+  Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
 
-Program Definition complement_proper
-  `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-  Proper (RA ==> RA ==> iff) (complement R) := _.
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0).
+    transitivity y0... symmetry...
+    transitivity (y x0)... 
+  Qed.
 
- Next Obligation.
+  (** The complement of a relation conserves its proper elements. *)
+  
+  Program Definition complement_proper
+          `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
+    Proper (RA ==> RA ==> iff) (complement R) := _.
+  
+  Next Obligation.
   Proof.
     unfold complement.
     pose (mR x y H x0 y0 H0).
     intuition.
   Qed.
  
-Hint Extern 1 (Proper _ (complement _)) => 
-  apply @complement_proper : typeclass_instances.
-
-(** The [inverse] too, actually the [flip] instance is a bit more general. *)
-
-Program Definition flip_proper
-  `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
-  Proper (RB ==> RA ==> RC) (flip f) := _.
+  (** The [flip] too, actually the [flip] instance is a bit more general. *)
 
+  Program Definition flip_proper
+          `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
+    Proper (RB ==> RA ==> RC) (flip f) := _.
+  
   Next Obligation.
   Proof.
     apply mor ; auto.
   Qed.
 
-Hint Extern 1 (Proper _ (flip _)) => 
-  apply @flip_proper : typeclass_instances.
 
-(** Every Transitive relation gives rise to a binary morphism on [impl],
+  (** Every Transitive relation gives rise to a binary morphism on [impl],
    contravariant in the first argument, covariant in the second. *)
-
-Program Instance trans_contra_co_morphism
-  `(Transitive A R) : Proper (R --> R ++> impl) R.
-
+  
+  Global Program 
+  Instance trans_contra_co_morphism
+    `(Transitive A R) : Proper (R --> R ++> impl) R.
+  
   Next Obligation.
   Proof with auto.
     transitivity x...
     transitivity x0...
   Qed.
 
-(** Proper declarations for partial applications. *)
+  (** Proper declarations for partial applications. *)
 
-Program Instance trans_contra_inv_impl_morphism
-  `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3.
+  Global Program 
+  Instance trans_contra_inv_impl_morphism
+  `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-Program Instance trans_co_impl_morphism
-  `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
+  Global Program 
+  Instance trans_co_impl_morphism
+    `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
   Qed.
 
-Program Instance trans_sym_co_inv_impl_morphism
-  `(PER A R) : Proper (R ++> inverse impl) (R x) | 3.
+  Global Program 
+  Instance trans_sym_co_inv_impl_morphism
+    `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity y... symmetry...
   Qed.
 
-Program Instance trans_sym_contra_impl_morphism
-  `(PER A R) : Proper (R --> impl) (R x) | 3.
+  Global Program Instance trans_sym_contra_impl_morphism
+    `(PER A R) : Proper (R --> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity x0... symmetry...
   Qed.
 
-Program Instance per_partial_app_morphism
+  Global Program Instance per_partial_app_morphism
   `(PER A R) : Proper (R ==> iff) (R x) | 2.
 
   Next Obligation.
@@ -310,20 +347,21 @@ Program Instance per_partial_app_morphism
     symmetry...
   Qed.
 
-(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
-   to get an [R y z] goal. *)
+  (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
 
-Program Instance trans_co_eq_inv_impl_morphism
-  `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2.
+  Global Program 
+  Instance trans_co_eq_inv_impl_morphism
+  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
+  (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
+  Global Program 
+  Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
@@ -333,11 +371,11 @@ Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
     transitivity y... transitivity y0... symmetry...
   Qed.
 
-Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
-Proof. firstorder. Qed.
+  Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
+  Proof. firstorder. Qed.
 
-Program Instance compose_proper A B C R₀ R₁ R₂ :
-  Proper ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
+  Global Program Instance compose_proper RA RB RC :
+    Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C).
 
   Next Obligation.
   Proof.
@@ -345,63 +383,79 @@ Program Instance compose_proper A B C R₀ R₁ R₂ :
     unfold compose. apply H. apply H0. apply H1.
   Qed.
 
-(** Coq functions are morphisms for Leibniz equality,
-   applied only if really needed. *)
+  (** Coq functions are morphisms for Leibniz equality,
+     applied only if really needed. *)
 
-Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
-  Reflexive (@Logic.eq A ==> R').
-Proof. simpl_relation. Qed.
-
-(** [respectful] is a morphism for relation equivalence. *)
-
-Instance respectful_morphism :
-  Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
-Proof.
-  reduce.
-  unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
-  split ; intros.
+  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+    Reflexive (@Logic.eq A ==> R').
+  Proof. simpl_relation. Qed.
 
+  (** [respectful] is a morphism for relation equivalence. *)
+  
+  Global Instance respectful_morphism :
+    Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) 
+           (@respectful A B).
+  Proof.
+    reduce.
+    unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
+    split ; intros.
+    
     rewrite <- H0.
     apply H1.
     rewrite H.
     assumption.
-
+    
     rewrite H0.
     apply H1.
     rewrite <- H.
     assumption.
-Qed.
-
-(** Every element in the carrier of a reflexive relation is a morphism for this relation.
-   We use a proxy class for this case which is used internally to discharge reflexivity constraints.
-   The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of
-   [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
-   to set different priorities in different hint bases and select a particular hint database for
-   resolution of a type class constraint.*)
-
-Class ProperProxy {A} (R : relation A) (m : A) : Prop :=
-  proper_proxy : R m m.
-
-Lemma eq_proper_proxy A (x : A) : ProperProxy (@eq A) x.
-Proof. firstorder. Qed.
-
-Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x.
-Proof. firstorder. Qed.
-
-Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x.
-Proof. firstorder. Qed.
-
-Hint Extern 1 (ProperProxy _ _) => 
-  class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
-Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
+  Qed.
 
-(** [R] is Reflexive, hence we can build the needed proof. *)
+  (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
-   Proper R' (m x).
-Proof. simpl_relation. Qed.
+  Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
+    Proper R' (m x).
+  Proof. simpl_relation. Qed.
+  
+  Class Params (of : A) (arity : nat).
+    
+  Lemma flip_respectful (R : relation A) (R' : relation B) :
+    relation_equivalence (flip (R ==> R')) (flip R ==> flip R').
+  Proof.
+    intros.
+    unfold flip, respectful.
+    split ; intros ; intuition.
+  Qed.
 
-Class Params {A : Type} (of : A) (arity : nat).
+  
+  (** Treating flip: can't make them direct instances as we
+   need at least a [flip] present in the goal. *)
+  
+  Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R.
+  Proof. firstorder. Qed.
+  
+  Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')).
+  Proof. firstorder. Qed.
+  
+  (** That's if and only if *)
+  
+  Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
+  Proof. simpl_relation. Qed.
+
+  (** Once we have normalized, we will apply this instance to simplify the problem. *)
+  
+  Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor.
+  
+  (** Every reflexive relation gives rise to a morphism, 
+  only for immediately solving goals without variables. *)
+  
+  Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x.
+  Proof. firstorder. Qed.
+  
+  Lemma proper_eq (x : A) : Proper (@eq A) x.
+  Proof. intros. apply reflexive_proper. Qed.
+  
+End GenericInstances.
 
 Class PartialApplication.
 
@@ -450,68 +504,6 @@ Ltac partial_application_tactic :=
       end
   end.
 
-Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances.
-
-Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
-  relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
-Proof.
-  intros.
-  unfold flip, respectful.
-  split ; intros ; intuition.
-Qed.
-
-(** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
-
-Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop :=
-  normalizes : relation_equivalence m m'.
-
-(** Current strategy: add [inverse] everywhere and reduce using [subrelation]
-   afterwards. *)
-
-Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)).
-Proof.
-  firstorder.
-Qed.
-
-Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
-  Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
-Proof. unfold Normalizes in *. intros. 
-  rewrite NA, NB. firstorder.
-Qed.
-
-Ltac inverse :=
-  match goal with
-    | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @inverse_arrow
-    | _ => class_apply @inverse_atom
-  end.
-
-Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.
-
-(** Treating inverse: can't make them direct instances as we
-   need at least a [flip] present in the goal. *)
-
-Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.
-Proof. firstorder. Qed.
-
-Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
-Proof. firstorder. Qed.
-
-Hint Extern 1 (subrelation (flip _) _) => class_apply @inverse1 : typeclass_instances.
-Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_instances.
-
-(** That's if and only if *)
-
-Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
-Proof. simpl_relation. Qed.
-
-(* Hint Extern 3 (subrelation eq ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *)
-
-(** Once we have normalized, we will apply this instance to simplify the problem. *)
-
-Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor.
-
-Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances.
-
 (** Bootstrap !!! *)
 
 Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
@@ -525,46 +517,83 @@ Proof.
   apply H0.
 Qed.
 
-Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m.
-Proof.
-  red in H, H0.
-  setoid_rewrite H.
-  assumption.
-Qed.
-
-Ltac proper_normalization :=
+Ltac proper_reflexive :=
   match goal with
     | [ _ : normalization_done |- _ ] => fail 1
-    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in
-      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
+    | _ => class_apply proper_eq || class_apply @reflexive_proper
   end.
 
-Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances.
 
-(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
+Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
 
-Lemma reflexive_proper `{Reflexive A R} (x : A)
-   : Proper R x.
-Proof. firstorder. Qed.
+Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper 
+  : typeclass_instances.
+Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
+  : typeclass_instances.
+Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
+  : typeclass_instances.
+Hint Extern 4 (@Proper _ _ _) => partial_application_tactic 
+  : typeclass_instances.
+Hint Extern 7 (@Proper _ _ _) => proper_reflexive 
+  : typeclass_instances.
 
-Lemma proper_eq A (x : A) : Proper (@eq A) x.
-Proof. intros. apply reflexive_proper. Qed.
+(** Special-purpose class to do normalization of signatures w.r.t. flip. *)
 
-Ltac proper_reflexive :=
+Section Normalize.
+  Context (A : Type).
+
+  Class Normalizes (m : relation A) (m' : relation A) : Prop :=
+    normalizes : relation_equivalence m m'.
+  
+  (** Current strategy: add [flip] everywhere and reduce using [subrelation]
+   afterwards. *)
+
+  Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
+  Proof.
+    red in H, H0.
+    rewrite H.
+    assumption.
+  Qed.
+
+  Lemma flip_atom R : Normalizes R (flip (flip R)).
+  Proof.
+    firstorder.
+  Qed.
+
+End Normalize.
+
+Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) :
+  Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature).
+Proof. 
+  unfold Normalizes in *. intros.
+  rewrite NA, NB. firstorder. 
+Qed.
+
+Ltac normalizes :=
   match goal with
-    | [ _ : normalization_done |- _ ] => fail 1
-    | _ => class_apply proper_eq || class_apply @reflexive_proper
+    | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow
+    | _ => class_apply @flip_atom
   end.
 
-Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.
+Ltac proper_normalization :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => 
+      let H := fresh "H" in
+      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
+  end.
 
+Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+Hint Extern 6 (@Proper _ _ _) => proper_normalization 
+  : typeclass_instances.
 
 (** When the relation on the domain is symmetric, we can
-    inverse the relation on the codomain. Same for binary functions. *)
+    flip the relation on the codomain. Same for binary functions. *)
 
 Lemma proper_sym_flip :
  forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f),
- Proper (R1==>inverse R2) f.
+ Proper (R1==>flip R2) f.
 Proof.
 intros A R1 Sym B R2 f Hf.
 intros x x' Hxx'. apply Hf, Sym, Hxx'.
@@ -572,7 +601,7 @@ Qed.
 
 Lemma proper_sym_flip_2 :
  forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f),
- Proper (R1==>R2==>inverse R3) f.
+ Proper (R1==>R2==>flip R3) f.
 Proof.
 intros A R1 Sym1 B R2 Sym2 C R3 f Hf.
 intros x x' Hxx' y y' Hyy'. apply Hf; auto.
@@ -627,8 +656,6 @@ apply partial_order_antisym; auto.
 rewrite Hxz; auto.
 Qed.
 
-Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => 
-  class_apply PartialOrder_StrictOrder : typeclass_instances.
 
 (** From a [StrictOrder] to the corresponding [PartialOrder]:
      [le = lt \/ eq].
@@ -659,5 +686,8 @@ elim (StrictOrder_Irreflexive x).
 transitivity y; auto.
 Qed.
 
+Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => 
+  class_apply PartialOrder_StrictOrder : typeclass_instances.
+
 Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => 
   class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 6f02ac9f5..4f80a67ae 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -16,7 +16,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
-Local Obligation Tactic := simpl_relation.
+Local Obligation Tactic := try solve [simpl_relation | firstorder auto].
 
 (** Standard instances for [not], [iff] and [impl]. *)
 
@@ -52,49 +52,20 @@ Program Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl.
 
 Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A).
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.
-    split ; intros.
-    destruct H0 as [x1 H1].
-    exists x1. rewrite H in H1. assumption.
-
-    destruct H0 as [x1 H1].
-    exists x1. rewrite H. assumption.
-  Qed.
-
 Program Instance ex_impl_morphism {A : Type} :
   Proper (pointwise_relation A impl ==> impl) (@ex A) | 1.
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.
-    exists H0. apply H. assumption.
-  Qed.
-
-Program Instance ex_inverse_impl_morphism {A : Type} :
-  Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1.
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.
-    exists H0. apply H. assumption.
-  Qed.
+Program Instance ex_flip_impl_morphism {A : Type} :
+  Proper (pointwise_relation A (flip impl) ==> flip impl) (@ex A) | 1.
 
 Program Instance all_iff_morphism {A : Type} :
   Proper (pointwise_relation A iff ==> iff) (@all A).
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
 Program Instance all_impl_morphism {A : Type} :
   Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
 
-Program Instance all_inverse_impl_morphism {A : Type} :
-  Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
+Program Instance all_flip_impl_morphism {A : Type} :
+  Proper (pointwise_relation A (flip impl) ==> flip impl) (@all A) | 1.
 
 (** Equivalent points are simultaneously accessible or not *)
 
@@ -104,13 +75,13 @@ Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop)
 Proof.
  apply proper_sym_impl_iff; auto with *.
  intros x y EQ WF. apply Acc_intro; intros z Hz.
- rewrite <- EQ in Hz. now apply Acc_inv with x.
+rewrite <- EQ in Hz. now apply Acc_inv with x.
 Qed.
 
 (** Equivalent relations have the same accessible points *)
 
 Instance Acc_rel_morphism {A:Type} :
- Proper (@relation_equivalence A ==> Logic.eq ==> iff) (@Acc A).
+ Proper (relation_equivalence ==> Logic.eq ==> iff) (@Acc A).
 Proof.
  apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry.
  intros R R' EQ a a' Ha WF. subst a'.
@@ -121,7 +92,7 @@ Qed.
 (** Equivalent relations are simultaneously well-founded or not *)
 
 Instance well_founded_morphism {A : Type} :
- Proper (@relation_equivalence A ==> iff) (@well_founded A).
+ Proper (relation_equivalence ==> iff) (@well_founded A).
 Proof.
  unfold well_founded. solve_proper.
 Qed.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index ea2afb306..dc46b4bbb 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -30,8 +30,6 @@ Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
 
 (* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *)
 
-Require Import List.
-
 Lemma predicate_equivalence_pointwise (l : Tlist) :
   Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id.
 Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
@@ -52,6 +50,6 @@ Instance subrelation_pointwise :
 Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed.
 
 
-Lemma inverse_pointwise_relation A (R : relation A) :
-  relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)).
+Lemma flip_pointwise_relation A (R : relation A) :
+  relation_equivalence (pointwise_relation A (flip R)) (flip (pointwise_relation A R)).
 Proof. intros. split; firstorder. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b8fdac8c9..61edb2b98 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -20,41 +20,187 @@ Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 
-(** We allow to unfold the [relation] definition while doing morphism search. *)
-
-Notation inverse R := (flip (R:relation _) : relation _).
-
-Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
-
-(** Opaque for proof-search. *)
-Typeclasses Opaque complement.
-
-(** These are convertible. *)
-
-Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
-Proof. reflexivity. Qed.
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
 
-(** We rebind relations in separate classes to be able to overload each proof. *)
+(** We allow to unfold the [relation] definition while doing morphism search. *)
 
-Set Implicit Arguments.
-Unset Strict Implicit.
+Section Defs.
+  Context {A : Type}.
+
+  (** We rebind relational properties in separate classes to be able to overload each proof. *)
+
+  Class Reflexive (R : relation A) :=
+    reflexivity : forall x : A, R x x.
+
+  Definition complement (R : relation A) : relation A := fun x y => R x y -> False.
+
+  (** Opaque for proof-search. *)
+  Typeclasses Opaque complement.
+  
+  (** These are convertible. *)
+  Lemma complement_inverse R : complement (flip R) = flip (complement R).
+  Proof. reflexivity. Qed.
+
+  Class Irreflexive (R : relation A) :=
+    irreflexivity : Reflexive (complement R).
+
+  Class Symmetric (R : relation A) :=
+    symmetry : forall {x y}, R x y -> R y x.
+  
+  Class Asymmetric (R : relation A) :=
+    asymmetry : forall {x y}, R x y -> R y x -> False.
+  
+  Class Transitive (R : relation A) :=
+    transitivity : forall {x y z}, R x y -> R y z -> R x z.
+
+  (** Various combinations of reflexivity, symmetry and transitivity. *)
+  
+  (** A [PreOrder] is both Reflexive and Transitive. *)
+  
+  Class PreOrder (R : relation A) : Prop := {
+    PreOrder_Reflexive :> Reflexive R | 2 ;
+    PreOrder_Transitive :> Transitive R | 2 }.
+
+  (** A [StrictOrder] is both Irreflexive and Transitive. *)
+
+  Class StrictOrder (R : relation A) : Prop := {
+    StrictOrder_Irreflexive :> Irreflexive R ;
+    StrictOrder_Transitive :> Transitive R }.
+
+  (** By definition, a strict order is also asymmetric *)
+  Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R.
+  Proof. firstorder. Qed.
+
+  (** A partial equivalence relation is Symmetric and Transitive. *)
+  
+  Class PER (R : relation A) : Prop := {
+    PER_Symmetric :> Symmetric R | 3 ;
+    PER_Transitive :> Transitive R | 3 }.
+
+  (** Equivalence relations. *)
+
+  Class Equivalence (R : relation A) : Prop := {
+    Equivalence_Reflexive :> Reflexive R ;
+    Equivalence_Symmetric :> Symmetric R ;
+    Equivalence_Transitive :> Transitive R }.
+
+  (** An Equivalence is a PER plus reflexivity. *)
+  
+  Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 :=
+    { }. 
+
+  (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
+  
+  Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) :=
+    antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
+
+  Class subrelation (R R' : relation A) : Prop :=
+    is_subrelation : forall {x y}, R x y -> R' x y.
+  
+  (** Any symmetric relation is equal to its inverse. *)
+  
+  Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
+  Proof. hnf. intros. red in H0. apply symmetry. assumption. Qed.
+
+  Section flip.
+  
+    Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
+    Proof. tauto. Qed.
+    
+    Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
+      irreflexivity (R:=R).
+    
+    Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
+      fun x y H => symmetry (R:=R) H.
+    
+    Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
+      fun x y H H' => asymmetry (R:=R) H H'.
+    
+    Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
+      fun x y z H H' => transitivity (R:=R) H' H.
+
+    Program Definition flip_Antisymmetric `(Antisymmetric eqA R) :
+      Antisymmetric eqA (flip R).
+    Proof. firstorder. Qed.
+
+    (** Inversing the larger structures *)
+
+    Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_PER `(PER R) : PER (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R).
+    Proof. firstorder. Qed.
+
+  End flip.
+
+  Section complement.
+
+    Definition complement_Irreflexive `(Reflexive R)
+      : Irreflexive (complement R).
+    Proof. firstorder. Qed.
+
+    Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R).
+    Proof. firstorder. Qed.
+  End complement.
+
+
+  (** Rewrite relation on a given support: declares a relation as a rewrite
+   relation for use by the generalized rewriting tactic.
+   It helps choosing if a rewrite should be handled
+   by the generalized or the regular rewriting tactic using leibniz equality.
+   Users can declare an [RewriteRelation A RA] anywhere to declare default
+   relations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
 
-Class Reflexive {A} (R : relation A) :=
-  reflexivity : forall x, R x x.
+  Class RewriteRelation (RA : relation A).
 
-Class Irreflexive {A} (R : relation A) :=
-  irreflexivity : Reflexive (complement R).
+  (** Any [Equivalence] declared in the context is automatically considered
+   a rewrite relation. *)
+    
+  Global Instance equivalence_rewrite_relation `(Equivalence eqA) : RewriteRelation eqA.
+
+  (** Leibniz equality. *)
+  Section Leibniz.
+    Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A.
+    Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A.
+    Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A.
+    
+    (** Leibinz equality [eq] is an equivalence relation.
+        The instance has low priority as it is always applicable
+        if only the type is constrained. *)
+    
+    Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
+  End Leibniz.
+  
+End Defs.
+
+(** Default rewrite relations handled by [setoid_rewrite]. *)
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
 
+(** Hints to drive the typeclass resolution avoiding loops
+ due to the use of full unification. *)
 Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
 
-Class Symmetric {A} (R : relation A) :=
-  symmetry : forall x y, R x y -> R y x.
-
-Class Asymmetric {A} (R : relation A) :=
-  asymmetry : forall x y, R x y -> R y x -> False.
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
 
-Class Transitive {A} (R : relation A) :=
-  transitivity : forall x y z, R x y -> R y z -> R x z.
+Hint Extern 4 (subrelation (flip _) _) => 
+  class_apply @subrelation_symmetric : typeclass_instances.
 
 Hint Resolve irreflexivity : ord.
 
@@ -72,40 +218,6 @@ Hint Extern 4 => solve_relation : relations.
 
 (** We can already dualize all these properties. *)
 
-Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
-
-Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R).
-Proof. tauto. Qed.
-
-Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
-
-Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
-  irreflexivity (R:=R).
-
-Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) :=
-  fun x y H => symmetry (R:=R) H.
-
-Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) :=
-  fun x y H H' => asymmetry (R:=R) H H'.
-
-Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) :=
-  fun x y z H H' => transitivity (R:=R) H' H.
-
-Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
-Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
-Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
-Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
-
-Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
-   : Irreflexive (complement R).
-Proof. firstorder. Qed.
-
-Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
-Proof. firstorder. Qed.
-
-Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
-Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances.
-
 (** * Standard instances. *)
 
 Ltac reduce_hyp H :=
@@ -145,54 +257,6 @@ Instance iff_Reflexive : Reflexive iff := iff_refl.
 Instance iff_Symmetric : Symmetric iff := iff_sym.
 Instance iff_Transitive : Transitive iff := iff_trans.
 
-(** Leibniz equality. *)
-
-Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A.
-Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A.
-Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A.
-
-(** Various combinations of reflexivity, symmetry and transitivity. *)
-
-(** A [PreOrder] is both Reflexive and Transitive. *)
-
-Class PreOrder {A} (R : relation A) : Prop := {
-  PreOrder_Reflexive :> Reflexive R | 2 ;
-  PreOrder_Transitive :> Transitive R | 2 }.
-
-(** A partial equivalence relation is Symmetric and Transitive. *)
-
-Class PER {A} (R : relation A) : Prop := {
-  PER_Symmetric :> Symmetric R | 3 ;
-  PER_Transitive :> Transitive R | 3 }.
-
-(** Equivalence relations. *)
-
-Class Equivalence {A} (R : relation A) : Prop := {
-  Equivalence_Reflexive :> Reflexive R ;
-  Equivalence_Symmetric :> Symmetric R ;
-  Equivalence_Transitive :> Transitive R }.
-
-(** An Equivalence is a PER plus reflexivity. *)
-
-Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
-  { PER_Symmetric := Equivalence_Symmetric ;
-    PER_Transitive := Equivalence_Transitive }.
-
-(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
-
-Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
-  antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
-
-Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) :
-  Antisymmetric A eqA (flip R).
-Proof. firstorder. Qed.
-
-(** Leibinz equality [eq] is an equivalence relation.
-   The instance has low priority as it is always applicable
-   if only the type is constrained. *)
-
-Program Instance eq_equivalence : Equivalence (@eq A) | 10.
-
 (** Logical equivalence [iff] is an equivalence relation. *)
 
 Program Instance iff_equivalence : Equivalence iff.
@@ -203,9 +267,6 @@ Program Instance iff_equivalence : Equivalence iff.
 
 Local Open Scope list_scope.
 
-(* Notation " [ ] " := nil : list_scope. *)
-(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
-
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
 (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *)
@@ -346,106 +407,66 @@ Program Instance predicate_implication_preorder :
 (** We define the various operations which define the algebra on binary relations,
    from the general ones. *)
 
-Definition relation_equivalence {A : Type} : relation (relation A) :=
-  @predicate_equivalence (_::_::Tnil).
-
-Class subrelation {A:Type} (R R' : relation A) : Prop :=
-  is_subrelation : @predicate_implication (A::A::Tnil) R R'.
-
-Arguments subrelation {A} R R'.
-
-Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_intersection (A::A::Tnil) R R'.
-
-Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_union (A::A::Tnil) R R'.
-
-(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
-
-Set Automatic Introduction.
-
-Instance relation_equivalence_equivalence (A : Type) :
-  Equivalence (@relation_equivalence A).
-Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
-
-Instance relation_implication_preorder A : PreOrder (@subrelation A).
-Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed.
-
-(** *** Partial Order.
+Section Binary.
+  Context {A : Type}.
+
+  Definition relation_equivalence : relation (relation A) :=
+    @predicate_equivalence (_::_::Tnil).
+
+  Global Instance: RewriteRelation relation_equivalence.
+  
+  Definition relation_conjunction (R : relation A) (R' : relation A) : relation A :=
+    @predicate_intersection (A::A::Tnil) R R'.
+
+  Definition relation_disjunction (R : relation A) (R' : relation A) : relation A :=
+    @predicate_union (A::A::Tnil) R R'.
+  
+  (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+  
+  Set Automatic Introduction.
+  
+  Global Instance relation_equivalence_equivalence :
+    Equivalence relation_equivalence.
+  Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
+  
+  Global Instance relation_implication_preorder : PreOrder (@subrelation A).
+  Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed.
+
+  (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
    We give an equivalent definition, up-to an equivalence relation
    on the carrier. *)
 
-Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
-  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
+  Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+    partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
+  
+  (** The equivalence proof is sufficient for proving that [R] must be a
+   morphism for equivalence (see Morphisms).  It is also sufficient to
+   show that [R] is antisymmetric w.r.t. [eqA] *)
+
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Proof with auto.
+    reduce_goal.
+    pose proof partial_order_equivalence as poe. do 3 red in poe.
+    apply <- poe. firstorder.
+  Qed.
 
-(** The equivalence proof is sufficient for proving that [R] must be a morphism
-   for equivalence (see Morphisms).
-   It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
 
-Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
-Proof with auto.
-  reduce_goal.
-  pose proof partial_order_equivalence as poe. do 3 red in poe.
-  apply <- poe. firstorder.
-Qed.
+  Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
+  Proof. firstorder. Qed.
+End Binary.
+
+Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
 
 (** The partial order defined by subrelation and relation equivalence. *)
 
 Program Instance subrelation_partial_order :
   ! PartialOrder (relation A) relation_equivalence subrelation.
 
-  Next Obligation.
-  Proof.
-    unfold relation_equivalence in *. compute; firstorder.
-  Qed.
+Next Obligation.
+Proof.
+  unfold relation_equivalence in *. compute; firstorder.
+Qed.
 
 Typeclasses Opaque arrows predicate_implication predicate_equivalence
-  relation_equivalence pointwise_lifting.
-
-(** Rewrite relation on a given support: declares a relation as a rewrite
-   relation for use by the generalized rewriting tactic.
-   It helps choosing if a rewrite should be handled
-   by the generalized or the regular rewriting tactic using leibniz equality.
-   Users can declare an [RewriteRelation A RA] anywhere to declare default
-   relations. This is also done automatically by the [Declare Relation A RA]
-   commands. *)
-
-Class RewriteRelation {A : Type} (RA : relation A).
-
-Instance: RewriteRelation impl.
-Instance: RewriteRelation iff.
-Instance: RewriteRelation (@relation_equivalence A).
-
-(** Any [Equivalence] declared in the context is automatically considered
-   a rewrite relation. *)
-
-Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
-
-(** Strict Order *)
-
-Class StrictOrder {A : Type} (R : relation A) : Prop := {
-  StrictOrder_Irreflexive :> Irreflexive R ;
-  StrictOrder_Transitive :> Transitive R
-}.
-
-Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R.
-Proof. firstorder. Qed.
-
-(** Inversing a [StrictOrder] gives another [StrictOrder] *)
-
-Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R).
-Proof. firstorder. Qed.
-
-(** Same for [PartialOrder]. *)
-
-Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R).
-Proof. firstorder. Qed.
-
-Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances.
-Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances.
-
-Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R).
-Proof. firstorder. Qed.
-
-Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances.
+            relation_equivalence pointwise_lifting.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 2b010206c..73be830a4 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -9,8 +9,8 @@
 (** * Relations over pairs *)
 
 
+Require Import SetoidList.
 Require Import Relations Morphisms.
-
 (* NB: This should be system-wide someday, but for that we need to
     fix the simpl tactic, since "simpl fst" would be refused for
     the moment.
@@ -40,7 +40,7 @@ Generalizable Variables A B RA RB Ri Ro f.
 (** Any function from [A] to [B] allow to obtain a relation over [A]
     out of a relation over [B]. *)
 
-Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A :=
+Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A :=
  fun a a' => R (f a) (f a').
 
 Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
@@ -62,13 +62,13 @@ Instance snd_measure : @Measure (A * B) B Snd.
 (** We define a product relation over [A*B]: each components should
     satisfy the corresponding initial relation. *)
 
-Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) :=
- relation_conjunction (RA @@1) (RB @@2).
+Polymorphic Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) :=
+ relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2).
 
 Infix "*" := RelProd : signature_scope.
 
 Section RelCompFun_Instances.
-  Context {A B : Type} (R : relation B).
+  Context {A : Type} {B : Type} (R : relation B).
 
   Global Instance RelCompFun_Reflexive
     `(Measure A B f, Reflexive _ R) : Reflexive (R@@f).
@@ -94,57 +94,61 @@ Section RelCompFun_Instances.
 
 End RelCompFun_Instances.
 
-Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B)
- `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).
-Proof. firstorder. Qed.
-
-Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B)
- `(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA*RB).
-Proof. firstorder. Qed.
-
-Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B)
- `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
-Proof. firstorder. Qed.
-
-Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B)
- `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
-
-Lemma FstRel_ProdRel {A B}(RA:relation A) :
- relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)).
-Proof. firstorder. Qed.
-
-Lemma SndRel_ProdRel {A B}(RB:relation B) :
- relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB).
-Proof. firstorder. Qed.
-
-Instance FstRel_sub {A B} (RA:relation A)(RB:relation B):
- subrelation (RA*RB) (RA @@1).
-Proof. firstorder. Qed.
-
-Instance SndRel_sub {A B} (RA:relation A)(RB:relation B):
- subrelation (RA*RB) (RB @@2).
-Proof. firstorder. Qed.
-
-Instance pair_compat { A B } (RA:relation A)(RB:relation B) :
- Proper (RA==>RB==> RA*RB) (@pair _ _).
-Proof. firstorder. Qed.
-
-Instance fst_compat { A B } (RA:relation A)(RB:relation B) :
- Proper (RA*RB ==> RA) Fst.
-Proof.
-intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
-Qed.
-
-Instance snd_compat { A B } (RA:relation A)(RB:relation B) :
- Proper (RA*RB ==> RB) Snd.
-Proof.
-intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
-Qed.
-
-Instance RelCompFun_compat {A B}(f:A->B)(R : relation B)
- `(Proper _ (Ri==>Ri==>Ro) R) :
- Proper (Ri@@f==>Ri@@f==>Ro) (R@@f)%signature.
-Proof. unfold RelCompFun; firstorder. Qed.
+Section RelProd_Instances.
+
+  Context {A : Type} {B : Type} (RA : relation A) (RB : relation B).
+
+  Global Instance RelProd_Reflexive `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).
+  Proof. firstorder. Qed.
+
+  Global Instance RelProd_Symmetric `(Symmetric _ RA, Symmetric _ RB)
+  : Symmetric (RA*RB).
+  Proof. firstorder. Qed.
+
+  Global Instance RelProd_Transitive 
+           `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
+  Proof. firstorder. Qed.
+
+  Global Program Instance RelProd_Equivalence 
+          `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
+
+  Lemma FstRel_ProdRel :
+    relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)).
+  Proof. firstorder. Qed.
+  
+  Lemma SndRel_ProdRel :
+    relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB).
+  Proof. firstorder. Qed.
+  
+  Global Instance FstRel_sub :
+    subrelation (RA*RB) (RA @@1).
+  Proof. firstorder. Qed.
+
+  Global Instance SndRel_sub :
+    subrelation (RA*RB) (RB @@2).
+  Proof. firstorder. Qed.
+  
+  Global Instance pair_compat :
+    Proper (RA==>RB==> RA*RB) (@pair _ _).
+  Proof. firstorder. Qed.
+  
+  Global Instance fst_compat :
+    Proper (RA*RB ==> RA) Fst.
+  Proof.
+    intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
+  Qed.
+
+  Global Instance snd_compat :
+    Proper (RA*RB ==> RB) Snd.
+  Proof.
+    intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
+  Qed.
+
+  Global Instance RelCompFun_compat (f:A->B)
+           `(Proper _ (Ri==>Ri==>Ro) RB) :
+    Proper (Ri@@f==>Ri@@f==>Ro) (RB@@f)%signature.
+  Proof. unfold RelCompFun; firstorder. Qed.
+End RelProd_Instances.
 
 Hint Unfold RelProd RelCompFun.
 Hint Extern 2 (RelProd _ _ _ _) => split.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 7bc208c45..3ea8fe10e 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -121,7 +121,7 @@ Program Instance bool_function_eqdec `(! EqDec (eq_setoid A))
       else in_right
     else in_right.
 
-  Solve Obligations with try red ; unfold equiv, complement ; program_simpl.
+  Solve Obligations with try red ; unfold complement ; program_simpl.
 
   Next Obligation.
   Proof.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 5d34a4bf5..bee922c6f 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1247,11 +1247,11 @@ Proof.
  intros m1 m2; functional induction (concat m1 m2); intros; auto;
  try factornode _x _x0 _x1 _x2 _x3 as m1.
  apply join_bst; auto.
- change (bst (m2',xd)#1); rewrite <-e1; eauto.
+ change (bst (m2',xd)#1). rewrite <-e1; eauto.
  intros y Hy.
  apply H1; auto.
  rewrite remove_min_in, e1; simpl; auto.
- change (gt_tree (m2',xd)#2#1 (m2',xd)#1); rewrite <-e1; eauto.
+ change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto.
 Qed.
 Hint Resolve concat_bst.
 
@@ -1930,7 +1930,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma Equivb_Equivb : forall cmp m m',
   Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
  Proof.
- intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition.
+ intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In. intuition. 
  generalize (H0 k); do 2 rewrite In_alt; intuition.
  generalize (H0 k); do 2 rewrite In_alt; intuition.
  generalize (H0 k); do 2 rewrite <- In_alt; intuition.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 85b7242b5..0e3b5cef1 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -437,12 +437,6 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb.
 destruct (eq_dec x y); auto.
 Qed.
 
-Definition option_map (A B:Type)(f:A->B)(o:option A) : option B :=
- match o with
-  | Some a => Some (f a)
-  | None => None
- end.
-
 Lemma map_o : forall m x (f:elt->elt'),
  find x (map f m) = option_map f (find x m).
 Proof.
@@ -678,7 +672,7 @@ Qed.
 Add Parametric Morphism elt : (@Empty elt)
  with signature Equal ==> iff as Empty_m.
 Proof.
-unfold Empty; intros m m' Hm; intuition.
+unfold Empty; intros m m' Hm. split; intros; intro. 
 rewrite <-Hm in H0; eapply H, H0.
 rewrite Hm in H0; eapply H, H0.
 Qed.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index f15ab222c..64d5b1c9a 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -527,7 +527,7 @@ Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' :=
    | nil => nil
    | (k,e)::m' => (k,f k e) :: mapi f m'
   end.
-
+ 
 End Elt.
 Section Elt2.
 (* A new section is necessary for previous definitions to work
@@ -543,14 +543,13 @@ Proof.
  intros m x e f.
  (* functional induction map elt elt' f m.  *) (* Marche pas ??? *)
  induction m.
- inversion 1.
+ inversion 1. 
 
  destruct a as (x',e').
  simpl.
- inversion_clear 1.
+ inversion_clear 1.  
  constructor 1.
  unfold eqke in *; simpl in *; intuition congruence.
- constructor 2.
  unfold MapsTo in *; auto.
 Qed.
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 792b88717..253800a45 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -8,7 +8,7 @@
 
 (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *)
 
-Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface.
+Require Import Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface.
 
 Set Implicit Arguments.
 Local Open Scope positive_scope.
@@ -69,7 +69,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Module E:=PositiveOrderedTypeBits.
   Module ME:=KeyOrderedType E.
 
-  Definition key := positive.
+  Definition key := positive : Type. 
 
   Inductive tree (A : Type) :=
     | Leaf : tree A
@@ -93,7 +93,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     | _ => false
    end.
 
-  Fixpoint find (i : positive) (m : t A) : option A :=
+  Fixpoint find (i : key) (m : t A) : option A :=
     match m with
     | Leaf => None
     | Node l o r =>
@@ -104,7 +104,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint mem (i : positive) (m : t A) : bool :=
+  Fixpoint mem (i : key) (m : t A) : bool :=
     match m with
     | Leaf => false
     | Node l o r =>
@@ -115,7 +115,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint add (i : positive) (v : A) (m : t A) : t A :=
+  Fixpoint add (i : key) (v : A) (m : t A) : t A :=
     match m with
     | Leaf =>
         match i with
@@ -131,7 +131,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint remove (i : positive) (m : t A) : t A :=
+  Fixpoint remove (i : key) (m : t A) : t A :=
     match i with
     | xH =>
         match m with
@@ -163,7 +163,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   (** [elements] *)
 
-    Fixpoint xelements (m : t A) (i : positive) : list (positive * A) :=
+    Fixpoint xelements (m : t A) (i : key) : list (key * A) :=
       match m with
       | Leaf => nil
       | Node l None r =>
@@ -190,33 +190,33 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Section CompcertSpec.
 
   Theorem gempty:
-    forall (i: positive), find i empty = None.
+    forall (i: key), find i empty = None.
   Proof.
     destruct i; simpl; auto.
   Qed.
 
   Theorem gss:
-    forall (i: positive) (x: A) (m: t A), find i (add i x m) = Some x.
+    forall (i: key) (x: A) (m: t A), find i (add i x m) = Some x.
   Proof.
     induction i; destruct m; simpl; auto.
   Qed.
 
-  Lemma gleaf : forall (i : positive), find i (Leaf : t A) = None.
+  Lemma gleaf : forall (i : key), find i (Leaf : t A) = None.
   Proof. exact gempty. Qed.
 
   Theorem gso:
-    forall (i j: positive) (x: A) (m: t A),
+    forall (i j: key) (x: A) (m: t A),
     i <> j -> find i (add j x m) = find i m.
   Proof.
     induction i; intros; destruct j; destruct m; simpl;
        try rewrite <- (gleaf i); auto; try apply IHi; congruence.
   Qed.
 
-  Lemma rleaf : forall (i : positive), remove i (Leaf : t A) = Leaf.
+  Lemma rleaf : forall (i : key), remove i (Leaf : t A) = Leaf.
   Proof. destruct i; simpl; auto. Qed.
 
   Theorem grs:
-    forall (i: positive) (m: t A), find i (remove i m) = None.
+    forall (i: key) (m: t A), find i (remove i m) = None.
   Proof.
     induction i; destruct m.
      simpl; auto.
@@ -236,7 +236,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
   Theorem gro:
-    forall (i j: positive) (m: t A),
+    forall (i j: key) (m: t A),
     i <> j -> find i (remove j m) = find i m.
   Proof.
     induction i; intros; destruct j; destruct m;
@@ -265,11 +265,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
   Lemma xelements_correct:
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       find i m = Some v -> List.In (append j i, v) (xelements m j).
     Proof.
       induction m; intros.
-       rewrite (gleaf i) in H; congruence.
+       rewrite (gleaf i) in H; discriminate. 
        destruct o; destruct i; simpl; simpl in H.
         rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
           apply IHm2; auto.
@@ -282,14 +282,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
   Theorem elements_correct:
-    forall (m: t A) (i: positive) (v: A),
+    forall (m: t A) (i: key) (v: A),
     find i m = Some v -> List.In (i, v) (elements m).
   Proof.
     intros m i v H.
     exact (xelements_correct m i xH H).
   Qed.
 
-  Fixpoint xfind (i j : positive) (m : t A) : option A :=
+  Fixpoint xfind (i j : key) (m : t A) : option A :=
       match i, j with
       | _, xH => find i m
       | xO ii, xO jj => xfind ii jj m
@@ -298,7 +298,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       end.
 
    Lemma xfind_left :
-      forall (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
+      forall (j i : key) (m1 m2 : t A) (o : option A) (v : A),
       xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v.
     Proof.
       induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
@@ -306,7 +306,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_ii :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j).
     Proof.
       induction m.
@@ -322,7 +322,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_io :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       ~List.In (xI i, v) (xelements m (xO j)).
     Proof.
       induction m.
@@ -337,7 +337,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_oo :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       List.In (xO i, v) (xelements m (xO j)) -> List.In (i, v) (xelements m j).
     Proof.
       induction m.
@@ -353,7 +353,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_oi :
-      forall (m: t A) (i j : positive) (v: A),
+      forall (m: t A) (i j : key) (v: A),
       ~List.In (xO i, v) (xelements m (xI j)).
     Proof.
       induction m.
@@ -368,7 +368,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_ih :
-      forall (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      forall (m1 m2: t A) (o: option A) (i : key) (v: A),
       List.In (xI i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m2 xH).
     Proof.
       destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -381,7 +381,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_oh :
-      forall (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      forall (m1 m2: t A) (o: option A) (i : key) (v: A),
       List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH).
     Proof.
       destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
@@ -394,7 +394,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_hi :
-      forall (m: t A) (i : positive) (v: A),
+      forall (m: t A) (i : key) (v: A),
       ~List.In (xH, v) (xelements m (xI i)).
     Proof.
       induction m; intros.
@@ -409,7 +409,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma xelements_ho :
-      forall (m: t A) (i : positive) (v: A),
+      forall (m: t A) (i : key) (v: A),
       ~List.In (xH, v) (xelements m (xO i)).
     Proof.
       induction m; intros.
@@ -424,13 +424,13 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
     Lemma find_xfind_h :
-      forall (m: t A) (i: positive), find i m = xfind i xH m.
+      forall (m: t A) (i: key), find i m = xfind i xH m.
     Proof.
       destruct i; simpl; auto.
     Qed.
 
     Lemma xelements_complete:
-      forall (i j : positive) (m: t A) (v: A),
+      forall (i j : key) (m: t A) (v: A),
       List.In (i, v) (xelements m j) -> xfind i j m = Some v.
     Proof.
       induction i; simpl; intros; destruct j; simpl.
@@ -458,7 +458,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     Qed.
 
   Theorem elements_complete:
-    forall (m: t A) (i: positive) (v: A),
+    forall (m: t A) (i: key) (v: A),
     List.In (i, v) (elements m) -> find i m = Some v.
   Proof.
     intros m i v H.
@@ -479,18 +479,18 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   End CompcertSpec.
 
-  Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v.
+  Definition MapsTo (i:key)(v:A)(m:t A) := find i m = Some v.
 
-  Definition In (i:positive)(m:t A) := exists e:A, MapsTo i e m.
+  Definition In (i:key)(m:t A) := exists e:A, MapsTo i e m.
 
-  Definition Empty m := forall (a : positive)(e:A) , ~ MapsTo a e m.
+  Definition Empty m := forall (a : key)(e:A) , ~ MapsTo a e m.
 
-  Definition eq_key (p p':positive*A) := E.eq (fst p) (fst p').
+  Definition eq_key (p p':key*A) := E.eq (fst p) (fst p').
 
-  Definition eq_key_elt (p p':positive*A) :=
+  Definition eq_key_elt (p p':key*A) :=
           E.eq (fst p) (fst p') /\ (snd p) = (snd p').
 
-  Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
+  Definition lt_key (p p':key*A) := E.lt (fst p) (fst p').
 
   Global Instance eqk_equiv : Equivalence eq_key := _.
   Global Instance eqke_equiv : Equivalence eq_key_elt := _.
@@ -715,8 +715,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Lemma elements_3w : NoDupA eq_key (elements m).
   Proof.
-  change eq_key with (@ME.eqk A).
-  apply ME.Sort_NoDupA; apply elements_3; auto.
+    apply ME.Sort_NoDupA.
+    apply elements_3.
   Qed.
 
   End FMapSpec.
@@ -727,9 +727,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Section Mapi.
 
-    Variable f : positive -> A -> B.
+    Variable f : key -> A -> B.
 
-    Fixpoint xmapi (m : t A) (i : positive) : t B :=
+    Fixpoint xmapi (m : t A) (i : key) : t B :=
        match m with
         | Leaf => @Leaf B
         | Node l o r => Node (xmapi l (append i (xO xH)))
@@ -746,7 +746,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   End A.
 
   Lemma xgmapi:
-      forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A),
+      forall (A B: Type) (f: key -> A -> B) (i j : key) (m: t A),
       find i (xmapi f m j) = option_map (f (append j i)) (find i m).
   Proof.
   induction i; intros; destruct m; simpl; auto.
@@ -756,7 +756,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
   Theorem gmapi:
-    forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A),
+    forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A),
     find i (mapi f m) = option_map (f i) (find i m).
   Proof.
   intros.
@@ -820,7 +820,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r)
       end.
 
-  Lemma xgmap2_l : forall (i : positive) (m : t A),
+  Lemma xgmap2_l : forall (i : key) (m : t A),
           f None None = None -> find i (xmap2_l m) = f (find i m) None.
     Proof.
       induction i; intros; destruct m; simpl; auto.
@@ -832,7 +832,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
       | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r)
       end.
 
-  Lemma xgmap2_r : forall (i : positive) (m : t B),
+  Lemma xgmap2_r : forall (i : key) (m : t B),
           f None None = None -> find i (xmap2_r m) = f None (find i m).
     Proof.
       induction i; intros; destruct m; simpl; auto.
@@ -848,7 +848,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-    Lemma gmap2: forall (i: positive)(m1:t A)(m2: t B),
+    Lemma gmap2: forall (i: key)(m1:t A)(m2: t B),
       f None None = None ->
       find i (_map2 m1 m2) = f (find i m1) (find i m2).
     Proof.
@@ -896,9 +896,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Section Fold.
 
     Variables A B : Type.
-    Variable f : positive -> A -> B -> B.
+    Variable f : key -> A -> B -> B.
 
-    Fixpoint xfoldi (m : t A) (v : B) (i : positive) :=
+    Fixpoint xfoldi (m : t A) (v : B) (i : key) :=
       match m with
         | Leaf _ => v
         | Node l (Some x) r =>
@@ -1070,7 +1070,7 @@ Module PositiveMapAdditionalFacts.
 
   (* Derivable from the Map interface *)
   Theorem gsspec:
-    forall (A:Type)(i j: positive) (x: A) (m: t A),
+    forall (A:Type)(i j: key) (x: A) (m: t A),
     find i (add j x m) = if E.eq_dec i j then Some x else find i m.
   Proof.
     intros.
@@ -1079,7 +1079,7 @@ Module PositiveMapAdditionalFacts.
 
    (* Not derivable from the Map interface *)
   Theorem gsident:
-    forall (A:Type)(i: positive) (m: t A) (v: A),
+    forall (A:Type)(i: key) (m: t A) (v: A),
     find i m = Some v -> add i v m = m.
   Proof.
     induction i; intros; destruct m; simpl; simpl in H; try congruence.
@@ -1118,4 +1118,3 @@ Module PositiveMapAdditionalFacts.
   Qed.
 
 End PositiveMapAdditionalFacts.
-
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 670d09154..efd49f54e 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -27,7 +27,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Module E:=PositiveOrderedTypeBits.
 
-  Definition elt := positive.
+  Definition elt := positive : Type.
 
   Inductive tree :=
     | Leaf : tree
@@ -35,9 +35,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Scheme tree_ind := Induction for tree Sort Prop.
 
-  Definition t := tree.
+  Definition t := tree : Type.
 
-  Definition empty := Leaf.
+  Definition empty : t := Leaf.
 
   Fixpoint is_empty (m : t) : bool :=
    match m with
@@ -45,7 +45,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     | Node l b r => negb b &&& is_empty l &&& is_empty r
    end.
 
+<<<<<<< HEAD
   Fixpoint mem (i : positive) (m : t) {struct m} : bool :=
+=======
+  Fixpoint mem (i : elt) (m : t) : bool :=
+>>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
     match m with
     | Leaf => false
     | Node l o r =>
@@ -56,7 +60,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint add (i : positive) (m : t) : t :=
+  Fixpoint add (i : elt) (m : t) : t :=
     match m with
     | Leaf =>
         match i with
@@ -76,13 +80,17 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** helper function to avoid creating empty trees that are not leaves *)
 
-  Definition node l (b: bool) r :=
+  Definition node (l : t) (b: bool) (r : t) : t :=
     if b then Node l b r else
      match l,r with
        | Leaf,Leaf => Leaf
        | _,_ => Node l false r end.
 
+<<<<<<< HEAD
   Fixpoint remove (i : positive) (m : t) {struct m} : t :=
+=======
+  Fixpoint remove (i : elt) (m : t) : t :=
+>>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -93,7 +101,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint union (m m': t) :=
+  Fixpoint union (m m': t) : t :=
     match m with
       | Leaf => m'
       | Node l o r =>
@@ -103,7 +111,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint inter (m m': t) :=
+  Fixpoint inter (m m': t) : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -113,7 +121,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint diff (m m': t) :=
+  Fixpoint diff (m m': t) : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -145,7 +153,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** reverses [y] and concatenate it with [x] *)
 
-  Fixpoint rev_append y x :=
+  Fixpoint rev_append (y x : elt) : elt :=
     match y with
       | 1 => x
       | y~1 => rev_append y x~1
@@ -156,8 +164,8 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Section Fold.
 
-    Variables B : Type.
-    Variable f : positive -> B -> B.
+    Variable B : Type.
+    Variable f : elt -> B -> B.
 
     (** the additional argument, [i], records the current path, in
        reverse order (this should be more efficient: we reverse this argument
@@ -165,7 +173,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        we also use this convention in all functions below
      *)
 
-    Fixpoint xfold (m : t) (v : B) (i : positive) :=
+    Fixpoint xfold (m : t) (v : B) (i : elt) :=
       match m with
         | Leaf => v
         | Node l true r =>
@@ -179,9 +187,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Section Quantifiers.
 
-    Variable f : positive -> bool.
+    Variable f : elt -> bool.
 
-    Fixpoint xforall (m : t) (i : positive) :=
+    Fixpoint xforall (m : t) (i : elt) :=
       match m with
         | Leaf => true
         | Node l o r =>
@@ -189,21 +197,21 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       end.
     Definition for_all m := xforall m 1.
 
-    Fixpoint xexists (m : t) (i : positive) :=
+    Fixpoint xexists (m : t) (i : elt) :=
       match m with
         | Leaf => false
         | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0
       end.
     Definition exists_ m := xexists m 1.
 
-    Fixpoint xfilter (m : t) (i : positive) :=
+    Fixpoint xfilter (m : t) (i : elt) : t :=
       match m with
         | Leaf => Leaf
         | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
       end.
     Definition filter m := xfilter m 1.
 
-    Fixpoint xpartition (m : t) (i : positive) :=
+    Fixpoint xpartition (m : t) (i : elt) : t * t :=
       match m with
         | Leaf => (Leaf,Leaf)
         | Node l o r =>
@@ -221,7 +229,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** uses [a] to accumulate values rather than doing a lot of concatenations *)
 
-  Fixpoint xelements (m : t) (i : positive) (a: list positive) :=
+  Fixpoint xelements (m : t) (i : elt) (a: list elt) :=
     match m with
       | Leaf => a
       | Node l false r => xelements l i~0 (xelements r i~1 a)
@@ -245,7 +253,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** would it be more efficient to use a path like in the above functions ? *)
 
-  Fixpoint choose (m: t) :=
+  Fixpoint choose (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r => if o then Some 1 else
@@ -255,7 +263,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint min_elt (m: t) :=
+  Fixpoint min_elt (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r =>
@@ -265,7 +273,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint max_elt (m: t) :=
+  Fixpoint max_elt (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r =>
@@ -750,7 +758,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof. intros. rewrite diff_spec. split; assumption. Qed.
 
   (** Specification of [fold] *)
-
+  
   Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
@@ -798,15 +806,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        rewrite <- andb_lazy_alt. apply andb_true_iff.
   Qed.
 
-  Lemma filter_1 : forall s x f, compat_bool E.eq f ->
+  Lemma filter_1 : forall s x f, @compat_bool elt E.eq f ->
     In x (filter f s) -> In x s.
   Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
 
-  Lemma filter_2 : forall s x f, compat_bool E.eq f ->
+  Lemma filter_2 : forall s x f, @compat_bool elt E.eq f ->
     In x (filter f s) -> f x = true.
   Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
 
-  Lemma filter_3 : forall s x f, compat_bool E.eq f -> In x s ->
+  Lemma filter_3 : forall s x f, @compat_bool elt E.eq f -> In x s ->
     f x = true -> In x (filter f s).
   Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
 
@@ -831,11 +839,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         apply H. assumption.
   Qed.
 
-  Lemma for_all_1 : forall s f, compat_bool E.eq f ->
+  Lemma for_all_1 : forall s f, @compat_bool elt E.eq f ->
     For_all (fun x => f x = true) s -> for_all f s = true.
   Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.
 
-  Lemma for_all_2 : forall s f, compat_bool E.eq f ->
+  Lemma for_all_2 : forall s f, @compat_bool elt E.eq f ->
     for_all f s = true -> For_all (fun x => f x = true) s.
   Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.
 
@@ -858,11 +866,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        intros [[x|x|] H]; eauto.
   Qed.
 
-  Lemma exists_1 : forall s f, compat_bool E.eq f ->
+  Lemma exists_1 : forall s f, @compat_bool elt E.eq f ->
       Exists (fun x => f x = true) s -> exists_ f s = true.
   Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.
 
-  Lemma exists_2 : forall s f, compat_bool E.eq f ->
+  Lemma exists_2 : forall s f, @compat_bool elt E.eq f ->
       exists_ f s = true -> Exists (fun x => f x = true) s.
   Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.
 
@@ -878,11 +886,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o; simpl; rewrite IHl, IHr; reflexivity.
   Qed.
 
-  Lemma partition_1 : forall s f, compat_bool E.eq f ->
+  Lemma partition_1 : forall s f, @compat_bool elt E.eq f ->
       Equal (fst (partition f s)) (filter f s).
   Proof. intros. rewrite partition_filter. apply eq_refl. Qed.
 
-  Lemma partition_2 : forall s f, compat_bool E.eq f ->
+  Lemma partition_2 : forall s f, @compat_bool elt E.eq f ->
       Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
   Proof. intros. rewrite partition_filter. apply eq_refl. Qed.
 
@@ -990,7 +998,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       constructor.
        intros x H. apply E.lt_not_eq in H. apply H. reflexivity.
        intro. apply E.lt_trans.
-      intros ? ? <- ? ? <-. reflexivity.
+     solve_proper.
       apply elements_3.
   Qed.
 
@@ -1101,7 +1109,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
           destruct (min_elt r).
             injection H. intros <-. clear H.
             destruct y as [z|z|].
-              apply (IHr p z); trivial.
+              apply (IHr e z); trivial.
               elim (Hp _ H').
               discriminate.
             discriminate.
@@ -1155,7 +1163,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
             injection H. intros <-. clear H.
             destruct y as [z|z|].
               elim (Hp _ H').
-              apply (IHl p z); trivial.
+              apply (IHl e z); trivial.
               discriminate.
             discriminate.
   Qed.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index a95695454..cc46fe617 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -143,6 +143,8 @@ Arguments S _%nat.
 (********************************************************************)
 (** * Container datatypes *)
 
+Set Universe Polymorphism.
+
 (** [option A] is the extension of [A] with an extra element [None] *)
 
 Inductive option (A:Type) : Type :=
@@ -182,7 +184,8 @@ Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 Arguments pair {A B} _ _.
 
 Section projections.
-  Variables A B : Type.
+  Context {A : Type} {B : Type}.
+
   Definition fst (p:A * B) := match p with
 				| (x, y) => x
                               end.
@@ -244,8 +247,10 @@ Definition app (A : Type) : list A -> list A -> list A :=
    | a :: l1 => a :: app l1 m
   end.
 
+
 Infix "++" := app (right associativity, at level 60) : list_scope.
 
+Unset Universe Polymorphism.
 
 (********************************************************************)
 (** * The comparison datatype *)
@@ -310,6 +315,7 @@ Defined.
 
 Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
  CompareSpec (eq x y) (lt x y) (lt y x).
+
 Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
  CompareSpecT (eq x y) (lt x y) (lt y x).
 Hint Unfold CompSpec CompSpecT.
@@ -336,8 +342,11 @@ Arguments identity_rect [A] a P f y i.
 
 (** Identity type *)
 
-Definition ID := forall A:Type, A -> A.
-Definition id : ID := fun A x => x.
+Polymorphic Definition ID := forall A:Type, A -> A.
+Polymorphic Definition id : ID := fun A x => x.
+
+Definition IDProp := forall A:Prop, A -> A.
+Definition idProp : IDProp := fun A x => x.
 
 
 (* begin hide *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 9251d00ff..f994b4ca6 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -15,6 +15,7 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope.
 (** * Propositional connectives *)
 
 (** [True] is the always true proposition *)
+
 Inductive True : Prop :=
   I : True.
 
@@ -232,7 +233,6 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
    P x] is in fact equivalent to [ex (fun x => P x)] which may be not
    convertible to [ex P] if [P] is not itself an abstraction *)
 
-
 Inductive ex (A:Type) (P:A -> Prop) : Prop :=
   ex_intro : forall x:A, P x -> ex (A:=A) P.
 
@@ -301,7 +301,8 @@ Arguments eq_ind [A] x P _ y _.
 Arguments eq_rec [A] x P _ y _.
 Arguments eq_rect [A] x P _ y _.
 
-Hint Resolve I conj or_introl or_intror eq_refl: core.
+Hint Resolve I conj or_introl or_intror : core. 
+Hint Resolve eq_refl: core. 
 Hint Resolve ex_intro ex_intro2: core.
 
 Section Logic_lemmas.
@@ -341,7 +342,7 @@ Section Logic_lemmas.
 
   Definition eq_ind_r :
     forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
+    intros A x P H y H0. elim eq_sym with (1 := H0); assumption.
   Defined.
 
   Definition eq_rec_r :
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index f58c21f48..f534dd6c6 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -21,19 +21,19 @@ Require Import Logic.
     Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset
     of elements of the type [A] which satisfy both [P] and [Q]. *)
 
-Inductive sig (A:Type) (P:A -> Prop) : Type :=
+Polymorphic Inductive sig (A:Type) (P:A -> Prop) : Type :=
     exist : forall x:A, P x -> sig P.
 
-Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
+Polymorphic Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
     exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
 (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
     Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
 
-Inductive sigT (A:Type) (P:A -> Type) : Type :=
+Polymorphic Inductive sigT (A:Type) (P:A -> Type) : Type :=
     existT : forall x:A, P x -> sigT P.
 
-Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
+Polymorphic Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
     existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
 
 (* Notations *)
@@ -65,7 +65,7 @@ Add Printing Let sigT2.
     [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the
     proof of [(P a)] *)
 
-
+Set Universe Polymorphism.
 Section Subset_projections.
 
   Variable A : Type.
@@ -123,6 +123,8 @@ End Subset_projections2.
     [(projT1 x)] is the first projection and [(projT2 x)] is the
     second projection, the type of which depends on the [projT1]. *)
 
+
+
 Section Projections.
 
   Variable A : Type.
@@ -131,6 +133,7 @@ Section Projections.
   Definition projT1 (x:sigT P) : A := match x with
                                       | existT _ a _ => a
                                       end.
+
   Definition projT2 (x:sigT P) : P (projT1 x) :=
     match x return P (projT1 x) with
     | existT _ _ h => h
@@ -212,6 +215,8 @@ Add Printing If sumor.
 Arguments inleft {A B} _ , [A] B _.
 Arguments inright {A B} _ , A [B] _.
 
+Unset Universe Polymorphism.
+
 (** Various forms of the axiom of choice for specifications *)
 
 Section Choice_lemmas.
@@ -257,10 +262,10 @@ Section Dependent_choice_lemmas.
     (forall x:X, {y | R x y}) ->
     forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}.
   Proof.
-    intros H x0.
+    intros H x0. 
     set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end).
     exists f.
-    split. reflexivity.
+    split. reflexivity. 
     induction n; simpl; apply proj2_sig.
   Defined.
 
@@ -273,11 +278,13 @@ End Dependent_choice_lemmas.
      [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)].
 
      It is implemented using the option type. *)
+Section Exc.
+  Variable A : Type.
 
-Definition Exc := option.
-Definition value := Some.
-Definition error := @None.
-
+  Definition Exc := option A.
+  Definition value := @Some A.
+  Definition error := @None A.
+End Exc.
 Arguments error [A].
 
 Definition except := False_rec. (* for compatibility with previous versions *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d282fe8c3..f6a0382c2 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -10,7 +10,7 @@ Require Import Le Gt Minus Bool.
 Require Setoid.
 
 Set Implicit Arguments.
-
+Set Universe Polymorphism.
 
 (******************************************************************)
 (** * Basics: definition of polymorphic lists and some operations *)
@@ -65,8 +65,6 @@ End ListNotations.
 
 Import ListNotations.
 
-(** ** Facts about lists *)
-
 Section Facts.
 
   Variable A : Type.
@@ -131,7 +129,7 @@ Section Facts.
   subst a; auto.
   exists [], l; auto.
   destruct (IHl H) as (l1,(l2,H0)).
-  exists (a::l1), l2; simpl; f_equal; auto.
+  exists (a::l1), l2; simpl. apply f_equal. auto.
   Qed.
 
   (** Inversion *)
@@ -174,7 +172,7 @@ Section Facts.
   Qed.
 
   Theorem app_nil_r : forall l:list A, l ++ [] = l.
-  Proof.
+  Proof. 
     induction l; simpl; f_equal; auto.
   Qed.
 
@@ -654,8 +652,6 @@ Section Elts.
 
 End Elts.
 
-
-
 (*******************************)
 (** * Manipulating whole lists *)
 (*******************************)
@@ -858,7 +854,7 @@ End ListOps.
 (************)
 
 Section Map.
-  Variables A B : Type.
+  Variables (A : Type) (B : Type).
   Variable f : A -> B.
 
   Fixpoint map (l:list A) : list B :=
@@ -983,7 +979,7 @@ Qed.
 (************************************)
 
 Section Fold_Left_Recursor.
-  Variables A B : Type.
+  Variables (A : Type) (B : Type).
   Variable f : A -> B -> A.
 
   Fixpoint fold_left (l:list B) (a0:A) : A :=
@@ -1021,7 +1017,7 @@ Qed.
 (************************************)
 
 Section Fold_Right_Recursor.
-  Variables A B : Type.
+  Variables (A : Type) (B : Type).
   Variable f : B -> A -> A.
   Variable a0 : A.
 
@@ -1211,7 +1207,7 @@ End Fold_Right_Recursor.
   (******************************************************)
 
   Section ListPairs.
-    Variables A B : Type.
+    Variables (A : Type) (B : Type).
 
   (** [split] derives two lists from a list of pairs *)
 
@@ -2039,3 +2035,5 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *)
 
 Hint Resolve app_nil_end : datatypes v62.
 (* end hide *)
+
+Unset Universe Polymorphism.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 8fd229917..d75eb384f 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -11,7 +11,7 @@ Require Export Sorted.
 Require Export Setoid Basics Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
-
+Set Universe Polymorphism.
 (** * Logical relations over lists with respect to a setoid equality
       or ordering. *)
 
@@ -34,7 +34,7 @@ Hint Constructors InA.
     of the previous one. Having [InA = Exists eqA] raises too
     many compatibility issues. For now, we only state the equivalence: *)
 
-Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l.
+Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l. 
 Proof. split; induction 1; auto. Qed.
 
 Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
@@ -104,7 +104,7 @@ Hypothesis eqA_equiv : Equivalence eqA.
 Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
 Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
 Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
-
+ 
 Hint Resolve eqarefl eqatrans.
 Hint Immediate eqasym.
 
@@ -151,7 +151,7 @@ Qed.
 
 Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
 Proof.
- intros l x y H H'. rewrite <- H; auto.
+ intros l x y H H'. rewrite <- H. auto.
 Qed.
 Hint Immediate InA_eqA.
 
@@ -498,7 +498,7 @@ Proof.
  apply Hrec; auto.
  inv; auto.
  eapply NoDupA_split; eauto.
- invlist ForallOrdPairs; auto.
+ invlist ForallOrdPairs; auto. 
  eapply equivlistA_NoDupA_split; eauto.
  transitivity (f y (fold_right f i (s1++s2))).
  apply Comp; auto. reflexivity.
@@ -819,7 +819,6 @@ intros.
 rewrite filter_In in H; destruct H.
 eapply SortA_InfA_InA; eauto.
 Qed.
-
 Arguments eq {A} x _.
 
 Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
index b0657b63a..05f03ea56 100644
--- a/theories/Lists/SetoidPermutation.v
+++ b/theories/Lists/SetoidPermutation.v
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 Require Import SetoidList.
+Set Universe Polymorphism.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -88,7 +89,7 @@ Lemma PermutationA_cons_app l l₁ l₂ x :
   PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂).
 Proof.
  intros E. rewrite E.
- now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc.
+ now rewrite app_comm_cons, (PermutationA_cons_append l₁ x), <- app_assoc.
 Qed.
 
 Lemma PermutationA_middle l₁ l₂ x :
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 383775735..cb61e8f00 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -67,18 +67,13 @@ Variables A B : Prop.
 
 Record retract : Prop :=
   {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
-
 Record retract_cond : Prop :=
   {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
 
-
 (** The dependent elimination above implies the axiom of choice: *)
-Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
-Proof.
-intros r.
-case r; simpl.
-trivial.
-Qed.
+
+Lemma AC : forall r:retract_cond, retract -> forall a:A, r.(j2) (r.(i2) a) = a.
+Proof. intros r. exact r.(inv2). Qed.
 
 End Retracts.
 
@@ -114,7 +109,7 @@ Proof.
 exists g f.
 intro a.
 unfold f, g; simpl.
-apply AC.
+apply AC. 
 exists (fun x:pow U => x) (fun x:pow U => x).
 trivial.
 Qed.
@@ -132,9 +127,10 @@ Lemma not_has_fixpoint : R R = Not_b (R R).
 Proof.
 unfold R at 1.
 unfold g.
-rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
+rewrite AC.
+trivial.
+exists (fun x:pow U => x) (fun x:pow U => x).
 trivial.
-exists (fun x:pow U => x) (fun x:pow U => x); trivial.
 Qed.
 
 
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index b22f58dad..57a82161d 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -96,6 +96,12 @@ Local Unset Intuition Negation Unfolding.
 
 (** Choice, reification and description schemes *)
 
+(** We make them all polymorphic. most of them have existentials as conclusion
+    so they require polymorphism otherwise their first application (e.g. to an
+    existential in [Set]) will fix the level of [A].
+*)
+Set Universe Polymorphism.
+
 Section ChoiceSchemes.
 
 Variables A B :Type.
@@ -217,39 +223,39 @@ End ChoiceSchemes.
 (** Generalized schemes *)
 
 Notation RelationalChoice :=
-  (forall A B, RelationalChoice_on A B).
+  (forall A B : Type, RelationalChoice_on A B).
 Notation FunctionalChoice :=
-  (forall A B, FunctionalChoice_on A B).
+  (forall A B : Type, FunctionalChoice_on A B).
 Definition FunctionalDependentChoice :=
-  (forall A, FunctionalDependentChoice_on A).
+  (forall A : Type, FunctionalDependentChoice_on A).
 Definition FunctionalCountableChoice :=
-  (forall A, FunctionalCountableChoice_on A).
+  (forall A : Type, FunctionalCountableChoice_on A).
 Notation FunctionalChoiceOnInhabitedSet :=
-  (forall A B, inhabited B -> FunctionalChoice_on A B).
+  (forall A B : Type, inhabited B -> FunctionalChoice_on A B).
 Notation FunctionalRelReification :=
-  (forall A B, FunctionalRelReification_on A B).
+  (forall A B : Type, FunctionalRelReification_on A B).
 
 Notation GuardedRelationalChoice :=
-  (forall A B, GuardedRelationalChoice_on A B).
+  (forall A B : Type, GuardedRelationalChoice_on A B).
 Notation GuardedFunctionalChoice :=
-  (forall A B, GuardedFunctionalChoice_on A B).
+  (forall A B : Type, GuardedFunctionalChoice_on A B).
 Notation GuardedFunctionalRelReification :=
-  (forall A B, GuardedFunctionalRelReification_on A B).
+  (forall A B : Type, GuardedFunctionalRelReification_on A B).
 
 Notation OmniscientRelationalChoice :=
-  (forall A B, OmniscientRelationalChoice_on A B).
+  (forall A B : Type, OmniscientRelationalChoice_on A B).
 Notation OmniscientFunctionalChoice :=
-  (forall A B, OmniscientFunctionalChoice_on A B).
+  (forall A B : Type, OmniscientFunctionalChoice_on A B).
 
 Notation ConstructiveDefiniteDescription :=
-  (forall A, ConstructiveDefiniteDescription_on A).
+  (forall A : Type, ConstructiveDefiniteDescription_on A).
 Notation ConstructiveIndefiniteDescription :=
-  (forall A, ConstructiveIndefiniteDescription_on A).
+  (forall A : Type, ConstructiveIndefiniteDescription_on A).
 
 Notation IotaStatement :=
-  (forall A, IotaStatement_on A).
+  (forall A : Type, IotaStatement_on A).
 Notation EpsilonStatement :=
-  (forall A, EpsilonStatement_on A).
+  (forall A : Type, EpsilonStatement_on A).
 
 (** Subclassical schemes *)
 
@@ -293,7 +299,7 @@ Proof.
 Qed.
 
 Lemma funct_choice_imp_rel_choice :
-  forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B.
+  forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B.
 Proof.
   intros A B FunCh R H.
   destruct (FunCh R H) as (f,H0).
@@ -306,7 +312,7 @@ Proof.
 Qed.
 
 Lemma funct_choice_imp_description :
-  forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
+  forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
 Proof.
   intros A B FunCh R H.
   destruct (FunCh R) as [f H0].
@@ -319,10 +325,10 @@ Proof.
 Qed.
 
 Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
-  forall A B, FunctionalChoice_on A B <->
+  forall A B : Type, FunctionalChoice_on A B <->
     RelationalChoice_on A B /\ FunctionalRelReification_on A B.
 Proof.
-  intros A B; split.
+  intros A B. split.
   intro H; split;
     [ exact (funct_choice_imp_rel_choice H)
       | exact (funct_choice_imp_description H) ].
@@ -363,7 +369,7 @@ Proof.
 Qed.
 
 Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
-  forall A B, inhabited B -> RelationalChoice_on A B ->
+  forall A B : Type, inhabited B -> RelationalChoice_on A B ->
     IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
 Proof.
   intros A B Inh AC_rel IndPrem P R H.
@@ -375,7 +381,7 @@ Proof.
 Qed.
 
 Lemma guarded_rel_choice_imp_rel_choice :
-  forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
+  forall A B : Type, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
 Proof.
   intros A B GAC_rel R H.
   destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
@@ -794,12 +800,13 @@ be applied on the same Type universes on both sides of the first
 Require Import Setoid.
 
 Theorem constructive_definite_descr_excluded_middle :
-  ConstructiveDefiniteDescription ->
+  (forall A : Type, ConstructiveDefiniteDescription_on A) ->
   (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
 Proof.
   intros Descr EM P.
   pose (select := fun b:bool => if b then P else ~P).
   assert { b:bool | select b } as ([|],HP).
+  red in Descr.
   apply Descr.
   rewrite <- unique_existence; split.
   destruct (EM P).
@@ -815,14 +822,13 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
   (forall P:Prop, P \/ ~ P) ->
   forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-  intros FunReify EM C; intuition auto using
+  intros FunReify EM C H. intuition auto using
     constructive_definite_descr_excluded_middle,
     (relative_non_contradiction_of_definite_descr (C:=C)).
 Qed.
 
 (**********************************************************************)
 (** * Choice => Dependent choice => Countable choice *)
-
 (* The implications below are standard *)
 
 Require Import Arith.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 87b279877..0eba49a7e 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -99,7 +99,7 @@ Lemma AC_bool_subset_to_bool :
 Proof.
   destruct (guarded_rel_choice _ _
    (fun Q:bool -> Prop =>  exists y : _, Q y)
-   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).
+   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). 
     exact (fun _ H => H).
   exists R; intros P HP.
   destruct (HR P HP) as (y,(Hy,Huni)).
@@ -172,7 +172,7 @@ Variables a1 a2 : A.
 
 (** We build the subset [A'] of [A] made of [a1] and [a2] *)
 
-Definition A' := sigT (fun x => x=a1 \/ x=a2).
+Definition A' := @sigT A (fun x => x=a1 \/ x=a2).
 
 Definition a1':A'.
 exists a1 ; auto.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 0e9f39f6b..2c971ec24 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -52,6 +52,8 @@ Table of contents:
 
 Import EqNotations.
 
+Set Universe Polymorphism.
+
 Section Dependent_Equality.
 
   Variable U : Type.
@@ -117,7 +119,7 @@ Lemma eq_sigT_eq_dep :
     existT P p x = existT P q y -> eq_dep p x q y.
 Proof.
   intros.
-  dependent rewrite H.
+  dependent rewrite H. 
   apply eq_dep_intro.
 Qed.
 
@@ -162,11 +164,12 @@ Proof.
   split; auto using eq_sig_eq_dep, eq_dep_eq_sig.
 Qed.
 
-(** Dependent equality is equivalent to a dependent pair of equalities *)
+(** Dependent equality is equivalent tco a dependent pair of equalities *)
 
 Set Implicit Arguments.
 
-Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}.
+Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> 
+                                                   {H:x1=x2 | rew H in H1 = H2}.
 Proof.
   intros; split; intro H.
   - change x2 with (projT1 (existT P x2 H2)).
@@ -191,7 +194,7 @@ Lemma eq_sigT_snd :
   forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2.
 Proof.
   intros.
-  unfold eq_sigT_fst.
+  unfold eq_sigT_fst. 
   change x2 with (projT1 (existT P x2 H2)).
   change H2 with (projT2 (existT P x2 H2)) at 3.
   destruct H.
@@ -271,8 +274,8 @@ Section Equivalences.
   Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
   Proof.
     intros eq_rect_eq; red; intros.
-    apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial.
-  Qed.
+    apply (eq_rect_eq__eq_dep1_eq eq_rect_eq). apply eq_dep_dep1; trivial.
+ Qed.
 
   (** Uniqueness of Identity Proofs (UIP) is a consequence of *)
   (** Injectivity of Dependent Equality *)
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 53b25d4a8..e4db81faf 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -35,6 +35,7 @@ Table of contents:
 (** * Streicher's K and injectivity of dependent pair hold on decidable types *)
 
 Set Implicit Arguments.
+Set Universe Polymorphism.
 
 Section EqdepDec.
 
@@ -203,7 +204,7 @@ Unset Implicit Arguments.
 
 Module Type DecidableType.
 
-  Parameter U:Type.
+  Monomorphic Parameter U:Type.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableType.
@@ -271,7 +272,7 @@ End DecidableEqDep.
 
 Module Type DecidableSet.
 
-  Parameter U:Type.
+  Parameter U:Set.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableSet.
@@ -294,23 +295,23 @@ Module DecidableEqDepSet (M:DecidableSet).
 
   Theorem eq_dep_eq :
     forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
-  Proof N.eq_dep_eq.
+  Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
 
   (** Uniqueness of Identity Proofs (UIP) *)
 
   Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
-  Proof N.UIP.
+  Proof (eq_dep_eq__UIP U eq_dep_eq).
 
   (** Uniqueness of Reflexive Identity Proofs *)
 
   Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x.
-  Proof N.UIP_refl.
+  Proof (UIP__UIP_refl U UIP).
 
   (** Streicher's axiom K *)
 
   Lemma Streicher_K :
     forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
-  Proof N.Streicher_K.
+  Proof (K_dec_type eq_dec).
 
   (** Proof-irrelevance on subsets of decidable sets *)
 
@@ -350,7 +351,7 @@ Qed.
 
 Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt.
 Proof.
-  change (match tt as b return tt = b -> Type with
+  change (match tt as b return tt = b -> Prop with
           | tt => fun x => x = eq_refl tt
           end x).
   destruct x; reflexivity.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 530e05559..b557a7867 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -28,9 +28,11 @@ Arguments JMeq_refl {A x} , [A] x.
 
 Hint Resolve JMeq_refl.
 
+Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
+
 Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
-Proof.
-destruct 1; trivial.
+Proof. 
+intros; destruct H; trivial.
 Qed.
 
 Hint Immediate JMeq_sym.
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 4f0d93fb9..843b9aaa7 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -856,7 +856,7 @@ intros.
 rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros; do 3 (rewrite fold_add; auto with *).
+intros. do 3 (rewrite fold_add; auto with *).
 do 3 rewrite fold_empty;auto.
 Qed.
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index bd8811689..a61ef8bcd 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -595,7 +595,7 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
   (** Specification of [lt] *)
   Instance lt_strorder : StrictOrder lt.
   Proof. constructor ; unfold lt; red.
-    unfold complement. red. intros. apply (irreflexivity H).
+    unfold complement. red. intros. apply (irreflexivity _ H).
     intros. transitivity y; auto.
   Qed.
 
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index b0e09b719..5c232f340 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -472,7 +472,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
    equal s s' = true <-> Equal s s'.
   Proof.
   induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl.
-  intuition.
+  intuition reflexivity. 
   split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv.
   split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv.
   inv.
@@ -820,7 +820,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
 
   Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
   Proof.
-  induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
+  induction s as [|x s IH]; intros [|x' s']; simpl; intuition. 
   elim_compare x x'; auto.
   Qed.
 
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index f3a1d39c9..25a8c1629 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -93,7 +93,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Module E:=PositiveOrderedTypeBits.
 
-  Definition elt := positive.
+  Definition elt := positive : Type.
 
   Inductive tree :=
     | Leaf : tree
@@ -101,9 +101,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   Scheme tree_ind := Induction for tree Sort Prop.
 
-  Definition t := tree.
+  Definition t := tree : Type.
 
-  Definition empty := Leaf.
+  Definition empty : t := Leaf.
 
   Fixpoint is_empty (m : t) : bool :=
    match m with
@@ -142,7 +142,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** helper function to avoid creating empty trees that are not leaves *)
 
-  Definition node l (b: bool) r :=
+  Definition node (l : t) (b: bool) (r : t) : t :=
     if b then Node l b r else
      match l,r with
        | Leaf,Leaf => Leaf
@@ -159,7 +159,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint union (m m': t) :=
+  Fixpoint union (m m': t) : t :=
     match m with
       | Leaf => m'
       | Node l o r =>
@@ -169,7 +169,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint inter (m m': t) :=
+  Fixpoint inter (m m': t) : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -179,7 +179,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint diff (m m': t) :=
+  Fixpoint diff (m m': t) : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -211,7 +211,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** reverses [y] and concatenate it with [x] *)
 
-  Fixpoint rev_append y x :=
+  Fixpoint rev_append (y x : elt) : elt :=
     match y with
       | 1 => x
       | y~1 => rev_append y x~1
@@ -262,14 +262,14 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       end.
     Definition exists_ m := xexists m 1.
 
-    Fixpoint xfilter (m : t) (i : positive) :=
+    Fixpoint xfilter (m : t) (i : positive) : t :=
       match m with
         | Leaf => Leaf
         | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
       end.
     Definition filter m := xfilter m 1.
 
-    Fixpoint xpartition (m : t) (i : positive) :=
+    Fixpoint xpartition (m : t) (i : positive) : t * t :=
       match m with
         | Leaf => (Leaf,Leaf)
         | Node l o r =>
@@ -311,7 +311,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
 
   (** would it be more efficient to use a path like in the above functions ? *)
 
-  Fixpoint choose (m: t) :=
+  Fixpoint choose (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r => if o then Some 1 else
@@ -321,7 +321,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint min_elt (m: t) :=
+  Fixpoint min_elt (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r =>
@@ -331,7 +331,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         end
     end.
 
-  Fixpoint max_elt (m: t) :=
+  Fixpoint max_elt (m: t) : option elt :=
     match m with
       | Leaf => None
       | Node l o r =>
@@ -805,7 +805,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        rewrite <- andb_lazy_alt. apply andb_true_iff.
   Qed.
 
-  Lemma filter_spec: forall s x f, compat_bool E.eq f ->
+  Lemma filter_spec: forall s x f, @compat_bool elt E.eq f ->
     (In x (filter f s) <-> In x s /\ f x = true).
   Proof. intros. apply xfilter_spec. Qed.
 
@@ -830,7 +830,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
         apply H. assumption.
   Qed.
 
-  Lemma for_all_spec: forall s f, compat_bool E.eq f ->
+  Lemma for_all_spec: forall s f, @compat_bool elt E.eq f ->
     (for_all f s = true <-> For_all (fun x => f x = true) s).
   Proof. intros. apply xforall_spec. Qed.
 
@@ -852,7 +852,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        intros [[x|x|] H]; eauto.
   Qed.
 
-  Lemma exists_spec : forall s f, compat_bool E.eq f ->
+  Lemma exists_spec : forall s f, @compat_bool elt E.eq f ->
     (exists_ f s = true <-> Exists (fun x => f x = true) s).
   Proof. intros. apply xexists_spec. Qed.
 
@@ -868,11 +868,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o; simpl; rewrite IHl, IHr; reflexivity.
   Qed.
 
-  Lemma partition_spec1 : forall s f, compat_bool E.eq f ->
+  Lemma partition_spec1 : forall s f, @compat_bool elt E.eq f ->
       Equal (fst (partition f s)) (filter f s).
   Proof. intros. rewrite partition_filter. reflexivity. Qed.
 
-  Lemma partition_spec2 : forall s f, compat_bool E.eq f ->
+  Lemma partition_spec2 : forall s f, @compat_bool elt E.eq f ->
       Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
   Proof. intros. rewrite partition_filter. reflexivity. Qed.
 
@@ -1079,7 +1079,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
           destruct (min_elt r).
             injection H. intros <-. clear H.
             destruct y as [z|z|].
-              apply (IHr p z); trivial.
+              apply (IHr e z); trivial.
               elim (Hp _ H').
               discriminate.
             discriminate.
@@ -1133,7 +1133,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
             injection H. intros <-. clear H.
             destruct y as [z|z|].
               elim (Hp _ H').
-              apply (IHl p z); trivial.
+              apply (IHl e z); trivial.
               discriminate.
             discriminate.
   Qed.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index f0cddcc38..d8f675ade 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -1047,7 +1047,7 @@ Qed.
 
 (** ** Filter *)
 
-Lemma filter_app A f (l l':list A) :
+Polymorphic Lemma filter_app A f (l l':list A) :
  List.filter f (l ++ l') = List.filter f l ++ List.filter f l'.
 Proof.
  induction l as [|x l IH]; simpl; trivial.
@@ -1196,7 +1196,7 @@ Lemma INV_rev l1 l2 acc :
 Proof.
  intros. rewrite rev_append_rev.
  apply SortA_app with X.eq; eauto with *.
- intros x y. inA. eapply l1_lt_acc; eauto.
+ intros x y. inA. eapply @l1_lt_acc; eauto.
 Qed.
 
 (** ** union *)
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 39e086c31..17c69d226 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -93,7 +93,7 @@ Module ZnZ.
     lor         : t -> t -> t;
     land        : t -> t -> t;
     lxor        : t -> t -> t }.
-
+ 
  Section Specs.
  Context {t : Type}{ops : Ops t}.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 809169a4d..a6bc44682 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -809,7 +809,7 @@ refine
  refine (@spec_ww_sqrt t w_is_even w_0 w_1 w_Bm1
            w_sub w_add_mul_div w_digits w_zdigits _ww_zdigits
                w_sqrt2 pred add_mul_div head0 compare
-            _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto.
+            _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); wwauto.
  exact ZnZ.spec_zdigits.
  exact ZnZ.spec_more_than_1_digit.
  exact ZnZ.spec_is_even.
@@ -846,7 +846,7 @@ refine
   intros (Hn,Hn').
   assert (E : ZnZ.to_Z y = [|WW x y|] mod wB).
   { simpl; symmetry.
-    rewrite Z.add_comm, Z.mod_add; auto with zarith.
+    rewrite Z.add_comm, Z.mod_add; auto with zarith nocore.
     apply Z.mod_small; eauto with ZnZ zarith. }
   rewrite E.
   unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto.
@@ -923,6 +923,7 @@ refine
 
 End Z_2nZ.
 
+
 Section MulAdd.
 
   Context {t : Type}{ops : ZnZ.Ops t}{specs : ZnZ.Specs ops}.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 8525b0e13..dddae7db5 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -211,8 +211,7 @@ Section DoubleDiv32.
  Variable w_div21       : w -> w -> w -> w*w.
  Variable ww_sub_c      : zn2z w -> zn2z w -> carry (zn2z w).
 
- Definition w_div32 a1 a2 a3 b1 b2 :=
-  Eval lazy beta iota delta [ww_add_c_cont ww_add] in
+ Definition w_div32_body a1 a2 a3 b1 b2 :=
   match w_compare a1 b1 with
   | Lt =>
     let (q,r) := w_div21 a1 a2 b1 in
@@ -233,6 +232,10 @@ Section DoubleDiv32.
   | Gt => (w_0, W0) (* cas absurde *)
   end.
 
+ Definition w_div32 a1 a2 a3 b1 b2 :=
+  Eval lazy beta iota delta [ww_add_c_cont ww_add w_div32_body] in
+     w_div32_body a1 a2 a3 b1 b2.
+
  (* Proof *)
 
   Variable w_digits      : positive.
@@ -312,26 +315,8 @@ Section DoubleDiv32.
    assert (U:= lt_0_wB w_digits); assert (U1:= lt_0_wwB w_digits).
    Spec_w_to_Z a1;Spec_w_to_Z a2;Spec_w_to_Z a3;Spec_w_to_Z b1;Spec_w_to_Z b2.
    rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Z.mul_assoc;rewrite <- Z.mul_add_distr_r.
-   change (w_div32 a1 a2 a3 b1 b2) with
-    match w_compare a1 b1 with
-    | Lt =>
-     let (q,r) := w_div21 a1 a2 b1 in
-     match ww_sub_c (w_WW r a3) (w_mul_c q b2) with
-     | C0 r1 => (q,r1)
-     | C1 r1 =>
-      let q := w_pred q in
-      ww_add_c_cont w_WW w_add_c w_add_carry_c
-      (fun r2=>(w_pred q, ww_add w_add_c w_add w_add_carry r2 (WW b1 b2)))
-      (fun r2 => (q,r2))
-      r1 (WW b1 b2)
-     end
-    | Eq =>
-     ww_add_c_cont w_WW w_add_c w_add_carry_c
-     (fun r => (w_Bm2, ww_add w_add_c w_add w_add_carry r (WW b1 b2)))
-     (fun r => (w_Bm1,r))
-     (WW (w_sub a2 b2) a3) (WW b1 b2)
-    | Gt => (w_0, W0) (* cas absurde *)
-    end.
+   change (w_div32 a1 a2 a3 b1 b2) with (w_div32_body a1 a2 a3 b1 b2).
+   unfold w_div32_body.
    rewrite spec_compare. case Z.compare_spec; intro Hcmp.
    simpl in Hlt.
    rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index df5d42bbc..789436334 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -692,7 +692,7 @@ intros x; case x; simpl ww_is_even.
  intros x y H; unfold ww_sqrt2.
  repeat match goal with |- context[split ?x] =>
    generalize (spec_split x); case (split x)
- end; simpl fst; simpl snd.
+ end; simpl @fst; simpl @snd.
  intros w0 w1 Hw0 w2 w3 Hw1.
  assert (U: wB/4 <= [|w2|]).
  case (Z.le_gt_cases (wB / 4) [|w2|]); auto; intros H1.
@@ -1193,7 +1193,7 @@ Qed.
   rewrite <- wwB_4_wB_4; auto.
   generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith.
   case (w_sqrt2 w0 w1); intros w2 c.
-  simpl ww_to_Z; simpl fst.
+  simpl ww_to_Z; simpl @fst.
   case c; unfold interp_carry; autorewrite with rm10.
   intros w3 (H6, H7); rewrite H6.
   assert (V1 := spec_to_Z w3);auto with zarith.
@@ -1256,7 +1256,7 @@ Qed.
   generalize (@spec_w_sqrt2 w0 w1 V);auto with zarith.
   case (w_sqrt2 w0 w1); intros w2 c.
   case (spec_to_Z w2); intros HH1 HH2.
-  simpl ww_to_Z; simpl fst.
+  simpl ww_to_Z; simpl @fst.
   assert (Hv3: [[ww_pred ww_zdigits]]
                  = Zpos (xO w_digits) - 1).
     rewrite spec_ww_pred; rewrite spec_ww_zdigits.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 03fc58c55..634ff7d63 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -623,7 +623,7 @@ Section Basics.
  rewrite i2l_length; omega.
  generalize (firstn_length (size-n) (i2l x)).
  rewrite i2l_length.
- intros H0 H1; rewrite H1 in H0.
+ intros H0 H1. rewrite H1 in H0.
  rewrite min_l in H0 by omega.
  simpl length in H0.
  omega.
@@ -882,16 +882,16 @@ Section Basics.
  destruct p; simpl snd.
 
  specialize IHn with p.
- destruct (p2ibis n p). simpl snd in *.
-rewrite nshiftr_S_tail.
+ destruct (p2ibis n p). simpl @snd in *.
+ rewrite nshiftr_S_tail.
  destruct (le_lt_dec size n).
  rewrite nshiftr_above_size; auto.
  assert (H:=nshiftr_0_firstl _ _ l IHn).
  replace (shiftr (twice_plus_one i)) with i; auto.
- destruct i; simpl in *; rewrite H; auto.
+ destruct i; simpl in *. rewrite H; auto.
 
  specialize IHn with p.
- destruct (p2ibis n p); simpl snd in *.
+ destruct (p2ibis n p); simpl @snd in *.
  rewrite nshiftr_S_tail.
  destruct (le_lt_dec size n).
  rewrite nshiftr_above_size; auto.
@@ -945,7 +945,7 @@ rewrite nshiftr_S_tail.
  intros.
  simpl p2ibis; destruct p; [ | | red; auto];
   specialize IHn with p;
-  destruct (p2ibis n p); simpl snd in *; simpl phi_inv_positive;
+  destruct (p2ibis n p); simpl @snd in *; simpl phi_inv_positive;
   rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice;
   replace (S (size - S n))%nat with (size - n)%nat by omega;
   apply IHn; omega.
@@ -1629,7 +1629,7 @@ Section Int31_Specs.
  Lemma spec_pos_mod : forall w p,
        [|ZnZ.pos_mod p w|] = [|w|] mod (2 ^ [|p|]).
  Proof.
- unfold ZnZ.pos_mod, int31_ops, compare31.
+ unfold int31_ops, ZnZ.pos_mod, compare31.
  change [|31|] with 31%Z.
  assert (forall w p, 31<=p -> [|w|] = [|w|] mod 2^p).
   intros.
@@ -1959,7 +1959,7 @@ Section Int31_Specs.
 
  Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|].
  intros Hj; generalize (spec_div i j Hj).
- case div31; intros q r; simpl fst.
+ case div31; intros q r; simpl @fst.
  intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith.
  rewrite H1; ring.
  Qed.
@@ -2094,7 +2094,7 @@ Section Int31_Specs.
  generalize (spec_div21 ih il j Hj Hj1).
  case div3121; intros q r (Hq, Hr).
  apply Zdiv_unique with (phi r); auto with zarith.
- simpl fst; apply eq_trans with (1 := Hq); ring.
+ simpl @fst; apply eq_trans with (1 := Hq); ring.
  Qed.
 
  Lemma sqrt312_step_correct rec ih il j:
@@ -2215,6 +2215,9 @@ Section Int31_Specs.
  apply Nat2Z.is_nonneg.
  Qed.
 
+ (* Avoid expanding [iter312_sqrt] before variables in the context. *)
+ Strategy 1 [iter312_sqrt].
+
  Lemma spec_sqrt2 : forall x y,
        wB/ 4 <= [|x|] ->
        let (s,r) := sqrt312 x y in
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 0e9323789..1e6593b10 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -95,7 +95,7 @@ Proof.
  intros.
  generalize (Even_or_Odd n) (Even_Odd_False n).
  rewrite <- even_spec, <- odd_spec.
- destruct (odd n), (even n); simpl; intuition.
+ destruct (odd n), (even n) ; simpl; intuition.
 Qed.
 
 Lemma negb_even : forall n, negb (even n) = odd n.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 8146fd014..6b6c85310 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -438,7 +438,7 @@ Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up.
 Proof.
  assert (Proper (eq==>eq==>Logic.eq) compare).
   intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order.
- intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx.
+ intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx.
 Qed.
 
 (** The spec of [sqrt_up] indeed determines it *)
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 621a2ed9c..adbbc5ea0 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -133,7 +133,6 @@ Proof.
 intros m n; unfold ltb at 1.
 f_equiv.
 rewrite recursion_succ; f_equiv'.
-reflexivity.
 Qed.
 
 (* Above, we rewrite applications of function. Is it possible to rewrite
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 67cab5507..f98e8da9a 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -13,7 +13,7 @@ and proves its properties *)
 
 Require Export NSub.
 
-Ltac f_equiv' := repeat (f_equiv; try intros ? ? ?; auto).
+Ltac f_equiv' := repeat (repeat f_equiv; try intros ? ? ?; auto).
 
 Module NStrongRecProp (Import N : NAxiomsRecSig').
 Include NSubProp N.
@@ -82,7 +82,6 @@ Proof.
 intros. unfold strong_rec0.
 f_equiv.
 rewrite recursion_succ; f_equiv'.
-reflexivity.
 Qed.
 
 Lemma strong_rec_0 : forall a,
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 93ae858d8..bfbcb9465 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -242,8 +242,8 @@ Module Make (W0:CyclicType) <: NType.
  Definition comparen_m n :
   forall m, word (dom_t n) (S m) -> dom_t n -> comparison :=
   let op := dom_op n in
-  let zero := @ZnZ.zero _ op in
-  let compare := @ZnZ.compare _ op in
+  let zero := ZnZ.zero (Ops:=op) in
+  let compare := ZnZ.compare (Ops:=op) in
   let compare0 := compare zero in
   fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
 
@@ -273,7 +273,7 @@ Module Make (W0:CyclicType) <: NType.
 
  Local Notation compare_folded :=
    (iter_sym _
-      (fun n => @ZnZ.compare _ (dom_op n))
+      (fun n => ZnZ.compare (Ops:=dom_op n))
       comparen_m
       comparenm
       CompOpp).
@@ -358,13 +358,13 @@ Module Make (W0:CyclicType) <: NType.
 
  Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t :=
   let op := dom_op n in
-  let zero := @ZnZ.zero _ op in
-  let succ := @ZnZ.succ _ op in
-  let add_c := @ZnZ.add_c _ op in
-  let mul_c := @ZnZ.mul_c _ op in
+  let zero := ZnZ.zero in
+  let succ := ZnZ.succ (Ops:=op) in
+  let add_c := ZnZ.add_c (Ops:=op) in
+  let mul_c := ZnZ.mul_c (Ops:=op) in
   let ww := @ZnZ.WW _ op in
   let ow := @ZnZ.OW _ op in
-  let eq0 := @ZnZ.eq0 _ op in
+  let eq0 := ZnZ.eq0 in
   let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in
   let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in
   fun m x y =>
@@ -464,13 +464,13 @@ Module Make (W0:CyclicType) <: NType.
  Definition wn_divn1 n :=
   let op := dom_op n in
   let zd := ZnZ.zdigits op in
-  let zero := @ZnZ.zero _ op in
-  let ww := @ZnZ.WW _ op in
-  let head0 := @ZnZ.head0 _ op in
-  let add_mul_div := @ZnZ.add_mul_div _ op in
-  let div21 := @ZnZ.div21 _ op in
-  let compare := @ZnZ.compare _ op in
-  let sub := @ZnZ.sub _ op in
+  let zero := ZnZ.zero in
+  let ww := ZnZ.WW in
+  let head0 := ZnZ.head0 in
+  let add_mul_div := ZnZ.add_mul_div in
+  let div21 := ZnZ.div21 in
+  let compare := ZnZ.compare in
+  let sub := ZnZ.sub in
   let ddivn1 :=
     DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
   fun m x y => let (u,v) := ddivn1 (S m) x y in (mk_t_w' n m u, mk_t n v).
@@ -633,12 +633,12 @@ Module Make (W0:CyclicType) <: NType.
  Definition wn_modn1 n :=
   let op := dom_op n in
   let zd := ZnZ.zdigits op in
-  let zero := @ZnZ.zero _ op in
-  let head0 := @ZnZ.head0 _ op in
-  let add_mul_div := @ZnZ.add_mul_div _ op in
-  let div21 := @ZnZ.div21 _ op in
-  let compare := @ZnZ.compare _ op in
-  let sub := @ZnZ.sub _ op in
+  let zero := ZnZ.zero in
+  let head0 := ZnZ.head0 in
+  let add_mul_div := ZnZ.add_mul_div in
+  let div21 := ZnZ.div21 in
+  let compare := ZnZ.compare in
+  let sub := ZnZ.sub in
   let dmodn1 :=
     DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in
   fun m x y => reduce n (dmodn1 (S m) x y).
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index b28ce15b9..8df4b7c64 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -324,8 +324,13 @@ pr "
 
  Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z.
  Proof.
-  do_size (destruct n; [exact ZnZ.spec_0|]).
-  destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0.
+   do_size (destruct n;
+            [match goal with
+             |- @eq Z (_ (zeron ?n)) _ => 
+               apply (ZnZ.spec_0 (Specs:=dom_spec n))
+             end|]).
+  destruct n; auto. simpl. rewrite make_op_S. fold word. 
+  apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))).
  Qed.
 
  (** * Digits *)
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 167be6d70..d9f4b0429 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -627,7 +627,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  assert (Hz := spec_irred_zero nx dy).
  assert (Hz':= spec_irred_zero ny dx).
  destruct irred as (n1,d1); destruct irred as (n2,d2).
- simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
+ simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
  rewrite spec_norm_denum.
  qsimpl.
 
@@ -665,7 +665,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  assert (Hgc := strong_spec_irred nx dy).
  assert (Hgc' := strong_spec_irred ny dx).
  destruct irred as (n1,d1); destruct irred as (n2,d2).
- simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
+ simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
 
  unfold norm_denum; qsimpl.
 
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index aed4fef05..22f3dcd64 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -375,7 +375,7 @@ Fixpoint gcdn (n : nat) (a b : positive) : positive :=
 Definition gcd (a b : positive) := gcdn (size_nat a + size_nat b)%nat a b.
 
 (** Generalized Gcd, also computing the division of a and b by the gcd *)
-
+Set Printing Universes.
 Fixpoint ggcdn (n : nat) (a b : positive) : (positive*(positive*positive)) :=
   match n with
     | O => (1,(a,b))
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 22436de69..ab1eccee2 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -15,6 +15,8 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
+Set Universe Polymorphism.
+
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
 Arguments id {A} x.
@@ -45,7 +47,7 @@ Definition const {A B} (a : A) := fun _ : B => a.
 
 (** The [flip] combinator reverses the first two arguments of a function. *)
 
-Definition flip {A B C} (f : A -> B -> C) x y := f y x.
+Monomorphic Definition flip {A B C} (f : A -> B -> C) x y := f y x.
 
 (** Application as a combinator. *)
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 323e80cc3..96345e154 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -263,7 +263,7 @@ Class DependentEliminationPackage (A : Type) :=
 
 Ltac elim_tac tac p :=
   let ty := type of p in
-  let eliminator := eval simpl in (elim (A:=ty)) in
+  let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in
     tac p eliminator.
 
 (** Specialization to do case analysis or induction.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index f6d795b94..d82fa602a 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -153,7 +153,7 @@ Section Fix_rects.
 
   Hypothesis equiv_lowers:
     forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)),
-    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) ->
+    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist (*FIXME shouldn't be needed *) (fun y => R y x0) x p')) ->
       f g = f h.
 
   (* From equiv_lowers, it follows that
@@ -231,10 +231,10 @@ Module WfExtensionality.
   Program Lemma fix_sub_eq_ext :
     forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
       (P : A -> Type)
-      (F_sub : forall x : A, (forall y:{y : A | R y x}, P y) -> P x),
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (` y)) -> P x),
       forall x : A,
         Fix_sub A R Rwf P F_sub x =
-          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub y).
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)).
   Proof.
     intros ; apply Fix_eq ; auto.
     intros.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index e395e4d03..e777c74d3 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -460,13 +460,13 @@ Proof.
   induction n; simpl; auto with qarith.
   rewrite IHn; auto with qarith.
 Qed.
-
+Transparent Qred.
 Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
 Proof.
   destruct n; simpl.
   destruct 1; auto.
   intros.
-  now apply Qc_is_canon.
+  now apply Qc_is_canon. 
 Qed.
 
 Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 4a826f691..f363fd7c2 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -167,14 +167,13 @@ Qed.
 
 Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R.
 Proof.
-unfold Qinv, Q2R, Qeq; intros (x1, x2); unfold Qden, Qnum.
-case x1.
+unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden.
 simpl; intros; elim H; trivial.
-intros; field; auto.
+intros; field; auto. 
 intros;
   change (IZR (Zneg x2)) with (- IZR (' x2))%R;
   change (IZR (Zneg p)) with (- IZR (' p))%R;
-  field; (*auto 8 with real.*)
+  simpl; field; (*auto 8 with real.*)
   repeat split; auto; auto with real.
 Qed.
 
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 3c15a3053..b2d9c749f 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -442,7 +442,7 @@ Proof.
   apply (Rabs_pos_lt _ H0).
   ring.
   assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro.
-  intro; rewrite <- H7; unfold dist, R_met; unfold R_dist;
+  intro; rewrite <- H7. unfold R_met, dist; unfold R_dist;
     unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0;
       apply Rabs_pos_lt.
   unfold Rdiv; apply prod_neq_R0;
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index d876b5d8e..0614f3998 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -695,7 +695,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
        exists deltatemp ; exact Htemp.
     elim (Hf_deriv eps eps_pos).
     intros deltatemp Htemp.
-     red in Hlinv ; red in Hlinv ; simpl dist in Hlinv ; unfold R_dist in Hlinv.
+     red in Hlinv ; red in Hlinv ; unfold dist in Hlinv ; unfold R_dist in Hlinv.
      assert (Hlinv' := Hlinv (fun h => (f (y+h) - f y)/h) (fun h => h <>0) l 0).
      unfold limit1_in, limit_in, dist in Hlinv' ; simpl in Hlinv'. unfold R_dist in Hlinv'.
      assert (Premisse : (forall eps : R,
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 658ffd12f..3d52a98cd 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -164,7 +164,7 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X')
     eps > 0 ->
     exists alp : R,
       alp > 0 /\
-      (forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps).
+      (forall x:Base X, D x /\ X.(dist) x x0 < alp -> X'.(dist) (f x) l < eps).
 
 (*******************************)
 (** **  R is a metric space    *)
@@ -191,9 +191,9 @@ Lemma tech_limit :
 Proof.
   intros f D l x0 H H0.
   case (Rabs_pos (f x0 - l)); intros H1.
-  absurd (dist R_met (f x0) l < dist R_met (f x0) l).
+  absurd (R_met.(@dist) (f x0) l < R_met.(@dist) (f x0) l).
   apply Rlt_irrefl.
-  case (H0 (dist R_met (f x0) l)); auto.
+  case (H0 (R_met.(@dist) (f x0) l)); auto.
   intros alpha1 [H2 H3]; apply H3; auto; split; auto.
   case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto.
   case (dist_refl R_met (f x0) l); intros Hr1 Hr2; symmetry; auto.
@@ -345,8 +345,9 @@ Lemma single_limit :
     adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'.
 Proof.
   unfold limit1_in; unfold limit_in; intros.
+  simpl in *.
   cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps).
-  clear H0 H1; unfold dist; unfold R_met; unfold R_dist;
+  clear H0 H1; simpl @dist; unfold R_met; unfold R_dist, dist;
     unfold Rabs; case (Rcase_abs (l - l')); intros.
   cut (forall eps:R, eps > 0 -> - (l - l') < eps).
   intro; generalize (prop_eps (- (l - l')) H1); intro;
@@ -356,7 +357,7 @@ Proof.
   intros; cut (eps * / 2 > 0).
   intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2));
     rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2).
-  elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial.
+  elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. 
   apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro;
     unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3);
       intro; elim (Rplus_ne 1); intros a b; rewrite a in H4;
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index f05539379..7e020dd41 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -339,7 +339,7 @@ Proof.
   unfold neighbourhood in H4; elim H4; intros del H5.
   exists (pos del); split.
   apply (cond_pos del).
-  intros; unfold included in H5; apply H5; elim H6; intros; apply H8.
+  intros. unfold included in H5; apply H5; elim H6; intros; apply H8.
   unfold disc; unfold Rminus; rewrite Rplus_opp_r;
     rewrite Rabs_R0; apply H0.
   apply disc_P1.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 5140c29c1..6ff3fa8b8 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -361,7 +361,7 @@ Proof with trivial.
   replace (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n) with
   (sum_f_R0 (fun k:nat => An k * Bn k) n +
     sum_f_R0 (fun k:nat => An k * - l) n)...
-  rewrite <- (scal_sum An n (- l)); field...
+  rewrite <- (scal_sum An n (- l)); field... 
   rewrite <- plus_sum; apply sum_eq; intros; ring...
 Qed.
 
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 058eec3da..5ab6f3824 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -32,9 +32,9 @@ Section Bounds.
   Variable U : Type.
   Variable D : PO U.
 
-  Let C := Carrier_of U D.
+  Let C := @Carrier_of U D.
 
-  Let R := Rel_of U D.
+  Let R := @Rel_of U D.
 
   Inductive Upper_Bound (B:Ensemble U) (x:U) : Prop :=
     Upper_Bound_definition :
@@ -103,6 +103,6 @@ Section Specific_orders.
 
   Record Chain : Type := Definition_of_chain
     {PO_of_chain : PO U;
-    Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
+    Chain_cond : Totally_ordered U PO_of_chain (@Carrier_of _ PO_of_chain)}.
 
 End Specific_orders.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 054164da5..8d97e3208 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -61,7 +61,7 @@ Section Partial_order_facts.
 
   Lemma Strict_Rel_Transitive_with_Rel :
     forall x y z:U,
-      Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
+      Strict_Rel_of U D x y -> @Rel_of U D y z -> Strict_Rel_of U D x z.
   Proof.
     unfold Strict_Rel_of at 1.
     red.
@@ -77,7 +77,7 @@ Section Partial_order_facts.
 
   Lemma Strict_Rel_Transitive_with_Rel_left :
     forall x y z:U,
-      Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
+      @Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
   Proof.
     unfold Strict_Rel_of at 1.
     red.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index acad98e5f..899acfc64 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -16,6 +16,7 @@
 Require Import List Setoid Compare_dec Morphisms FinFun.
 Import ListNotations. (* For notations [] and [a;b;c] *)
 Set Implicit Arguments.
+Set Universe Polymorphism.
 
 Section Permutation.
 
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 03952c95a..a89b90238 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -20,6 +20,8 @@
 
 Require Import List Relations Relations_1.
 
+Set Universe Polymorphism.
+
 (** Preambule *)
 
 Set Implicit Arguments.
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 79e817717..f85222dfb 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -80,13 +80,13 @@ Module KeyDecidableType(D:DecidableType).
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
-    unfold eqke; induction 1; intuition.
+    unfold eqke; induction 1; intuition. 
   Qed.
   Hint Resolve InA_eqke_eqk.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
-   intros; apply InA_eqA with p; auto with *.
+   intros; apply InA_eqA with p; auto with *. 
   Qed.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index eb5373859..747d03f8a 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -126,14 +126,14 @@ Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
       [EqualityType] and [DecidableType] *)
 
 Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
- Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
- Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
- Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
+ Definition eq_refl := F.eq_equiv.(@Equivalence_Reflexive _ _). 
+ Definition eq_sym := F.eq_equiv.(@Equivalence_Symmetric _ _).
+ Definition eq_trans := F.eq_equiv.(@Equivalence_Transitive _ _).
 End BackportEq.
 
 Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
  Instance eq_equiv : Equivalence E.eq.
- Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
+ Proof. exact (Build_Equivalence _ F.eq_refl F.eq_sym F.eq_trans). Qed.
 End UpdateEq.
 
 Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index ffd0649af..a0ee4caaa 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -440,7 +440,7 @@ Qed.
 
 Lemma max_min_antimono f :
  Proper (eq==>eq) f ->
- Proper (le==>inverse le) f ->
+ Proper (le==>flip le) f ->
  forall x y, max (f x) (f y) == f (min x y).
 Proof.
  intros Eqf Lef x y.
@@ -452,7 +452,7 @@ Qed.
 
 Lemma min_max_antimono f :
  Proper (eq==>eq) f ->
- Proper (le==>inverse le) f ->
+ Proper (le==>flip le) f ->
  forall x y, min (f x) (f y) == f (max x y).
 Proof.
  intros Eqf Lef x y.
@@ -557,11 +557,11 @@ Module UsualMinMaxLogicalProperties
   forall x y, min (f x) (f y) = f (min x y).
  Proof. intros; apply min_mono; auto. congruence. Qed.
 
- Lemma min_max_antimonotone f : Proper (le ==> inverse le) f ->
+ Lemma min_max_antimonotone f : Proper (le ==> flip le) f ->
   forall x y, min (f x) (f y) = f (max x y).
  Proof. intros; apply min_max_antimono; auto. congruence. Qed.
 
- Lemma max_min_antimonotone f : Proper (le ==> inverse le) f ->
+ Lemma max_min_antimonotone f : Proper (le ==> flip le) f ->
   forall x y, max (f x) (f y) = f (min x y).
  Proof. intros; apply max_min_antimono; auto. congruence. Qed.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index fa08f9366..fb28e0cfc 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -328,7 +328,7 @@ Module KeyOrderedType(O:OrderedType).
   Proof. split; eauto. Qed.
 
   Global Instance ltk_strorder : StrictOrder ltk.
-  Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed.
+  Proof. constructor; eauto. intros x; apply (irreflexivity (fst x)). Qed.
 
   Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
   Proof.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 2e9c0cf56..88fbd8c11 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -31,7 +31,7 @@ Module Type CompareFacts (Import O:DecStrOrder').
 
  Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y.
  Proof.
- case compare_spec; intro H; split; try easy; intro LT;
+  case compare_spec; intro H; split; try easy; intro LT;
   contradict LT; rewrite H; apply irreflexivity.
  Qed.
 
@@ -90,7 +90,7 @@ Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull').
  Instance le_order : PartialOrder eq le.
  Proof. compute; iorder. Qed.
 
- Instance le_antisym : Antisymmetric _ eq le.
+ Instance le_antisym : Antisymmetric eq le.
  Proof. apply partial_order_antisym; auto with *. Qed.
 
  Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 68ffc379d..475a25a41 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -29,7 +29,7 @@ Set Implicit Arguments.
     [le x y -> le y z -> le x z].
 *)
 
-Inductive ord := OEQ | OLT | OLE.
+Inductive ord : Set := OEQ | OLT | OLE.
 Definition trans_ord o o' :=
  match o, o' with
  | OEQ, _ => o'
@@ -70,7 +70,7 @@ Lemma le_refl : forall x, x<=x.
 Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed.
 
 Lemma lt_irrefl : forall x, ~ x<x.
-Proof. intros; apply StrictOrder_Irreflexive. Qed.
+Proof. intros. apply StrictOrder_Irreflexive. Qed.
 
 (** Symmetry rules *)
 
@@ -100,8 +100,9 @@ Local Notation "#" := interp_ord.
 
 Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
 Proof.
-destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition;
- subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
+destruct o, o'; simpl; intros x y z;
+rewrite ?P.le_lteq; intuition auto;
+subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
 Qed.
 
 Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index f57726bea..1c4c16cc1 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -24,7 +24,7 @@ Inductive t : nat -> Set :=
 
 Section SCHEMES.
 Definition case0 P (p: t 0): P p :=
-  match p with | F1 | FS  _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
+  match p with | F1 | FS  _ => fun devil => False_rect (@IDProp) devil (* subterm !!! *) end.
 
 Definition caseS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 8f672deda..f12aa0b87 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -21,6 +21,8 @@ Require Vectors.Fin.
 Import EqNotations.
 Local Open Scope nat_scope.
 
+Set Universe Polymorphism.
+
 (**
 A vector is a list of size n whose elements belong to a set A. *)
 
@@ -43,10 +45,10 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  |@cons _ a 0 v =>
    match v with
      |nil _ => bas a
-     |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+     |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
    end
  |@cons _ a (S nn') v => rect a v (rectS_fix v)
- |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+ |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
  end.
 
 (** An induction scheme for 2 vectors of same length *)
@@ -60,13 +62,13 @@ match v1 as v1' in t _ n1
   |[] => fun v2 =>
      match v2 with
        |[] => bas
-       |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+       |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
      end
   |h1 :: t1 => fun v2 =>
     match v2 with
       |h2 :: t2 => fun t1' =>
         rect (rect2_fix t1' t2) h1 h2
-      |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+      |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
     end t1
 end.
 
@@ -74,7 +76,7 @@ end.
 Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
 match v with
   |[] => H
-  |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+  |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
 end.
 
 (** A vector of length [S _] is [cons] *)
@@ -82,7 +84,7 @@ Definition caseS {A} (P : forall {n}, t A (S n) -> Type)
   (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v :=
 match v with
   |h :: t => H h t
-  |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+  |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
 end.
 End SCHEMES.
 
@@ -245,11 +247,11 @@ fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A :=
 match v in t _ n0 return t C n0 -> A with
   |[] => fun w => match w with
     |[] => a
-    |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+    |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
   end
   |@cons _ vh vn vt => fun w => match w with
     |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt
-    |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+    |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
   end vt
 end.
 
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index ed2b56d1f..3e8c1175f 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -105,7 +105,7 @@ Proof.
 assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h).
   induction v0.
     now simpl.
-    intros; simpl. rewrite<- IHv0. now f_equal.
+    intros; simpl. rewrite<- IHv0, assoc. now f_equal.
   induction v.
     reflexivity.
     simpl. intros; now rewrite<- (IHv).
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 24f5d308a..28288c0cb 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -130,7 +130,7 @@ Section Wf_Lexicographic_Exponentiation.
     match goal with [ |- clos_refl_trans ?A ?R ?x ?y ] => cut (clos_refl A R x y) end.
     intros; inversion H8; subst; [apply rt_step|apply rt_refl]; assumption.
     generalize H1.
-    rewrite H4; intro.
+    setoid_rewrite H4; intro.
 
     generalize (app_inj_tail _ _ _ _ H8); simple induction 1.
     intros.
@@ -182,7 +182,8 @@ Section Wf_Lexicographic_Exponentiation.
           Descl x0 /\ Descl y0).
 
     intro.
-    generalize (app_nil_end x1); simple induction 1; simple induction 1.
+    generalize (app_nil_end x1).
+    simple induction 1; simple induction 1. 
     split. apply d_conc; auto with sets.
 
     apply d_nil.
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 3935e1248..f1bfb027f 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -151,9 +151,7 @@ Section Efficient_Rec.
     forall P:Z -> Prop,
       (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
       forall x:Z, 0 <= x -> P x.
-  Proof.
-    exact Zlt_0_rec.
-  Qed.
+  Proof. intros; now apply Zlt_0_rec. Qed.
 
   (** Obsolete version of [Z.lt] induction principle on non-negative numbers *)
 
@@ -170,7 +168,7 @@ Section Efficient_Rec.
       (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
       forall x:Z, 0 <= x -> P x.
   Proof.
-    exact Z_lt_rec.
+    intros; now apply Z_lt_rec.
   Qed.
 
   (** An even more general induction principle using [Z.lt]. *)
@@ -196,7 +194,7 @@ Section Efficient_Rec.
       (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) ->
       forall x:Z, z <= x -> P x.
   Proof.
-    exact Zlt_lower_bound_rec.
+    intros; now apply Zlt_lower_bound_rec with z.
   Qed.
 
 End Efficient_Rec.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index b4163ef99..a5e710504 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -53,10 +53,11 @@ Theorem Z_lt_abs_rec :
     forall n:Z, P n.
 Proof.
   intros P HP p.
-  set (Q := fun z => 0 <= z -> P z * P (- z)) in *.
-  cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ].
-  elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
-  unfold Q; clear Q; intros.
+  set (Q := fun z => 0 <= z -> P z * P (- z)).
+  cut (Q (Z.abs p)); [ intros H | apply (Z_lt_rec Q); auto with zarith ].
+  elim (Zabs_dec p); intro eq; rewrite eq;
+    elim H; auto with zarith.
+  intros x H; subst Q. 
   split; apply HP.
   rewrite Z.abs_eq; auto; intros.
   elim (H (Z.abs m)); intros; auto with zarith.