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

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

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

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

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

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

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

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

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

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

Forgot to git add those files.

interp_constr returns the universe context

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

Merge with latest trunk + fixes

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

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

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

Correct classes/structures universe inference

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

Fix unification of universe variables.

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

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

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

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

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

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

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

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

Fix after rebase.

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

Refine printing of universe contexts

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

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

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

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

Adapt auto hints to polymorphic references.

Really produce polymorphic hints... second try

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

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

Fix erroneous shadowing of sigma variable.

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

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

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

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

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

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

Correct polymorphic discharge of section variables.

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

Fix r2l rewrite scheme to support universe polymorphism

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

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

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

Wrong sigma used in leibniz_rewrite

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

Make coercions work with universe polymorphic projections.

Fix eronneous bound in universes constraint solving.

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

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

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

More putting things into modules.

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

Fix congruence, eq_constr implem, discharge of polymorphic inductives.

Fix merge in auto.

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

Add -parameters-matter to coqc

Do compute the param levels at elaboration time if parameters_matter.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Handle selective Polymorphic/Monomorphic flag right for records.

Remove leftover command

Fix after update with latest trunk.

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

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

Forgot one part of the last patch on coercions.

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

Use leq_univ_poly in evarconv to avoid fixing universes.

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

Fix SearchAbout bug (issue #10).

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

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

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

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

- Move from universe_level_subst to universe_subst everywhere.

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

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

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

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

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

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

Test global universe equality early during simplication of constraints.

Better hashconsing, but still not good on universe lists.

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

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

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

Fix after merge

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

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

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

Fix after rebase with trunk

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

Proper sharing of lower bounds with fixed universes.

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

Constraints were not enforced in compilation of cases

Fix after rebase with trunk

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

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

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

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

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

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

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

Fixes in inductiveops, evarutil.

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

Fixes in tacinterp not propagating evars correctly.

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

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

Move from universe inference to universe checking in the kernel.

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

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

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

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

Moved kernel to universe checking only.

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

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

Remove libtypes.ml

Fix after merge.

Fix after rebase with trunk.

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

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

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

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

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

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

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

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

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

Fixes after rebase with trunk (esp. reductionops).

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

Proper expansion of projections during unification.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Add interface file for fast_typeops

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

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

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

First step at compatibility layer for projections.

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

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

Backport changes from HoTT/coq:

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

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

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

1 files changed, 1151 insertions, 780 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ae73d7a41e..83cb15f47e 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Names
+open Pp
 open Errors
 open Util
 open Nameops
@@ -32,91 +34,86 @@ open Decl_kinds
 open Elimschemes
 open Goal
 open Environ
-open Pp
-open Names
 open Tacinterp
 open Termops
+open Genarg
+open Extraargs
+open Pcoq.Constr
 open Entries
 open Libnames
+open Evarutil
 
 (** Typeclass-based generalized rewriting. *)
 
 (** Constants used by the tactic. *)
 
 let classes_dirpath =
-  DirPath.make (List.map Id.of_string ["Classes";"Coq"])
+  Names.DirPath.make (List.map Id.of_string ["Classes";"Coq"])
 
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
   else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
 
-let get_class str =
-  let qualid = Qualid (Loc.ghost, qualid_of_string str) in
-    lazy (class_info (Nametab.global qualid))
-
-let proper_class = get_class "Coq.Classes.Morphisms.Proper"
-let proper_proxy_class = get_class "Coq.Classes.Morphisms.ProperProxy"
-
-let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
-
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
 let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
     Nametab.global_of_path sp
 
-let try_find_reference dir s =
-  constr_of_global (try_find_global_reference dir s)
+let find_reference dir s =
+  let gr = lazy (try_find_global_reference dir s) in
+    fun () -> Lazy.force gr
 
-let gen_constant dir s = Coqlib.gen_constant "rewrite" dir s
-let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq")
-let coq_f_equal = lazy (gen_constant ["Init"; "Logic"] "f_equal")
-let coq_all = lazy (gen_constant ["Init"; "Logic"] "all")
-let coq_forall = lazy (gen_constant ["Classes"; "Morphisms"] "forall_def")
-let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
-let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
+type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 
-let reflexive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Reflexive")
-let reflexive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "reflexivity")
+let find_global dir s =
+  let gr = lazy (try_find_global_reference dir s) in
+    fun (evd,cstrs) -> 
+      let evd, c = Evarutil.new_global evd (Lazy.force gr) in
+	(evd, cstrs), c
 
-let symmetric_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Symmetric")
-let symmetric_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "symmetry")
+(** Utility for dealing with polymorphic applications *)
 
-let transitive_type = lazy (try_find_reference ["Classes"; "RelationClasses"] "Transitive")
-let transitive_proof = lazy (try_find_reference ["Classes"; "RelationClasses"] "transitivity")
+let app_poly evars f args =
+  let evars, fc = f evars in
+    evars, mkApp (fc, args)
 
-let coq_inverse = lazy (gen_constant ["Program"; "Basics"] "flip")
+let e_app_poly evars f args =
+  let evars', c = app_poly !evars f args in
+    evars := evars';
+    c
 
-let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |])
+(** Global constants. *)
 
-let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation")
-let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation")
-let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
-let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation")
-let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation")
-let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation")
-let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation")
-let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
-let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
-let rewrite_relation_class = lazy (gen_constant ["Classes"; "RelationClasses"] "RewriteRelation")
+let gen_reference dir s = Coqlib.gen_reference "rewrite" dir s
+let coq_eq_ref = find_reference ["Init"; "Logic"] "eq"
+let coq_eq = find_global ["Init"; "Logic"] "eq"
+let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
+let coq_all = find_global ["Init"; "Logic"] "all"
+let impl = find_global ["Program"; "Basics"] "impl"
+let arrow = find_global ["Program"; "Basics"] "arrow"
+let coq_inverse = find_global ["Program"; "Basics"] "flip"
 
-let proper_type = lazy (constr_of_global (Lazy.force proper_class).cl_impl)
-let proper_proxy_type = lazy (constr_of_global (Lazy.force proper_proxy_class).cl_impl)
+(* let coq_inverse = lazy (gen_constant ["Program"; "Basics"] "flip") *)
 
-(** Utility functions *)
+(* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |]) *)
 
-let split_head = function
-    hd :: tl -> hd, tl
-  | [] -> assert(false)
+(* let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation") *)
+(* let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation") *)
+(* let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") *)
+(* let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation") *)
+(* let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation") *)
+(* let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation") *)
+(* let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation") *)
+(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
+(* let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) *)
 
-let evd_convertible env evd x y =
-  try ignore(Evarconv.the_conv_x env x y evd); true
-  with e when Errors.noncritical e -> false
+(* let proper_type = lazy (Universes.constr_of_global (Lazy.force proper_class).cl_impl) *)
+(* let proper_proxy_type = lazy (Universes.constr_of_global (Lazy.force proper_proxy_class).cl_impl) *)
 
-let convertible env evd x y =
-  Reductionops.is_conv env evd x y
 
-(** Bookkeeping which evars are constraints so that we can
+
+(** Bookkeeping which evars are constraints so that we can 
     remove them at the end of the tactic. *)
 
 let goalevars evars = fst evars
@@ -127,10 +124,17 @@ let new_cstr_evar (evd,cstrs) env t =
     (evd', Evar.Set.add (fst (destEvar t)) cstrs), t
 
 (** Building or looking up instances. *)
+let e_new_cstr_evar evars env t =
+  let evd', t = new_cstr_evar !evars env t in evars := evd'; t
+
+let new_goal_evar (evd,cstrs) env t =
+  let evd', t = Evarutil.new_evar evd env t in
+    (evd', cstrs), t
+
+let e_new_goal_evar evars env t =
+  let evd', t = new_goal_evar !evars env t in evars := evd'; t
 
-let proper_proof env evars carrier relation x =
-  let goal = mkApp (Lazy.force proper_proxy_type, [| carrier ; relation; x |])
-  in new_cstr_evar evars env goal
+(** Building or looking up instances. *)
 
 let extends_undefined evars evars' =
   let f ev evi found = found || not (Evd.mem evars ev)
@@ -138,95 +142,328 @@ let extends_undefined evars evars' =
 
 let find_class_proof proof_type proof_method env evars carrier relation =
   try
-    let goal = mkApp (Lazy.force proof_type, [| carrier ; relation |]) in
-    let evars', c = Typeclasses.resolve_one_typeclass env evars goal in
-      if extends_undefined evars evars' then raise Not_found
-      else mkApp (Lazy.force proof_method, [| carrier; relation; c |])
+    let evars, goal = app_poly evars proof_type [| carrier ; relation |] in
+    let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in
+      if extends_undefined (goalevars evars) evars' then raise Not_found
+      else app_poly (evars',cstrevars evars) proof_method [| carrier; relation; c |]
   with e when Logic.catchable_exception e -> raise Not_found
+ 
+(** Utility functions *)
 
-let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
-let get_symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
-let get_transitive_proof env = find_class_proof transitive_type transitive_proof env
-
-(** Build an infered signature from constraints on the arguments and expected output
-    relation *)
-
-let build_signature evars env m (cstrs : (types * types option) option list)
-    (finalcstr : (types * types option) option) =
-  let mk_relty evars newenv ty obj =
-    match obj with
+module GlobalBindings (M : sig
+  val relation_classes : string list
+  val morphisms : string list
+  val relation : string list * string
+end) = struct
+  open M
+  let relation : evars -> evars * constr = find_global (fst relation) (snd relation)
+
+  let reflexive_type = find_global relation_classes "Reflexive"
+  let reflexive_proof = find_global relation_classes "reflexivity"
+    
+  let symmetric_type = find_global relation_classes "Symmetric"
+  let symmetric_proof = find_global relation_classes "symmetry"
+
+  let transitive_type = find_global relation_classes "Transitive"
+  let transitive_proof = find_global relation_classes "transitivity"
+
+  let forall_relation = find_global morphisms "forall_relation"
+  let pointwise_relation = find_global morphisms "pointwise_relation"
+
+  let forall_relation_ref = find_reference morphisms "forall_relation"
+  let pointwise_relation_ref = find_reference morphisms "pointwise_relation"
+
+  let respectful = find_global morphisms "respectful"
+  let respectful_ref = find_reference morphisms "respectful"
+
+  let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation"
+
+  let coq_forall = find_global morphisms "forall_def"
+
+  let subrelation = find_global relation_classes "subrelation"
+  let do_subrelation = find_global morphisms "do_subrelation"
+  let apply_subrelation = find_global morphisms "apply_subrelation"
+
+  let rewrite_relation_class = find_global relation_classes "RewriteRelation"
+
+  let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper"))
+  let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy"))
+    
+  let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
+    
+  let proper_type = 
+    let l = lazy (Lazy.force proper_class).cl_impl in
+      fun (evd,cstrs) -> 
+	let evd, c = Evarutil.new_global evd (Lazy.force l) in
+	  (evd, cstrs), c
+	
+  let proper_proxy_type = 
+    let l = lazy (Lazy.force proper_proxy_class).cl_impl in
+      fun (evd,cstrs) -> 
+	let evd, c = Evarutil.new_global evd (Lazy.force l) in
+	  (evd, cstrs), c
+
+  let proper_proof env evars carrier relation x =
+    let evars, goal = app_poly evars proper_proxy_type [| carrier ; relation; x |] in
+      new_cstr_evar evars env goal
+
+  let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
+  let get_symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
+  let get_transitive_proof env = find_class_proof transitive_type transitive_proof env
+
+  let mk_relation evd a = 
+    app_poly evd relation [| a |]
+
+  (** Build an infered signature from constraints on the arguments and expected output
+      relation *)
+    
+  let build_signature evars env m (cstrs : (types * types option) option list)
+      (finalcstr : (types * types option) option) =
+    let mk_relty evars newenv ty obj =
+      match obj with
       | None | Some (_, None) ->
-	  let relty = mk_relation ty in
-	    if closed0 ty then
-	      let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
-		new_cstr_evar evars env' relty
-	    else new_cstr_evar evars newenv relty
+	let evars, relty = mk_relation evars ty in
+	  if closed0 ty then 
+	    let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
+	      new_cstr_evar evars env' relty
+	  else new_cstr_evar evars newenv relty
       | Some (x, Some rel) -> evars, rel
-  in
-  let rec aux env evars ty l =
-    let t = Reductionops.whd_betadeltaiota env (fst evars) ty in
-      match kind_of_term t, l with
-      | Prod (na, ty, b), obj :: cstrs ->
+    in
+    let rec aux env evars ty l =
+      let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in
+	match kind_of_term t, l with
+	| Prod (na, ty, b), obj :: cstrs ->
 	  if noccurn 1 b (* non-dependent product *) then
-	    let ty = Reductionops.nf_betaiota (fst evars) ty in
+	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let evars, relty = mk_relty evars env ty obj in
-	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
+	    let evars, newarg = app_poly evars respectful [| ty ; b' ; relty ; arg |] in
 	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
 	  else
-	    let (evars, b, arg, cstrs) = aux (Environ.push_rel (na, None, ty) env) evars b cstrs in
-	    let ty = Reductionops.nf_betaiota (fst evars) ty in
+	    let (evars, b, arg, cstrs) = 
+	      aux (Environ.push_rel (na, None, ty) env) evars b cstrs 
+	    in
+	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
 	    let pred = mkLambda (na, ty, b) in
 	    let liftarg = mkLambda (na, ty, arg) in
-	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
+	    let evars, arg' = app_poly evars forall_relation [| ty ; pred ; liftarg |] in
 	      if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
 	      else error "build_signature: no constraint can apply on a dependent argument"
-      | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
-      | _, [] ->
+	| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
+	| _, [] ->
 	  (match finalcstr with
 	  | None | Some (_, None) ->
-	      let t = Reductionops.nf_betaiota (fst evars) ty in
-	      let evars, rel = mk_relty evars env t None in
-		evars, t, rel, [t, Some rel]
+	    let t = Reductionops.nf_betaiota (fst evars) ty in
+	    let evars, rel = mk_relty evars env t None in
+	      evars, t, rel, [t, Some rel]
 	  | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
-  in aux env evars m cstrs
+    in aux env evars m cstrs
 
-type hypinfo = {
-  cl : clausenv;
-  ext : Evar.Set.t; (* New evars in this clausenv *)
-  prf : constr;
-  car : constr;
-  rel : constr;
-  c1 : constr;
-  c2 : constr;
-  c  : (Tacinterp.interp_sign * Tacexpr.glob_constr_and_expr with_bindings) option;
-  abs : bool;
-}
+  (** Folding/unfolding of the tactic constants. *)
+
+  let unfold_impl t =
+    match kind_of_term t with
+    | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) ->
+      mkProd (Anonymous, a, lift 1 b)
+    | _ -> assert false
+
+  let unfold_all t =
+    match kind_of_term t with
+    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
+      (match kind_of_term b with
+      | Lambda (n, ty, b) -> mkProd (n, ty, b)
+      | _ -> assert false)
+    | _ -> assert false
+
+  let unfold_forall t =
+    match kind_of_term t with
+    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
+      (match kind_of_term b with
+      | Lambda (n, ty, b) -> mkProd (n, ty, b)
+      | _ -> assert false)
+    | _ -> assert false
+
+  let arrow_morphism evd ta tb a b =
+    let ap = is_Prop ta and bp = is_Prop tb in
+      if ap && bp then app_poly evd impl [| a; b |], unfold_impl
+      else if ap then (* Domain in Prop, CoDomain in Type *)
+	(evd, mkProd (Anonymous, a, b)), (fun x -> x)
+      else if bp then (* Dummy forall *)
+	(app_poly evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall
+      else (* None in Prop, use arrow *)
+	(app_poly evd arrow [| a; b |]), unfold_impl
+
+  let rec decomp_pointwise n c =
+    if Int.equal n 0 then c
+    else
+      match kind_of_term c with
+      | App (f, [| a; b; relb |]) when Globnames.is_global (pointwise_relation_ref ()) f ->
+	decomp_pointwise (pred n) relb
+      | App (f, [| a; b; arelb |]) when Globnames.is_global (forall_relation_ref ()) f ->
+	decomp_pointwise (pred n) (Reductionops.beta_applist (arelb, [mkRel 1]))
+      | _ -> invalid_arg "decomp_pointwise"
+
+  let rec apply_pointwise rel = function
+    | arg :: args ->
+      (match kind_of_term rel with
+      | App (f, [| a; b; relb |]) when Globnames.is_global (pointwise_relation_ref ()) f ->
+	apply_pointwise relb args
+      | App (f, [| a; b; arelb |]) when Globnames.is_global (forall_relation_ref ()) f ->
+	apply_pointwise (Reductionops.beta_applist (arelb, [arg])) args
+      | _ -> invalid_arg "apply_pointwise")
+    | [] -> rel
+
+  let pointwise_or_dep_relation evd n t car rel =
+    if noccurn 1 car && noccurn 1 rel then
+      app_poly evd pointwise_relation [| t; lift (-1) car; lift (-1) rel |]
+    else
+      app_poly evd forall_relation
+	[| t; mkLambda (n, t, car); mkLambda (n, t, rel) |]
+
+  let lift_cstr env evars (args : constr list) c ty cstr =
+    let start evars env car =
+      match cstr with
+      | None | Some (_, None) -> 
+	let evars, rel = mk_relation evars car in
+	  new_cstr_evar evars env rel
+      | Some (ty, Some rel) -> evars, rel
+    in
+    let rec aux evars env prod n = 
+      if Int.equal n 0 then start evars env prod
+      else
+	match kind_of_term (Reduction.whd_betadeltaiota env prod) with
+	| Prod (na, ty, b) ->
+	  if noccurn 1 b then
+	    let b' = lift (-1) b in
+	    let evars, rb = aux evars env b' (pred n) in
+	      app_poly evars pointwise_relation [| ty; b'; rb |]
+	  else
+	    let evars, rb = aux evars (Environ.push_rel (na, None, ty) env) b (pred n) in
+	      app_poly evars forall_relation
+		[| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
+	| _ -> raise Not_found
+    in 
+    let rec find env c ty = function
+      | [] -> None
+      | arg :: args ->
+	try let evars, found = aux evars env ty (succ (List.length args)) in
+	      Some (evars, found, c, ty, arg :: args)
+	with Not_found ->
+	  find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args
+    in find env c ty args
+
+  let unlift_cstr env sigma = function
+    | None -> None
+    | Some codom -> Some (decomp_pointwise 1 codom)
+
+end
+
+(* let my_type_of env evars c = Typing.e_type_of env evars c *)
+(* let mytypeofkey = Profile.declare_profile "my_type_of";; *)
+(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *)
+
+
+let type_app_poly env evd f args =
+  let evars, c = app_poly evd f args in
+  let evd', t = Typing.e_type_of env (goalevars evars) c in
+    (evd', cstrevars evars), c
+
+module PropGlobal = struct
+  module Consts =
+  struct 
+    let relation_classes = ["Classes"; "RelationClasses"]
+    let morphisms = ["Classes"; "Morphisms"]
+    let relation = ["Relations";"Relation_Definitions"], "relation"
+  end
+
+  module G = GlobalBindings(Consts)
+
+  include G
+  include Consts
+  let inverse env evd car rel = 
+    type_app_poly env evd coq_inverse [| car ; car; mkProp; rel |]
+      (* app_poly evd coq_inverse [| car ; car; mkProp; rel |] *)
+
+end
+
+module TypeGlobal = struct
+  module Consts = 
+    struct 
+      let relation_classes = ["Classes"; "CRelationClasses"]
+      let morphisms = ["Classes"; "CMorphisms"]
+      let relation = relation_classes, "crelation"
+    end
+
+  module G = GlobalBindings(Consts)
+  include G
+
+
+  let inverse env (evd,cstrs) car rel = 
+    let evd, (sort,_) = Evarutil.new_type_evar Evd.univ_flexible evd env in
+      app_poly (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
+
+end
+
+let sort_of_rel env evm rel =
+  Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel)
 
 (** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
 let is_applied_rewrite_relation env sigma rels t =
   match kind_of_term t with
   | App (c, args) when Array.length args >= 2 ->
       let head = if isApp c then fst (destApp c) else c in
-	if eq_constr (Lazy.force coq_eq) head then None
+	if Globnames.is_global (coq_eq_ref ()) head then None
 	else
 	  (try
 	      let params, args = Array.chop (Array.length args - 2) args in
 	      let env' = Environ.push_rel_context rels env in
-	      let evd, evar = Evarutil.new_evar sigma env' (new_Type ()) in
-	      let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in
-	      let _ = Typeclasses.resolve_one_typeclass env' evd inst in
+	      let evars, (evar, _) = Evarutil.new_type_evar Evd.univ_flexible sigma env' in
+	      let evars, inst = 
+		app_poly (evars,Evar.Set.empty)
+		  TypeGlobal.rewrite_relation_class [| evar; mkApp (c, params) |] in
+	      let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
 		Some (it_mkProd_or_LetIn t rels)
 	  with e when Errors.noncritical e -> None)
   | _ -> None
 
-let rec decompose_app_rel env evd t =
+(* let _ = *)
+(*   Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation *)
+
+let split_head = function
+    hd :: tl -> hd, tl
+  | [] -> assert(false)
+
+let evd_convertible env evd x y =
+  try ignore(Evarconv.the_conv_x env x y evd); true
+  with e when Errors.noncritical e -> false
+
+let convertible env evd x y =
+  Reductionops.is_conv env evd x y
+
+type hypinfo = {
+  cl : clausenv;
+  prf : constr;
+  car : constr;
+  rel : constr;
+  sort : bool; (* true = Prop; false = Type *)
+  l2r : bool;
+  c1 : constr;
+  c2 : constr;
+  c  : (Tacinterp.interp_sign * Tacexpr.glob_constr_and_expr with_bindings) option;
+  abs : (constr * types) option;
+  flags : Unification.unify_flags;
+}
+
+let get_symmetric_proof b = 
+  if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
+
+let rec decompose_app_rel env evd t = 
   match kind_of_term t with
-  | App (f, args) ->
-      if Array.length args > 1 then
+  | App (f, args) -> 
+      if Array.length args > 1 then 
 	let fargs, args = Array.chop (Array.length args - 2) args in
 	  mkApp (f, fargs), args
-      else
+      else 
 	let (f', args) = decompose_app_rel env evd args.(0) in
 	let ty = Typing.type_of env evd args.(0) in
 	let f'' = mkLambda (Name (Id.of_string "x"), ty,
@@ -235,37 +472,46 @@ let rec decompose_app_rel env evd t =
 	in (f'', args)
   | _ -> error "The term provided is not an applied relation."
 
-let decompose_applied_relation env sigma orig (c,l) =
-  let ctype = Typing.type_of env sigma c in
+let decompose_applied_relation env origsigma sigma flags orig (c,l) left2right =
+  let c' = c in
+  let ctype = Typing.type_of env sigma c' in
   let find_rel ty =
-    let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c, ty) l in
+    let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c',ty) l in
     let (equiv, args) = decompose_app_rel env eqclause.evd (Clenv.clenv_type eqclause) in
-    let c1 = args.(0) and c2 = args.(1) in
+    let c1 = args.(0) and c2 = args.(1) in 
     let ty1, ty2 =
       Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
     in
       if not (evd_convertible env eqclause.evd ty1 ty2) then None
       else
+	let sort = sort_of_rel env eqclause.evd equiv in
 	let value = Clenv.clenv_value eqclause in
-	let ext = Evarutil.evars_of_term value in
-	  Some { cl=eqclause; ext=ext; prf=value;
-		 car=ty1; rel = equiv; c1=c1; c2=c2; c=orig; abs=false; }
+	let eqclause = { eqclause with evd = Evd.diff eqclause.evd origsigma } in
+	  Some { cl=eqclause; prf=value;
+		 car=ty1; rel = equiv; sort = Sorts.is_prop sort;
+		 l2r=left2right; c1=c1; c2=c2; c=orig; abs=None;
+		 flags = flags }
   in
     match find_rel ctype with
     | Some c -> c
     | None ->
-	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
-	match find_rel (it_mkProd_or_LetIn t' ctx) with
+	let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
+	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> n, None, t) ctx)) with
 	| Some c -> c
 	| None -> error "The term does not end with an applied homogeneous relation."
 
-let decompose_applied_relation_expr env sigma (is, (c,l)) =
-  let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
-  decompose_applied_relation env sigma (Some (is, (c,l))) cbl
+let decompose_applied_relation_expr env sigma flags (is, (c,l)) left2right =
+  let sigma', cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
+    decompose_applied_relation env sigma sigma' flags (Some (is, (c,l))) cbl left2right
+
+let rewrite_db = "rewrite"
 
-(** Hint database named "rewrite", now created directly in Auto *)
+let conv_transparent_state = (Id.Pred.empty, Cpred.full)
 
-let rewrite_db = Auto.rewrite_db
+let _ = 
+  Auto.add_auto_init
+    (fun () ->
+       Auto.create_hint_db false rewrite_db conv_transparent_state true)
 
 let rewrite_transparent_state () =
   Auto.Hint_db.transparent_state (Auto.searchtable_map rewrite_db)
@@ -288,10 +534,10 @@ let rewrite_unif_flags = {
 }
 
 let rewrite2_unif_flags =
-  {  Unification.modulo_conv_on_closed_terms = Some cst_full_transparent_state;
+  {  Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
      Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
      Unification.modulo_delta = empty_transparent_state;
-     Unification.modulo_delta_types = cst_full_transparent_state;
+     Unification.modulo_delta_types = conv_transparent_state;
      Unification.modulo_delta_in_merge = None;
      Unification.check_applied_meta_types = true;
      Unification.resolve_evars = false;
@@ -304,7 +550,7 @@ let rewrite2_unif_flags =
      Unification.allow_K_in_toplevel_higher_order_unification = true
   }
 
-let general_rewrite_unif_flags () =
+let general_rewrite_unif_flags () = 
   let ts = rewrite_transparent_state () in
     {  Unification.modulo_conv_on_closed_terms = Some ts;
        Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
@@ -322,13 +568,14 @@ let general_rewrite_unif_flags () =
        Unification.allow_K_in_toplevel_higher_order_unification = true }
 
 let refresh_hypinfo env sigma hypinfo =
-    let {c=c} = hypinfo in
+  if Option.is_empty hypinfo.abs then
+    let {l2r=l2r; c=c;cl=cl;flags=flags} = hypinfo in
       match c with
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    decompose_applied_relation_expr env sigma c
+	    decompose_applied_relation_expr env sigma flags c l2r;
 	| _ -> hypinfo
-
+  else hypinfo
 
 let solve_remaining_by by env prf =
   match by with
@@ -336,10 +583,10 @@ let solve_remaining_by by env prf =
   | Some tac ->
     let indep = clenv_independent env in
     let tac = eval_tactic tac in
-    let evd' =
+    let evd' = 
       List.fold_right (fun mv evd ->
         let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
-	let c,_ = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
+	let c,_,_ = Pfedit.build_by_tactic env.env (ty,Univ.ContextSet.empty) (Tacticals.New.tclCOMPLETE tac) in
 	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
       indep env.evd
     in { env with evd = evd' }, prf
@@ -352,35 +599,32 @@ let extend_evd sigma ext sigma' =
 let shrink_evd sigma ext =
   Evar.Set.fold (fun i acc -> Evd.remove acc i) ext sigma
 
-let no_constraints cstrs =
+let no_constraints cstrs = 
   fun ev _ -> not (Evar.Set.mem ev cstrs)
 
-let eq_env x y = x == y
+let poly_inverse sort =
+  if sort then PropGlobal.inverse else TypeGlobal.inverse
 
-let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
+let unify_eqn env (sigma, cstrs) hypinfo by t =
   if isEvar t then None
   else try
-    let hypinfo =
-      if hypinfo.abs || eq_env hypinfo.cl.env env then hypinfo
-      else refresh_hypinfo env sigma hypinfo
-    in
-    let {cl=cl; ext=ext; prf=prf; car=car; rel=rel; c1=c1; c2=c2; abs=abs} =
-      hypinfo in
+    let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = 
+      !hypinfo in
     let left = if l2r then c1 else c2 in
-    let evd' = Evd.evars_reset_evd ~with_conv_pbs:true sigma cl.evd in
-    let evd'' = extend_evd evd' ext cl.evd in
-    let cl = { cl with evd = evd'' } in
-    let hypinfo, evd', prf, c1, c2, car, rel =
-      if abs then
+    let evd' = Evd.merge sigma cl.evd in
+    let cl = { cl with evd = evd' } in
+    let evd', prf, c1, c2, car, rel =
+      match abs with
+      | Some (absprf, absprfty) ->
 	  let env' = clenv_unify ~flags:rewrite_unif_flags CONV left t cl in
-	    hypinfo, env'.evd, prf, c1, c2, car, rel
-      else
-	  let env' = clenv_unify ~flags CONV left t cl in
+	    env'.evd, prf, c1, c2, car, rel
+      | None ->
+	  let env' = clenv_unify ~flags:!hypinfo.flags CONV left t cl in
 	  let env' = Clenvtac.clenv_pose_dependent_evars true env' in
 	  let evd' = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
 	    ~fail:true env'.env env'.evd in
 	  let env' = { env' with evd = evd' } in
-	  let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in
+	  let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in	   
 	  let nf c = Evarutil.nf_evar env'.evd (Clenv.clenv_nf_meta env' c) in
 	  let c1 = nf c1 and c2 = nf c2
 	  and car = nf car and rel = nf rel
@@ -388,131 +632,41 @@ let unify_eqn l2r flags env (sigma, cstrs) hypinfo by t =
 	  let ty1 = Typing.type_of env'.env env'.evd c1
 	  and ty2 = Typing.type_of env'.env env'.evd c2
 	  in
-	    if convertible env env'.evd ty1 ty2 then
+	    if convertible env env'.evd ty1 ty2 then 
 	      (if occur_meta_or_existential prf then
-		let hypinfo = refresh_hypinfo env env'.evd hypinfo in
-		 (hypinfo, env'.evd, prf, c1, c2, car, rel)
+		(hypinfo := refresh_hypinfo env env'.evd !hypinfo;
+		 env'.evd, prf, c1, c2, car, rel)
 	       else (** Evars have been solved, we can go back to the initial evd,
 			but keep the potential refinement of existing evars. *)
-		let evd' = shrink_evd env'.evd ext in
-		  (hypinfo, evd', prf, c1, c2, car, rel))
+		  env'.evd, prf, c1, c2, car, rel)
 	    else raise Reduction.NotConvertible
     in
-    let res =
-      if l2r then (prf, (car, rel, c1, c2))
+    let evars = evd', Evar.Set.empty in
+    let evd, res =
+      if l2r then evars, (prf, (car, rel, c1, c2))
       else
-	try (mkApp (get_symmetric_proof env evd' car rel,
-		   [| c1 ; c2 ; prf |]),
-	    (car, rel, c2, c1))
+	try
+	  let evars, symprf = get_symmetric_proof !hypinfo.sort env evars car rel in
+	    evars, (mkApp (symprf, [| c1 ; c2 ; prf |]),
+		    (car, rel, c2, c1))
 	with Not_found ->
-	  (prf, (car, inverse car rel, c2, c1))
-    in Some (hypinfo, evd', res)
+	  let evars, rel' = poly_inverse !hypinfo.sort env evars car rel in
+	    evars, (prf, (car, rel', c2, c1))
+    in Some (evd, res)
   with e when Class_tactics.catchable e -> None
 
-let unfold_impl t =
-  match kind_of_term t with
-    | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) ->
-	mkProd (Anonymous, a, lift 1 b)
-    | _ -> assert false
-
-let unfold_all t =
-  match kind_of_term t with
-    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
-	(match kind_of_term b with
-	  | Lambda (n, ty, b) -> mkProd (n, ty, b)
-	  | _ -> assert false)
-    | _ -> assert false
-
-let unfold_forall t =
-  match kind_of_term t with
-    | App (id, [| a; b |]) (* when eq_constr id (Lazy.force coq_all) *) ->
-	(match kind_of_term b with
-	  | Lambda (n, ty, b) -> mkProd (n, ty, b)
-	  | _ -> assert false)
-    | _ -> assert false
-
-let arrow_morphism ta tb a b =
-  let ap = is_Prop ta and bp = is_Prop tb in
-    if ap && bp then mkApp (Lazy.force impl, [| a; b |]), unfold_impl
-    else if ap then (* Domain in Prop, CoDomain in Type *)
-      mkProd (Anonymous, a, b), (fun x -> x)
-    else if bp then (* Dummy forall *)
-      mkApp (Lazy.force coq_all, [| a; mkLambda (Anonymous, a, b) |]), unfold_forall
-    else (* None in Prop, use arrow *)
-      mkApp (Lazy.force arrow, [| a; b |]), unfold_impl
-
-let rec decomp_pointwise n c =
-  if Int.equal n 0 then c
-  else
-    match kind_of_term c with
-    | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) ->
-	decomp_pointwise (pred n) relb
-    | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) ->
-	decomp_pointwise (pred n) (Reductionops.beta_applist (arelb, [mkRel 1]))
-    | _ -> invalid_arg "decomp_pointwise"
-
-let rec apply_pointwise rel = function
-  | arg :: args ->
-      (match kind_of_term rel with
-      | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) ->
-	  apply_pointwise relb args
-      | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) ->
-	  apply_pointwise (Reductionops.beta_applist (arelb, [arg])) args
-      | _ -> invalid_arg "apply_pointwise")
-  | [] -> rel
-
-let pointwise_or_dep_relation n t car rel =
-  if noccurn 1 car && noccurn 1 rel then
-    mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |])
-  else
-    mkApp (Lazy.force forall_relation,
-	  [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |])
-
-let lift_cstr env evars (args : constr list) c ty cstr =
-  let start evars env car =
-    match cstr with
-    | None | Some (_, None) ->
-      new_cstr_evar evars env (mk_relation car)
-    | Some (ty, Some rel) -> evars, rel
-  in
-  let rec aux evars env prod n =
-    if Int.equal n 0 then start evars env prod
-    else
-      match kind_of_term (Reduction.whd_betadeltaiota env prod) with
-      | Prod (na, ty, b) ->
-	  if noccurn 1 b then
-	    let b' = lift (-1) b in
-	    let evars, rb = aux evars env b' (pred n) in
-	      evars, mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |])
-	  else
-	    let evars, rb = aux evars (Environ.push_rel (na, None, ty) env) b (pred n) in
-	      evars, mkApp (Lazy.force forall_relation,
-		    [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |])
-      | _ -> raise Not_found
-  in
-  let rec find env c ty = function
-    | [] -> None
-    | arg :: args ->
-	try let evars, found = aux evars env ty (succ (List.length args)) in
-	      Some (evars, found, c, ty, arg :: args)
-	with Not_found ->
-	  find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args
-  in find env c ty args
-
-let unlift_cstr env sigma = function
-  | None -> None
-  | Some codom -> Some (decomp_pointwise 1 codom)
-
 type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }
 
 let default_flags = { under_lambdas = true; on_morphisms = true; }
 
-type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
-
-type rewrite_proof =
+type rewrite_proof = 
   | RewPrf of constr * constr
   | RewCast of cast_kind
 
+let map_rewprf f p = match p with
+  | RewPrf (x, y) -> RewPrf (f x, f y)
+  | RewCast _ -> p
+
 let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
 
 type rewrite_result_info = {
@@ -523,34 +677,41 @@ type rewrite_result_info = {
   rew_evars : evars;
 }
 
-type 'a rewrite_result =
-| Fail
-| Same
-| Info of 'a
+type rewrite_result = rewrite_result_info option
 
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
-  constr option -> evars -> 'a * rewrite_result_info rewrite_result
+type strategy = Environ.env -> Id.t list -> constr -> types ->
+  (bool (* prop *) * constr option) -> evars -> rewrite_result option
 
-type strategy = unit pure_strategy
+let make_eq () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+let make_eq_refl () =
+(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+
+let get_rew_rel r = match r.rew_prf with
+  | RewPrf (rel, prf) -> rel
+  | RewCast c -> mkApp (make_eq (),[| r.rew_car; r.rew_from; r.rew_to |])
 
 let get_rew_prf r = match r.rew_prf with
-  | RewPrf (rel, prf) -> rel, prf
+  | RewPrf (rel, prf) -> rel, prf 
   | RewCast c ->
-    let rel = mkApp (Coqlib.build_coq_eq (), [| r.rew_car |]) in
-      rel, mkCast (mkApp (Coqlib.build_coq_eq_refl (), [| r.rew_car; r.rew_from |]),
+    let rel = mkApp (make_eq (), [| r.rew_car |]) in
+      rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]),
 		   c, mkApp (rel, [| r.rew_from; r.rew_to |]))
 
-let resolve_subrelation env avoid car rel prf rel' res =
+let poly_subrelation sort = 
+  if sort then PropGlobal.subrelation else TypeGlobal.subrelation
+
+let resolve_subrelation env avoid car rel sort prf rel' res =
   if eq_constr rel rel' then res
   else
-    let app = mkApp (Lazy.force subrelation, [|car; rel; rel'|]) in
-    let evars, subrel = new_cstr_evar res.rew_evars env app in
+    let evars, app = app_poly res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
+    let evars, subrel = new_cstr_evar evars env app in
     let appsub = mkApp (subrel, [| res.rew_from ; res.rew_to ; prf |]) in
       { res with
 	rew_prf = RewPrf (rel', appsub);
 	rew_evars = evars }
 
-let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars =
+let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars =
   let evars, morph_instance, proj, sigargs, m', args, args' =
     let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
     | Some i -> i
@@ -559,21 +720,23 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars
     let morphargs', morphobjs' = Array.chop first args' in
     let appm = mkApp(m, morphargs) in
     let appmtype = Typing.type_of env (goalevars evars) appm in
-    let cstrs = List.map
-      (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
-      (Array.to_list morphobjs')
+    let cstrs = List.map 
+      (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) 
+      (Array.to_list morphobjs') 
     in
       (* Desired signature *)
-    let evars, appmtype', signature, sigargs =
-      build_signature evars env appmtype cstrs cstr
+    let evars, appmtype', signature, sigargs = 
+      if b then PropGlobal.build_signature evars env appmtype cstrs cstr
+      else TypeGlobal.build_signature evars env appmtype cstrs cstr
     in
       (* Actual signature found *)
     let cl_args = [| appmtype' ; signature ; appm |] in
-    let app = mkApp (Lazy.force proper_type, cl_args) in
+    let evars, app = app_poly evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
+      cl_args in
     let env' = Environ.push_named
-      (Id.of_string "do_subrelation",
-       Some (Lazy.force do_subrelation),
-       Lazy.force apply_subrelation)
+      (Id.of_string "do_subrelation", 
+       Some (snd (app_poly evars PropGlobal.do_subrelation [||])), 
+       snd (app_poly evars PropGlobal.apply_subrelation [||]))
       env
     in
     let evars, morph = new_cstr_evar evars env' app in
@@ -589,13 +752,15 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars
 	      and relation = substl subst relation in
 	      (match y with
 	      | None ->
-		  let evars, proof = proper_proof env evars carrier relation x in
+		  let evars, proof = 
+		    (if b then PropGlobal.proper_proof else TypeGlobal.proper_proof) 
+		      env evars carrier relation x in
 		    [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
 	      | Some r ->
-		  [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars,
+		  [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, 
 	      sigargs, r.rew_to :: typeargs')
 	  | None ->
-	      if not (Option.is_empty y) then
+	      if not (Option.is_empty y) then 
 		error "Cannot rewrite the argument of a dependent function";
 	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
       ([], [], evars, sigargs, []) args args'
@@ -607,66 +772,68 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars
       | _ -> assert(false)
 
 let apply_constraint env avoid car rel prf cstr res =
-  match cstr with
+  match snd cstr with
   | None -> res
-  | Some r -> resolve_subrelation env avoid car rel prf r res
+  | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
+
+let eq_env x y = x == y
 
-let apply_rule l2r flags by loccs : (hypinfo * int) pure_strategy =
+let apply_rule hypinfo by loccs : strategy =
   let (nowhere_except_in,occs) = convert_occs loccs in
   let is_occ occ =
-    if nowhere_except_in
-    then Int.List.mem occ occs
-    else not (Int.List.mem occ occs)
-  in
-  fun (hypinfo, occ) env avoid t ty cstr evars ->
-    let unif = unify_eqn l2r flags env evars hypinfo by t in
-    match unif with
-    | None -> ((hypinfo, occ), Fail)
-    | Some (hypinfo, evd', (prf, (car, rel, c1, c2))) ->
-      let occ = succ occ in
-      let res =
-        if not (is_occ occ) then Fail
-        else if eq_constr t c2 then Same
-        else
-          let res = { rew_car = ty; rew_from = c1;
-                      rew_to = c2; rew_prf = RewPrf (rel, prf);
-                      rew_evars = evd', cstrevars evars }
-          in Info (apply_constraint env avoid car rel prf cstr res)
-      in
-      ((hypinfo, occ), res)
-
-let apply_lemma l2r flags c by loccs : strategy =
-  fun () env avoid t ty cstr evars ->
-    let hypinfo =
-      decompose_applied_relation env (goalevars evars) None c
+    if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
+  let occ = ref 0 in
+    fun env avoid t ty cstr evars ->
+      if not (eq_env !hypinfo.cl.env env) then
+	hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
+      let unif = unify_eqn env evars hypinfo by t in
+	if not (Option.is_empty unif) then incr occ;
+	match unif with
+	| Some (evars', (prf, (car, rel, c1, c2))) when is_occ !occ ->
+	    begin
+	      if eq_constr t c2 then Some None
+	      else
+		let res = { rew_car = ty; rew_from = c1;
+			    rew_to = c2; rew_prf = RewPrf (rel, prf); 
+			    rew_evars = evars' }
+		in Some (Some (apply_constraint env avoid car rel prf cstr res))
+	    end
+	| _ -> None
+
+let apply_lemma flags (evm,c) left2right by loccs : strategy =
+  fun env avoid t ty cstr evars ->
+    let hypinfo = 
+      let evars' = Evd.merge (goalevars evars) evm in
+	ref (decompose_applied_relation env (goalevars evars) evars'
+	       flags None c left2right)
     in
-    let _, res = apply_rule l2r flags by loccs (hypinfo, 0) env avoid t ty cstr evars in
-    (), res
+      apply_rule hypinfo by loccs env avoid t ty cstr evars
 
 let make_leibniz_proof c ty r =
-  let prf =
+  let evars = ref r.rew_evars in
+  let prf = 
     match r.rew_prf with
-    | RewPrf (rel, prf) ->
-	let rel = mkApp (Lazy.force coq_eq, [| ty |]) in
+    | RewPrf (rel, prf) -> 
+	let rel = e_app_poly evars coq_eq [| ty |] in
 	let prf =
-	  mkApp (Lazy.force coq_f_equal,
+	  e_app_poly evars coq_f_equal
 		[| r.rew_car; ty;
 		   mkLambda (Anonymous, r.rew_car, c);
-		   r.rew_from; r.rew_to; prf |])
+		   r.rew_from; r.rew_to; prf |]
 	in RewPrf (rel, prf)
     | RewCast k -> r.rew_prf
   in
-    { r with rew_car = ty;
+    { rew_car = ty; rew_evars = !evars;
       rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf }
 
 let reset_env env =
   let env' = Global.env_of_context (Environ.named_context_val env) in
     Environ.push_rel_context (Environ.rel_context env) env'
-
+      
 let fold_match ?(force=false) env sigma c =
   let (ci, p, c, brs) = destCase c in
   let cty = Retyping.get_type_of env sigma c in
-  let dep, pred, exists, (sk, eff) =
+  let dep, pred, exists, (sk,eff) = 
     let env', ctx, body =
       let ctx, pred = decompose_lam_assum p in
       let env' = Environ.push_rel_context ctx env in
@@ -678,7 +845,7 @@ let fold_match ?(force=false) env sigma c =
     let pred = if dep then p else
 	it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
     in
-    let sk =
+    let sk = 
       if sortp == InProp then
 	if sortc == InProp then
 	  if dep then case_dep_scheme_kind_from_prop
@@ -691,7 +858,7 @@ let fold_match ?(force=false) env sigma c =
 	if dep
 	then case_dep_scheme_kind_from_type
 	else case_scheme_kind_from_type)
-    in
+    in 
     let exists = Ind_tables.check_scheme sk ci.ci_ind in
       if exists || force then
 	dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind
@@ -702,108 +869,121 @@ let fold_match ?(force=false) env sigma c =
     let pars, args = List.chop ci.ci_npar args in
     let meths = List.map (fun br -> br) (Array.to_list brs) in
       applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
-  in
+  in 
     sk, (if exists then env else reset_env env), app, eff
 
 let unfold_match env sigma sk app =
   match kind_of_term app with
-  | App (f', args) when eq_constr f' (mkConst sk) ->
-      let v = Environ.constant_value (Global.env ()) sk in
+  | App (f', args) when eq_constant (fst (destConst f')) sk ->
+      let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
 	Reductionops.whd_beta sigma (mkApp (v, args))
   | _ -> app
 
 let is_rew_cast = function RewCast _ -> true | _ -> false
 
-let coerce env avoid cstr res =
+let coerce env avoid cstr res = 
   let rel, prf = get_rew_prf res in
     apply_constraint env avoid res.rew_car rel prf cstr res
 
-let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
-  let rec aux state env avoid t ty cstr evars =
+let subterm all flags (s : strategy) : strategy =
+  let rec aux env avoid t ty (prop, cstr) evars =
     let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
       match kind_of_term t with
       | App (m, args) ->
-	  let rewrite_args state success =
-	    let state, args', evars', progress =
+	  let rewrite_args success =
+	    let args', evars', progress =
 	      Array.fold_left
-		(fun (state, acc, evars, progress) arg ->
-		  if not (Option.is_empty progress) && not all then (state, None :: acc, evars, progress)
+		(fun (acc, evars, progress) arg ->
+		  if not (Option.is_empty progress) && not all then (None :: acc, evars, progress)
 		  else
-		    let state, res = s state env avoid arg (Typing.type_of env (goalevars evars) arg) None evars in
+		    let argty = Typing.type_of env (goalevars evars) arg in
+		    let res = s env avoid arg argty (prop,None) evars in
 		      match res with
-		      | Same -> (state, None :: acc, evars, if Option.is_empty progress then Some false else progress)
-		      | Info r -> (state, Some r :: acc, r.rew_evars, Some true)
-		      | Fail -> (state, None :: acc, evars, progress))
-		(state, [], evars, success) args
+		      | Some None -> (None :: acc, evars, 
+				      if Option.is_empty progress then Some false else progress)
+		      | Some (Some r) -> 
+			(Some r :: acc, r.rew_evars, Some true)
+		      | None -> (None :: acc, evars, progress))
+		([], evars, success) args
 	    in
-	      state, match progress with
-	      | None -> Fail
-	      | Some false -> Same
+	      match progress with
+	      | None -> None
+	      | Some false -> Some None
 	      | Some true ->
 		  let args' = Array.of_list (List.rev args') in
 		    if Array.exists
-		      (function
-			 | None -> false
+		      (function 
+			 | None -> false 
 			 | Some r -> not (is_rew_cast r.rew_prf)) args'
 		    then
-		      let evars', prf, car, rel, c1, c2 = resolve_morphism env avoid t m args args' cstr' evars' in
+		      let evars', prf, car, rel, c1, c2 = 
+			resolve_morphism env avoid t m args args' (prop, cstr') evars' 
+		      in
 		      let res = { rew_car = ty; rew_from = c1;
 				  rew_to = c2; rew_prf = RewPrf (rel, prf);
-				  rew_evars = evars' }
-		      in Info res
-		    else
+				  rew_evars = evars' } 
+		      in Some (Some res)
+		    else 
 		      let args' = Array.map2
 			(fun aorig anew ->
 			   match anew with None -> aorig
-			   | Some r -> r.rew_to) args args'
+			   | Some r -> r.rew_to) args args' 
 		      in
 		      let res = { rew_car = ty; rew_from = t;
 				  rew_to = mkApp (m, args'); rew_prf = RewCast DEFAULTcast;
 				  rew_evars = evars' }
-		      in Info res
+		      in Some (Some res)
 
 	  in
 	    if flags.on_morphisms then
 	      let mty = Typing.type_of env (goalevars evars) m in
-	      let evars, cstr', m, mty, argsl, args =
+	      let evars, cstr', m, mty, argsl, args = 
 		let argsl = Array.to_list args in
-		  match lift_cstr env evars argsl m mty None with
-		  | Some (evars, cstr', m, mty, args) ->
+		let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in
+		  match lift env evars argsl m mty None with
+		  | Some (evars, cstr', m, mty, args) -> 
 		    evars, Some cstr', m, mty, args, Array.of_list args
 		  | None -> evars, None, m, mty, argsl, args
 	      in
-	      let state, m' = s state env avoid m mty cstr' evars in
+	      let m' = s env avoid m mty (prop, cstr') evars in
 		match m' with
-		| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
-		| Same -> rewrite_args state (Some false)
-		| Info r ->
+		| None -> rewrite_args None (* Standard path, try rewrite on arguments *)
+		| Some None -> rewrite_args (Some false)
+		| Some (Some r) ->
 		    (* We rewrote the function and get a proof of pointwise rel for the arguments.
 		       We just apply it. *)
 		    let prf = match r.rew_prf with
 		      | RewPrf (rel, prf) ->
-			  RewPrf (apply_pointwise rel argsl, mkApp (prf, args))
+			let app = if prop then PropGlobal.apply_pointwise 
+			  else TypeGlobal.apply_pointwise 
+			in
+			  RewPrf (app rel argsl, mkApp (prf, args))
 		      | x -> x
 		    in
 		    let res =
 		      { rew_car = prod_appvect r.rew_car args;
 			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
-			rew_prf = prf;
-			rew_evars = r.rew_evars }
-		    in
-		      state, match prf with
+			rew_prf = prf; rew_evars = r.rew_evars }
+		    in 
+		      match prf with
 		      | RewPrf (rel, prf) ->
-			Info (apply_constraint env avoid res.rew_car rel prf cstr res)
-		      | RewCast _ -> Info res
-	    else rewrite_args state None
-
+			Some (Some (apply_constraint env avoid res.rew_car
+				      rel prf (prop,cstr) res))
+		      | _ -> Some (Some res)
+	    else rewrite_args None
+	      
       | Prod (n, x, b) when noccurn 1 b ->
 	  let b = subst1 mkProp b in
-	  let tx = Typing.type_of env (goalevars evars) x and tb = Typing.type_of env (goalevars evars) b in
-	  let mor, unfold = arrow_morphism tx tb x b in
-	  let state, res = aux state env avoid mor ty cstr evars in
-	    state, (match res with
-	    | Info r -> Info { r with rew_to = unfold r.rew_to }
-	    | Fail | Same -> res)
+	  let tx = Typing.type_of env (goalevars evars) x 
+	  and tb = Typing.type_of env (goalevars evars) b in
+	  let arr = if prop then PropGlobal.arrow_morphism 
+	    else TypeGlobal.arrow_morphism 
+	  in
+	  let (evars', mor), unfold = arr evars tx tb x b in
+	  let res = aux env avoid mor ty (prop,cstr) evars' in
+	    (match res with
+	    | Some (Some r) -> Some (Some { r with rew_to = unfold r.rew_to })
+	    | _ -> res)
 
       (* 		if x' = None && flags.under_lambdas then *)
       (* 		  let lam = mkLambda (n, x, b) in *)
@@ -821,80 +1001,116 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 
       | Prod (n, dom, codom) ->
 	  let lam = mkLambda (n, dom, codom) in
-	  let app, unfold =
+	  let (evars', app), unfold = 
 	    if eq_constr ty mkProp then
-	      mkApp (Lazy.force coq_all, [| dom; lam |]), unfold_all
-	    else mkApp (Lazy.force coq_forall, [| dom; lam |]), unfold_forall
+	      (app_poly evars coq_all [| dom; lam |]), TypeGlobal.unfold_all
+	    else 
+	      let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
+		(app_poly evars forall [| dom; lam |]), TypeGlobal.unfold_forall
 	  in
-	  let state, res = aux state env avoid app ty cstr evars in
-	    state, (match res with
-	     | Info r -> Info { r with rew_to = unfold r.rew_to }
-	     | Fail | Same -> res)
+	  let res = aux env avoid app ty (prop,cstr) evars' in
+	    (match res with
+	     | Some (Some r) -> Some (Some { r with rew_to = unfold r.rew_to })
+	     | _ -> res)
+
+(* TODO: real rewriting under binders: introduce x x' (H : R x x') and rewrite with 
+   H at any occurrence of x. Ask for (R ==> R') for the lambda. Formalize this.
+   B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing
+   dependent relations and using projections to get them out.
+ *)
+      (* | Lambda (n, t, b) when flags.under_lambdas -> *)
+      (* 	  let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *)
+      (* 	  let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *)
+      (* 	  let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *)
+      (* 	  let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *)
+      (* 	  let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *)
+      (* 	  let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *)
+      (* 	    (match b' with *)
+      (* 	    | Some (Some r) -> *)
+      (* 		let prf = match r.rew_prf with *)
+      (* 		  | RewPrf (rel, prf) -> *)
+      (* 		      let rel = pointwise_or_dep_relation n' t r.rew_car rel in *)
+      (* 		      let prf = mkLambda (n', t, prf) in *)
+      (* 			RewPrf (rel, prf) *)
+      (* 		  | x -> x *)
+      (* 		in *)
+      (* 		  Some (Some { r with *)
+      (* 		    rew_prf = prf; *)
+      (* 		    rew_car = mkProd (n, t, r.rew_car); *)
+      (* 		    rew_from = mkLambda(n, t, r.rew_from); *)
+      (* 		    rew_to = mkLambda (n, t, r.rew_to) }) *)
+      (* 	    | _ -> b') *)
 
       | Lambda (n, t, b) when flags.under_lambdas ->
-	  let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
-	  let env' = Environ.push_rel (n', None, t) env in
-	  let state, b' = s state env' avoid b (Typing.type_of env' (goalevars evars) b) (unlift_cstr env (goalevars evars) cstr) evars in
-	    state, (match b' with
-	    | Info r ->
-		let prf = match r.rew_prf with
-		  | RewPrf (rel, prf) ->
-		      let rel = pointwise_or_dep_relation n' t r.rew_car rel in
-		      let prf = mkLambda (n', t, prf) in
-			RewPrf (rel, prf)
-		  | x -> x
+	let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
+	let env' = Environ.push_rel (n', None, t) env in
+	let bty = Typing.type_of env' (goalevars evars) b in
+	let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
+	let b' = s env' avoid b bty (prop, unlift env evars cstr) evars in
+	  (match b' with
+	  | Some (Some r) ->
+	    let r = match r.rew_prf with
+	      | RewPrf (rel, prf) ->
+		let point = if prop then PropGlobal.pointwise_or_dep_relation else
+		    TypeGlobal.pointwise_or_dep_relation
 		in
-		  Info { r with
-		    rew_prf = prf;
-		    rew_car = mkProd (n, t, r.rew_car);
-		    rew_from = mkLambda(n, t, r.rew_from);
-		    rew_to = mkLambda (n, t, r.rew_to) }
-	    | Fail | Same -> b')
-
+		let evars, rel = point r.rew_evars n' t r.rew_car rel in
+		let prf = mkLambda (n', t, prf) in
+		  { r with rew_prf = RewPrf (rel, prf); rew_evars = evars }
+	      | x -> r
+	    in
+	      Some (Some { r with
+		rew_car = mkProd (n, t, r.rew_car);
+		rew_from = mkLambda(n, t, r.rew_from);
+		rew_to = mkLambda (n, t, r.rew_to) })
+	  | _ -> b')
+	    
       | Case (ci, p, c, brs) ->
-	  let cty = Typing.type_of env (goalevars evars) c in
-	  let cstr' = Some (mkApp (Lazy.force coq_eq, [| cty |])) in
-	  let state, c' = s state env avoid c cty cstr' evars in
-	  let state, res =
-	    match c' with
-	    | Info r ->
-		let res = make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r in
-		  state, Info (coerce env avoid cstr res)
-	    | Same | Fail ->
-	      if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
-		let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
-		let state, found, brs' = Array.fold_left
-		  (fun (state, found, acc) br ->
-		   if not (Option.is_empty found) then (state, found, fun x -> lift 1 br :: acc x)
-		   else
-                     let state, res = s state env avoid br ty cstr evars in
-		     match res with
-		     | Info r -> (state, Some r, fun x -> mkRel 1 :: acc x)
-		     | Fail | Same -> (state, None, fun x -> lift 1 br :: acc x))
-		  (state, None, fun x -> []) brs
-		in
-		  state, match found with
-		  | Some r ->
-		    let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in
-		      Info (make_leibniz_proof ctxc ty r)
-		  | None -> c'
-	      else
-		match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
-		| None -> state, c'
-		| Some (cst, _, t',_) -> (* eff XXX *)
-                  let state, res = aux state env avoid t' ty cstr evars in
-		  state, match res with
-		  | Info prf ->
-		    Info { prf with
-				 rew_from = t; rew_to = unfold_match env (goalevars evars) cst prf.rew_to }
-		  | x' -> c'
-	  in
-	    state, (match res with
-	     | Info r ->
-	       let rel, prf = get_rew_prf r in
-		 Info (apply_constraint env avoid r.rew_car rel prf cstr r)
-	     | x -> x)
-      | _ -> state, Fail
+	let cty = Typing.type_of env (goalevars evars) c in
+	let evars', eqty = app_poly evars coq_eq [| cty |] in
+	let cstr' = Some eqty in
+	let c' = s env avoid c cty (prop, cstr') evars' in
+	let res = 
+	  match c' with
+	  | Some (Some r) ->
+	    let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
+	    let res = make_leibniz_proof case ty r in
+	      Some (Some (coerce env avoid (prop,cstr) res))
+	  | x ->
+	    if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
+	      let evars', eqty = app_poly evars coq_eq [| ty |] in
+	      let cstr = Some eqty in
+	      let found, brs' = Array.fold_left 
+		(fun (found, acc) br ->
+		  if not (Option.is_empty found) then (found, fun x -> lift 1 br :: acc x)
+		  else
+		    match s env avoid br ty (prop,cstr) evars with
+		    | Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x)
+		    | _ -> (None, fun x -> lift 1 br :: acc x))
+		(None, fun x -> []) brs
+	      in
+		match found with
+		| Some r ->
+		  let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in
+		    Some (Some (make_leibniz_proof ctxc ty r))
+		| None -> x
+	    else
+	      match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
+	      | None -> x
+	      | Some (cst, _, t', eff (*FIXME*)) ->
+		match aux env avoid t' ty (prop,cstr) evars with
+		| Some (Some prf) -> 
+		  Some (Some { prf with
+		    rew_from = t; 
+		    rew_to = unfold_match env (goalevars evars) cst prf.rew_to })
+		| x' -> x
+	in 
+	  (match res with
+	  | Some (Some r) ->  
+	    let rel, prf = get_rew_prf r in
+	      Some (Some (apply_constraint env avoid r.rew_car rel prf (prop,cstr) r))
+	  | x -> x)
+      | _ -> None
   in aux
 
 let all_subterms = subterm true default_flags
@@ -903,25 +1119,35 @@ let one_subterm = subterm false default_flags
 (** Requires transitivity of the rewrite step, if not a reduction.
     Not tail-recursive. *)
 
-let transitivity state env avoid (res : rewrite_result_info) (next : 'a pure_strategy) : 'a * rewrite_result_info rewrite_result =
-  let state, res' = next state env avoid res.rew_to res.rew_car (get_opt_rew_rel res.rew_prf) res.rew_evars in
-  state, match res' with
-  | Fail -> Fail
-  | Same -> Info res
-  | Info res' ->
+let transitivity env avoid prop (res : rewrite_result_info) (next : strategy) : 
+    rewrite_result option =
+  let nextres =
+    next env avoid res.rew_to res.rew_car
+      (prop, get_opt_rew_rel res.rew_prf) res.rew_evars 
+  in 
+  match nextres with
+  | None -> None
+  | Some None -> Some (Some res)
+  | Some (Some res') ->
       match res.rew_prf with
-      | RewCast c -> Info { res' with rew_from = res.rew_from }
+      | RewCast c -> Some (Some { res' with rew_from = res.rew_from })
       | RewPrf (rew_rel, rew_prf) ->
 	  match res'.rew_prf with
-	  | RewCast _ -> Info { res with rew_to = res'.rew_to }
+	  | RewCast _ -> Some (Some ({ res with rew_to = res'.rew_to }))
 	  | RewPrf (res'_rel, res'_prf) ->
-	      let prfty = mkApp (Lazy.force transitive_type, [| res.rew_car; rew_rel |]) in
-	      let evars, prf = new_cstr_evar res'.rew_evars env prfty in
-	      let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
-				      rew_prf; res'_prf |])
-	      in Info { res' with rew_from = res.rew_from;
-		rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) }
-
+	    let trans = 
+	      if prop then PropGlobal.transitive_type 
+	      else TypeGlobal.transitive_type
+	    in
+	    let evars, prfty = 
+	      app_poly res'.rew_evars trans [| res.rew_car; rew_rel |] 
+	    in
+	    let evars, prf = new_cstr_evar evars env prfty in
+	    let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
+				    rew_prf; res'_prf |])
+	    in Some (Some { res' with rew_from = res.rew_from; 
+	      rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) })
+		
 (** Rewriting strategies.
 
     Inspired by ELAN's rewriting strategies:
@@ -931,103 +1157,129 @@ let transitivity state env avoid (res : rewrite_result_info) (next : 'a pure_str
 module Strategies =
   struct
 
-    let fail : 'a pure_strategy =
-      fun s env avoid t ty cstr evars -> (s, Fail)
+    let fail : strategy =
+      fun env avoid t ty cstr evars -> None
 
-    let id : 'a pure_strategy =
-      fun s env avoid t ty cstr evars -> (s, Same)
+    let id : strategy =
+      fun env avoid t ty cstr evars -> Some None
 
-    let refl : 'a pure_strategy =
-      fun s env avoid t ty cstr evars ->
+    let refl : strategy =
+      fun env avoid t ty (prop,cstr) evars ->
 	let evars, rel = match cstr with
-	  | None -> new_cstr_evar evars env (mk_relation ty)
+	  | None -> 
+	    let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
+	    let evars, rty = mkr evars ty in
+	      new_cstr_evar evars env rty
 	  | Some r -> evars, r
 	in
 	let evars, proof =
-	  let mty = mkApp (Lazy.force proper_proxy_type, [| ty ; rel; t |]) in
+	  let proxy = 
+	    if prop then PropGlobal.proper_proxy_type 
+	    else TypeGlobal.proper_proxy_type
+	  in
+	  let evars, mty = app_poly evars proxy [| ty ; rel; t |] in
 	    new_cstr_evar evars env mty
 	in
-	  s, Info { rew_car = ty; rew_from = t; rew_to = t;
-		       rew_prf = RewPrf (rel, proof); rew_evars = evars }
-
-    let progress (s : 'a pure_strategy) : 'a pure_strategy =
-      fun state env avoid t ty cstr evars ->
-        let state, res = s state env avoid t ty cstr evars in
-	state, match res with
-	| Fail -> Fail
-	| Same -> Fail
-	| Info _ -> res
-
-    let seq (fst : 'a pure_strategy) (snd : 'a pure_strategy) : 'a pure_strategy =
-      fun state env avoid t ty cstr evars ->
-        let state, res = fst state env avoid t ty cstr evars in
-	match res with
-	| Fail -> state, Fail
-	| Same -> snd state env avoid t ty cstr evars
-	| Info res -> transitivity state env avoid res snd
-
-    let choice fst snd : 'a pure_strategy =
-      fun state env avoid t ty cstr evars ->
-        let state, res = fst state env avoid t ty cstr evars in
-	match res with
-	| Fail -> snd state env avoid t ty cstr evars
-	| Same | Info _ -> state, res
-
-    let try_ str : 'a pure_strategy = choice str id
-
-    let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
-      let rec aux state env avoid t ty cstr evars =
-        f aux state env avoid t ty cstr evars
-      in aux
-
-    let any (s : 'a pure_strategy) : 'a pure_strategy =
+	  Some (Some { rew_car = ty; rew_from = t; rew_to = t;
+		       rew_prf = RewPrf (rel, proof); rew_evars = evars })
+
+    let progress (s : strategy) : strategy =
+      fun env avoid t ty cstr evars ->
+	match s env avoid t ty cstr evars with
+	| None -> None
+	| Some None -> None
+	| r -> r
+
+    let seq first snd : strategy =
+      fun env avoid t ty cstr evars ->
+	match first env avoid t ty cstr evars with
+	| None -> None
+	| Some None -> snd env avoid t ty cstr evars
+	| Some (Some res) -> transitivity env avoid (fst cstr) res snd
+
+    let choice fst snd : strategy =
+      fun env avoid t ty cstr evars ->
+	match fst env avoid t ty cstr evars with
+	| None -> snd env avoid t ty cstr evars
+	| res -> res
+
+    let try_ str : strategy = choice str id
+
+    let fix (f : strategy -> strategy) : strategy =
+      let rec aux env = f (fun env -> aux env) env in aux
+
+    let any (s : strategy) : strategy =
       fix (fun any -> try_ (seq s any))
 
-    let repeat (s : 'a pure_strategy) : 'a pure_strategy =
+    let repeat (s : strategy) : strategy =
       seq s (any s)
 
-    let bu (s : 'a pure_strategy) : 'a pure_strategy =
+    let bu (s : strategy) : strategy =
       fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))
 
-    let td (s : 'a pure_strategy) : 'a pure_strategy =
+    let td (s : strategy) : strategy =
       fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))
 
-    let innermost (s : 'a pure_strategy) : 'a pure_strategy =
+    let innermost (s : strategy) : strategy =
       fix (fun ins -> choice (one_subterm ins) s)
 
-    let outermost (s : 'a pure_strategy) : 'a pure_strategy =
+    let outermost (s : strategy) : strategy =
       fix (fun out -> choice s (one_subterm out))
 
-    let lemmas flags cs : 'a pure_strategy =
+    let lemmas flags cs : strategy =
       List.fold_left (fun tac (l,l2r,by) ->
-	choice tac (apply_lemma l2r flags l by AllOccurrences))
+	choice tac (apply_lemma flags l l2r by AllOccurrences))
 	fail cs
 
-    let old_hints (db : string) : 'a pure_strategy =
+    let inj_open hint =
+      (Evd.from_env ~ctx:hint.Autorewrite.rew_ctx (Global.env()),
+       (hint.Autorewrite.rew_lemma, NoBindings))
+
+    let old_hints (db : string) : strategy =
       let rules = Autorewrite.find_rewrites db in
 	lemmas rewrite_unif_flags
-	  (List.map (fun hint -> ((hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r, hint.Autorewrite.rew_tac)) rules)
+	  (List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
+				  hint.Autorewrite.rew_tac)) rules)
 
-    let hints (db : string) : 'a pure_strategy =
-      fun state env avoid t ty cstr evars ->
+    let hints (db : string) : strategy =
+      fun env avoid t ty cstr evars ->
       let rules = Autorewrite.find_matches db t in
-      let lemma hint = ((hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r,
+      let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
 			hint.Autorewrite.rew_tac) in
       let lems = List.map lemma rules in
-	lemmas rewrite_unif_flags lems state env avoid t ty cstr evars
+	lemmas rewrite_unif_flags lems env avoid t ty cstr evars
 
-    let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
-      fun state env avoid t ty cstr evars ->
-        let rfn, ckind = Redexpr.reduction_of_red_expr env r in
+    let reduce (r : Redexpr.red_expr) : strategy =
+	fun env avoid t ty cstr evars ->
+          let rfn, ckind = Redexpr.reduction_of_red_expr env r in
 	  let t' = rfn env (goalevars evars) t in
 	    if eq_constr t' t then
-	      state, Same
+	      Some None
 	    else
-	      state, Info { rew_car = ty; rew_from = t; rew_to = t';
-			   rew_prf = RewCast ckind; rew_evars = evars }
+	      Some (Some { rew_car = ty; rew_from = t; rew_to = t';
+			   rew_prf = RewCast ckind; rew_evars = evars })
+	
+    let fold c : strategy =
+      fun env avoid t ty cstr evars ->
+(* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
+	let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
+	let unfolded =
+	  try Tacred.try_red_product env sigma c
+	  with e when Errors.noncritical e ->
+            error "fold: the term is not unfoldable !"
+	in
+	  try
+	  let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ())
+	    unfolded t in
+	    let c' = Evarutil.nf_evar sigma c in
+	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
+			   rew_prf = RewCast DEFAULTcast; 
+			   rew_evars = (sigma, snd evars) })
+	  with e when Errors.noncritical e -> None
 
-    let fold_glob c : 'a pure_strategy =
-      fun state env avoid t ty cstr evars ->
+
+    let fold_glob c : strategy =
+      fun env avoid t ty cstr evars ->
 (* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
 	let sigma, c = Pretyping.understand_tcc (goalevars evars) env c in
 	let unfolded =
@@ -1036,120 +1288,133 @@ module Strategies =
             error "fold: the term is not unfoldable !"
 	in
 	  try
-	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
+	    let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
 	    let c' = Evarutil.nf_evar sigma c in
-	      state, Info { rew_car = ty; rew_from = t; rew_to = c';
+	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast;
-			   rew_evars = sigma, cstrevars evars }
-	  with e when Errors.noncritical e -> state, Fail
-
+			   rew_evars = (sigma, snd evars) })
+	  with e when Errors.noncritical e -> None
+  
 
 end
 
 (** The strategy for a single rewrite, dealing with occurences. *)
 
-let rewrite_with l2r flags c occs : strategy =
-  fun () env avoid t ty cstr evars ->
+let rewrite_strat flags occs hyp =
+  let app = apply_rule hyp None occs in
+  let rec aux () =
+    Strategies.choice app (subterm true flags (fun env -> aux () env))
+  in aux ()
+
+let get_hypinfo_ids {c = opt} =
+  match opt with
+  | None -> []
+  | Some (is, gc) ->
+    let avoid = Option.default [] (TacStore.get is.extra f_avoid_ids) in
+      Id.Map.fold (fun id _ accu -> id :: accu) is.lfun avoid
+      
+let rewrite_with flags c left2right loccs : strategy =
+  fun env avoid t ty cstr evars ->
     let gevars = goalevars evars in
-    let hypinfo = decompose_applied_relation_expr env gevars c in
-    let (is, _) = c in
-    let avoid = match TacStore.get is.extra f_avoid_ids with
-    | None -> avoid
-    | Some l -> l @ avoid
-    in
-    let avoid = Id.Map.fold (fun id _ accu -> id :: accu) is.lfun avoid in
-    let app = apply_rule l2r flags None occs in
-    let strat = Strategies.fix (fun aux -> Strategies.choice app (subterm true default_flags aux)) in
-    let _, res = strat (hypinfo, 0) env avoid t ty cstr (gevars, cstrevars evars) in
-    ((), res)
-
-let apply_strategy (s : strategy) env avoid concl cstr evars =
-  let _, res =
-    s () env avoid concl (Typing.type_of env (goalevars evars) concl)
-      (Option.map snd cstr) evars
+    let hypinfo = ref (decompose_applied_relation_expr env gevars flags c left2right) in
+    let avoid = get_hypinfo_ids !hypinfo @ avoid in
+      rewrite_strat default_flags loccs hypinfo env avoid t ty cstr (gevars, cstrevars evars)
+
+let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
+  let res =
+    s env avoid concl (Typing.type_of env (goalevars evars) concl)
+      (prop, Some cstr) evars
   in
     match res with
-    | Fail -> Fail
-    | Same -> Same
-    | Info res ->
-	Info (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to)
+    | None -> None
+    | Some None -> Some None
+    | Some (Some res) ->
+	Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to))
 
-let solve_constraints env evars =
+let solve_constraints env (evars,cstrs) =
   Typeclasses.resolve_typeclasses env ~split:false ~fail:true evars
 
 let nf_zeta =
   Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 
-exception RewriteFailure of std_ppcmds
+exception RewriteFailure of Pp.std_ppcmds
 
-type result = (evar_map * constr option * types) rewrite_result
+type result = (evar_map * constr option * types) option option
 
 let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
-  let cstr =
-    let sort = mkProp in
-    let impl = Lazy.force impl in
+  let evars = (sigma, Evar.Set.empty) in
+  let evars, cstr =
+    let sort = Typing.sort_of env (goalevars evars) concl in
+    let prop, (evars, arrow) = 
+      if is_prop_sort sort then true, app_poly evars impl [||]
+      else false, app_poly evars arrow [||]
+    in
       match is_hyp with
-      | None -> (sort, inverse sort impl)
-      | Some _ -> (sort, impl)
+      | None -> 
+	let evars, t = poly_inverse prop env evars (mkSort sort) arrow in 
+	  evars, (prop, t)
+      | Some _ -> evars, (prop, arrow)
   in
-  let evars = (sigma, Evar.Set.empty) in
-  let eq = apply_strategy strat env avoid concl (Some cstr) evars in
+  let eq = apply_strategy strat env avoid concl cstr evars in
     match eq with
-    | Fail -> Fail
-    | Same -> Same
-    | Info (p, (evars, cstrs), car, oldt, newt) ->
-	let evars' = solve_constraints env evars in
+    | Some (Some (p, (evars, cstrs), car, oldt, newt)) ->
+	let evars' = solve_constraints env (evars, cstrs) in
+	let p = map_rewprf (fun p -> nf_zeta env evars' (Evarutil.nf_evar evars' p)) p in
 	let newt = Evarutil.nf_evar evars' newt in
+	let abs = Option.map (fun (x, y) ->
+				Evarutil.nf_evar evars' x, Evarutil.nf_evar evars' y) abs in
 	let evars = (* Keep only original evars (potentially instantiated) and goal evars,
 		       the rest has been defined and substituted already. *)
-	  Evd.fold (fun ev evi acc ->
-	    if Evar.Set.mem ev cstrs then Evd.remove acc ev
-	    else acc) evars' evars'
+	  Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars'
 	in
-        match p with
-        | RewCast c -> Info (evars, None, newt)
-        | RewPrf (_, p) ->
-          let p = nf_zeta env evars' (Evarutil.nf_evar evars' p) in
-          let term = match abs with
-          | None -> p
-          | Some (t, ty) ->
-            let t = Evarutil.nf_evar evars' t in
-            let ty = Evarutil.nf_evar evars' ty in
-            mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |])
-          in
-          let proof = match is_hyp with
-          | None -> term
-          | Some id -> mkApp (term, [| mkVar id |])
-          in
-          Info (evars, Some proof, newt)
-
-(** ppedrot: this is a workaround. The current implementation of rewrite leaks
-    evar maps. We know that we should not produce effects in here, so we reput
-    them after computing... *)
-let tclEFFECT (tac : tactic) : tactic = fun gl ->
-  let eff = Evd.eval_side_effects gl.sigma in
-  let gls = tac gl in
-  let sigma = Evd.emit_side_effects eff (Evd.drop_side_effects gls.sigma) in
-  { gls with sigma; }
-
-let cl_rewrite_clause_tac ?abs strat clause gl =
-  let evartac evd = Refiner.tclEVARS evd in
+	let res =
+	  match is_hyp with
+	  | Some id ->
+	      (match p with
+	       | RewPrf (rel, p) ->
+		   let term =
+		     match abs with
+		     | None -> p
+		     | Some (t, ty) ->
+			 mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |])
+		   in
+		     Some (evars, Some (mkApp (term, [| mkVar id |])), newt)
+	       | RewCast c ->
+		   Some (evars, None, newt))
+		
+	  | None ->
+	      (match p with
+	       | RewPrf (rel, p) ->
+		   (match abs with
+		    | None -> Some (evars, Some p, newt)
+		    | Some (t, ty) ->
+			let proof = mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |]) in
+			  Some (evars, Some proof, newt))
+	       | RewCast c -> Some (evars, None, newt))
+	in Some res
+    | Some None -> Some None
+    | None -> None
+		   
+let rewrite_refine (evd,c) = 
+  Tacmach.refine c
+
+let cl_rewrite_clause_tac ?abs strat meta clause gl =
+  let evartac evd = Refiner.tclEVARS (Evd.clear_metas evd) in
   let treat res =
     match res with
-    | Fail -> tclFAIL 0 (str "Nothing to rewrite")
-    | Same ->
-	tclFAIL 0 (str"No progress made")
-    | Info (undef, p, newt) ->
-	let tac =
+    | None -> tclFAIL 0 (str "Nothing to rewrite")
+    | Some None -> tclIDTAC
+    | Some (Some (undef, p, newt)) ->
+	let tac = 
 	  match clause, p with
 	  | Some id, Some p ->
 	      cut_replacing id newt (Tacmach.refine p)
-	  | Some id, None ->
+	  | Some id, None -> 
 	      change_in_hyp None newt (id, InHypTypeOnly)
 	  | None, Some p ->
 	      let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
 		tclTHENLAST
-		  (Tacmach.internal_cut_no_check false name newt)
+		  (Tacmach.internal_cut false name newt)
 		  (tclTHEN (Tactics.revert [name]) (Tacmach.refine p))
 	  | None, None -> change_in_concl None newt
 	in tclTHEN (evartac undef) tac
@@ -1162,7 +1427,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
 	| None -> pf_concl gl, None
       in
       let sigma = project gl in
-      let concl = Evarutil.nf_evar sigma concl in
+      let concl = Evarutil.nf_evar sigma concl in 
       let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
 	treat res
     with
@@ -1170,35 +1435,35 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
 	Refiner.tclFAIL 0
 	  (str"Unable to satisfy the rewriting constraints."
 	   ++ fnl () ++ Himsg.explain_typeclass_error env e)
-  in tclEFFECT tac gl
+  in tac gl
 
 
 let bind_gl_info f =
-  bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev)))
+  bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev))) 
 
 let new_refine c : Goal.subgoals Goal.sensitive =
   let refable = Goal.Refinable.make
-    (fun handle -> Goal.Refinable.constr_of_open_constr handle true c)
+    (fun handle -> Goal.Refinable.constr_of_open_constr handle true c) 
   in Goal.bind refable Goal.refine
 
-let assert_replacing id newt tac =
-  let sens = bind_gl_info
+let assert_replacing id newt tac = 
+  let sens = bind_gl_info 
     (fun concl env sigma ->
-       let nc' =
+       let nc' = 
 	 Environ.fold_named_context
 	   (fun _ (n, b, t as decl) nc' ->
 	      if Id.equal n id then (n, b, newt) :: nc'
 	      else decl :: nc')
 	   env ~init:[]
        in
-       let reft = Refinable.make
-	 (fun h ->
+       let reft = Refinable.make 
+	 (fun h -> 
 	    Goal.bind (Refinable.mkEvar h
 			 (Environ.reset_with_named_context (val_of_named_context nc') env) concl)
-	      (fun ev ->
+	      (fun ev -> 
 		 Goal.bind (Refinable.mkEvar h env newt)
 		   (fun ev' ->
-		      let inst =
+		      let inst = 
 			fold_named_context
 			  (fun _ (n, b, t) inst ->
 			     if Id.equal n id then ev' :: inst
@@ -1206,34 +1471,32 @@ let assert_replacing id newt tac =
 			  env ~init:[]
 		      in
 		      let (e, args) = destEvar ev in
-			Goal.return
-                         (mkEvar (e, Array.of_list inst)))))
+			Goal.return (mkEvar (e, Array.of_list inst)))))
        in Goal.bind reft Goal.refine)
-  in Tacticals.New.tclTHEN (Proofview.tclSENSITIVE sens)
+  in Proofview.tclTHEN (Proofview.tclSENSITIVE sens) 
        (Proofview.tclFOCUS 2 2 tac)
 
-let newfail n s =
+let newfail n s = 
   Proofview.tclZERO (Refiner.FailError (n, lazy s))
 
 let cl_rewrite_clause_newtac ?abs strat clause =
-  let treat (res, is_hyp) =
+  let treat (res, is_hyp) = 
     match res with
-    | Fail -> newfail 0 (str "Nothing to rewrite")
-    | Same ->
-	newfail 0 (str"No progress made")
-    | Info res ->
+    | None -> newfail 0 (str "Nothing to rewrite")
+    | Some None -> Proofview.tclUNIT ()
+    | Some (Some res) ->
 	match is_hyp, res with
 	| Some id, (undef, Some p, newt) ->
 	    assert_replacing id newt (Proofview.tclSENSITIVE (new_refine (undef, p)))
-	| Some id, (undef, None, newt) ->
+	| Some id, (undef, None, newt) -> 
 	    Proofview.tclSENSITIVE (Goal.convert_hyp false (id, None, newt))
 	| None, (undef, Some p, newt) ->
 	    let refable = Goal.Refinable.make
-	      (fun handle ->
+	      (fun handle -> 
 		 Goal.bind env
 		   (fun env -> Goal.bind (Refinable.mkEvar handle env newt)
 		      (fun ev ->
-			 Goal.Refinable.constr_of_open_constr handle true
+			 Goal.Refinable.constr_of_open_constr handle true 
 			   (undef, mkApp (p, [| ev |])))))
 	    in
 	      Proofview.tclSENSITIVE (Goal.bind refable Goal.refine)
@@ -1248,9 +1511,9 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	   | Some id -> Environ.named_type id env, Some id
 	   | None -> concl, None
 	 in
-	   try
-	     let res =
-	       cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
+	   try 
+	     let res = 
+	       cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp 
 	     in return (res, is_hyp)
 	   with
 	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
@@ -1262,52 +1525,73 @@ let newtactic_init_setoid () =
   try init_setoid (); Proofview.tclUNIT ()
   with e when Errors.noncritical e -> Proofview.tclZERO e
 
-let tactic_init_setoid () =
+let tactic_init_setoid () = 
   init_setoid (); tclIDTAC
-
+  
 let cl_rewrite_clause_new_strat ?abs strat clause =
-  Tacticals.New.tclTHEN (newtactic_init_setoid ())
+  Proofview.tclTHEN (newtactic_init_setoid ())
   (try cl_rewrite_clause_newtac ?abs strat clause
    with RewriteFailure s ->
    newfail 0 (str"setoid rewrite failed: " ++ s))
 
-let cl_rewrite_clause_newtac' l left2right occs clause =
-  Proofview.tclFOCUS 1 1
-       (cl_rewrite_clause_new_strat (rewrite_with left2right rewrite_unif_flags l occs) clause)
+(* let cl_rewrite_clause_newtac' l left2right occs clause = *)
+(*   Proof_global.run_tactic  *)
+(*     (Proofview.tclFOCUS 1 1  *)
+(*        (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)) *)
 
 let cl_rewrite_clause_strat strat clause =
   tclTHEN (tactic_init_setoid ())
-  (fun gl ->
+  (fun gl -> 
+   let meta = Evarutil.new_meta() in
      (*     let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in *)
-     try cl_rewrite_clause_tac strat clause gl
+     try cl_rewrite_clause_tac strat (mkMeta meta) clause gl
      with RewriteFailure e ->
        tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl
-     | Refiner.FailError (n, pp) ->
+     | Refiner.FailError (n, pp) -> 
        tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)
 
 let cl_rewrite_clause l left2right occs clause gl =
-  cl_rewrite_clause_strat (rewrite_with left2right (general_rewrite_unif_flags ()) l occs) clause gl
+  cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl
+
+let occurrences_of = function
+  | n::_ as nl when n < 0 -> (false,List.map abs nl)
+  | nl ->
+      if List.exists (fun n -> n < 0) nl then
+	error "Illegal negative occurrence number.";
+      (true,nl)
+
+open Extraargs
+
+let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars ->
+  let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in
+    apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) 
+      l2r None occs env avoid t ty cstr (evd, cstrevars evars)
 
-let apply_glob_constr c l2r occs = fun () env avoid t ty cstr evars ->
+let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars ->
   let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
-    apply_lemma l2r (general_rewrite_unif_flags ()) (c, NoBindings)
-      None occs () env avoid t ty cstr (evd, cstrevars evars)
+    apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) 
+      l2r None occs env avoid t ty cstr (evd, cstrevars evars)
 
-let interp_glob_constr_list env sigma cl =
-  let understand sigma (c, _) =
-    let sigma, c = Pretyping.understand_tcc sigma env c in
-    (sigma, ((c, NoBindings), true, None))
-  in
-  List.fold_map understand sigma cl
+let interp_constr_list env sigma =
+  List.map (fun c -> 
+	      let evd, c = Constrintern.interp_open_constr sigma env c in
+		(evd, (c, NoBindings)), true, None)
+
+let interp_glob_constr_list env sigma =
+  List.map (fun c -> 
+	      let evd, c = Pretyping.understand_tcc sigma env c in
+		(evd, (c, NoBindings)), true, None)
 
-type ('constr,'redexpr) strategy_ast =
+(* Syntax for rewriting with strategies *)
+
+type ('constr,'redexpr) strategy_ast = 
   | StratId | StratFail | StratRefl
   | StratUnary of string * ('constr,'redexpr) strategy_ast
   | StratBinary of string * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
   | StratConstr of 'constr * bool
   | StratTerms of 'constr list
   | StratHints of bool * string
-  | StratEval of 'redexpr
+  | StratEval of 'redexpr 
   | StratFold of 'constr
 
 let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> ('a2,'b2) strategy_ast = function
@@ -1324,7 +1608,7 @@ let rec strategy_of_ast = function
   | StratId -> Strategies.id
   | StratFail -> Strategies.fail
   | StratRefl -> Strategies.refl
-  | StratUnary (f, s) ->
+  | StratUnary (f, s) -> 
     let s' = strategy_of_ast s in
     let f' = match f with
       | "subterms" -> all_subterms
@@ -1349,28 +1633,31 @@ let rec strategy_of_ast = function
     in f' s' t'
   | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
   | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
-  | StratTerms l ->
-    (fun () env avoid t ty cstr (evars, cstrs) ->
-     let evars, cl = interp_glob_constr_list env evars l in
-       Strategies.lemmas rewrite_unif_flags cl () env avoid t ty cstr (evars, cstrs))
-  | StratEval r ->
-    (fun () env avoid t ty cstr evars ->
+  | StratTerms l -> 
+    (fun env avoid t ty cstr evars ->
+     let l' = interp_glob_constr_list env (goalevars evars) (List.map fst l) in
+       Strategies.lemmas rewrite_unif_flags l' env avoid t ty cstr evars)
+  | StratEval r -> 
+    (fun env avoid t ty cstr evars ->
      let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
-       Strategies.reduce r_interp () env avoid t ty cstr (sigma,cstrevars evars))
+       Strategies.reduce r_interp env avoid t ty cstr (sigma,cstrevars evars))
   | StratFold c -> Strategies.fold_glob (fst c)
 
 
-let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s))),l)
+(* By default the strategy for "rewrite_db" is top-down *)
+
+let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
 
 let declare_an_instance n s args =
   ((Loc.ghost,Name n), Explicit,
-  CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s)),
+  CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None),
 	   args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
-  new_instance binders instance (Some (CRecord (Loc.ghost,None,fields)))
+  new_instance (Flags.is_universe_polymorphism ()) 
+    binders instance (Some (CRecord (Loc.ghost,None,fields)))
     ~global ~generalize:false None
 
 let declare_instance_refl global binders a aeq n lemma =
@@ -1437,51 +1724,49 @@ let proper_projection r ty =
   let ctx, inst = decompose_prod_assum ty in
   let mor, args = destApp inst in
   let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
-  let app = mkApp (Lazy.force proper_proj,
+  let app = mkApp (Lazy.force PropGlobal.proper_proj,
 		  Array.append args [| instarg |]) in
     it_mkLambda_or_LetIn app ctx
 
 let declare_projection n instance_id r =
-  let ty = Global.type_of_global r in
-  let c = constr_of_global r in
+  let c,uctx = Universes.fresh_global_instance (Global.env()) r in
+  let poly = Global.is_polymorphic r in
+  let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in
   let term = proper_projection c ty in
-  let env = Global.env() in
-  let typ = Typing.type_of env Evd.empty term in
+  let typ = Typing.type_of (Global.env ()) Evd.empty term in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n =
       let rec aux t =
 	match kind_of_term t with
-	    App (f, [| a ; a' ; rel; rel' |]) when eq_constr f (Lazy.force respectful) ->
-	      succ (aux rel')
-	  | _ -> 0
+	| App (f, [| a ; a' ; rel; rel' |]) 
+	    when Globnames.is_global (PropGlobal.respectful_ref ()) f ->
+	  succ (aux rel')
+	| _ -> 0
       in
       let init =
 	match kind_of_term typ with
-	    App (f, args) when eq_constr f (Lazy.force respectful) ->
+	    App (f, args) when Globnames.is_global (PropGlobal.respectful_ref ()) f  ->
 	      mkApp (f, fst (Array.chop (Array.length args - 2) args))
 	  | _ -> typ
       in aux init
     in
-    let ctx,ccl = Reductionops.splay_prod_n env Evd.empty (3 * n) typ
+    let ctx,ccl = Reductionops.splay_prod_n (Global.env()) Evd.empty (3 * n) typ
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
-  let cst =
-    { const_entry_body = Future.from_val (term,Declareops.no_seff);
-      const_entry_secctx = None;
-      const_entry_type = Some typ;
-      const_entry_opaque = false;
-      const_entry_inline_code = false;
-      const_entry_feedback = None;
-  } in
-    ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
+  let cst = 
+    Declare.definition_entry ~types:typ ~poly ~univs:(Univ.ContextSet.to_context uctx) 
+      term 
+  in
+    ignore(Declare.declare_constant n 
+	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
 
 let build_morphism_signature m =
   let env = Global.env () in
-  let m = Constrintern.interp_constr Evd.empty env m in
-  let t = Typing.type_of env Evd.empty m in
-  let evdref = ref (Evd.empty, Evar.Set.empty) in
+  let m,ctx = Constrintern.interp_constr Evd.empty env m in
+  let sigma = Evd.from_env ~ctx env in
+  let t = Typing.type_of env sigma m in
   let cstrs =
     let rec aux t =
       match kind_of_term t with
@@ -1490,21 +1775,19 @@ let build_morphism_signature m =
 	| _ -> []
     in aux t
   in
-  let evars, t', sig_, cstrs = build_signature !evdref env t cstrs None in
-  let _ = evdref := evars in
+  let evars, t', sig_, cstrs = 
+    PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t cstrs None in
+  let evd = ref evars in
   let _ = List.iter
     (fun (ty, rel) ->
       Option.iter (fun rel ->
-	let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
-	let evars,c = new_cstr_evar !evdref env default in
-	  evdref := evars)
+	let default = e_app_poly evd PropGlobal.default_relation [| ty; rel |] in
+	  ignore(e_new_cstr_evar evd env default))
 	rel)
     cstrs
   in
-  let morph =
-    mkApp (Lazy.force proper_type, [| t; sig_; m |])
-  in
-  let evd = solve_constraints env (goalevars !evdref) in
+  let morph = e_app_poly evd PropGlobal.proper_type [| t; sig_; m |] in
+  let evd = solve_constraints env !evd in
   let m = Evarutil.nf_evar evd morph in
     Evarutil.check_evars env Evd.empty evd m; m
 
@@ -1512,12 +1795,10 @@ let default_morphism sign m =
   let env = Global.env () in
   let t = Typing.type_of env Evd.empty m in
   let evars, _, sign, cstrs =
-    build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
+    PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
   in
-  let morph =
-    mkApp (Lazy.force proper_type, [| t; sign; m |])
-  in
-  let evars, mor = resolve_one_typeclass env (fst evars) morph in
+  let evars, morph = app_poly evars PropGlobal.proper_type [| t; sign; m |] in
+  let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
     mor, proper_projection mor morph
 
 let add_setoid global binders a aeq t n =
@@ -1532,6 +1813,7 @@ let add_setoid global binders a aeq t n =
        (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
        (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
+
 let make_tactic name =
   let open Tacexpr in
   let loc = Loc.ghost in
@@ -1541,39 +1823,50 @@ let make_tactic name =
 
 let add_morphism_infer glob m n =
   init_setoid ();
+  let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance = build_morphism_signature m in
+  let ctx = Univ.ContextSet.empty (*FIXME *) in
     if Lib.is_modtype () then
       let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
-				(Entries.ParameterEntry (None,instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+				(Entries.ParameterEntry 
+				 (None,poly,(instance,Univ.UContext.empty),None), 
+				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-	add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
+	add_instance (Typeclasses.new_instance 
+			(Lazy.force PropGlobal.proper_class) None glob 
+			poly (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
-      let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+      let kind = Decl_kinds.Global, poly, 
+	Decl_kinds.DefinitionBody Decl_kinds.Instance 
+      in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
+      let hook _ = function
+	| Globnames.ConstRef cst ->
+	  add_instance (Typeclasses.new_instance 
+			  (Lazy.force PropGlobal.proper_class) None
+			  glob poly (ConstRef cst));
+	  declare_projection n instance_id (ConstRef cst)
+	| _ -> assert false
+      in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind instance
-	      (fun _ -> function
-		Globnames.ConstRef cst ->
-		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
-				   glob (ConstRef cst));
-		  declare_projection n instance_id (ConstRef cst)
-		| _ -> assert false);
+	    Lemmas.start_proof instance_id kind (instance, ctx) hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
   init_setoid ();
+  let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
     ((Loc.ghost,Name instance_id), Explicit,
     CAppExpl (Loc.ghost,
-	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper")),
+	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-    ignore(new_instance ~global:glob binders instance (Some (CRecord (Loc.ghost,None,[])))
+    ignore(new_instance ~global:glob poly binders instance (Some (CRecord (Loc.ghost,None,[])))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
 
 (** Bind to "rewrite" too *)
@@ -1601,22 +1894,24 @@ let check_evar_map_of_evars_defs evd =
          check_freemetas_is_empty rebus2 freemetas2
    ) metas
 
-let unification_rewrite l2r c1 c2 cl car rel but env =
+let unification_rewrite flags l2r c1 c2 cl car rel but gl =
+  let env = pf_env gl in
+  let evd = Evd.merge (project gl) cl.evd in
   let (evd',c') =
     try
       (* ~flags:(false,true) to allow to mark occurrences that must not be
          rewritten simply by replacing them with let-defined definitions
          in the context *)
-      Unification.w_unify_to_subterm
+      Unification.w_unify_to_subterm 
        ~flags:{ rewrite_unif_flags with Unification.resolve_evars = true } env
-        cl.evd ((if l2r then c1 else c2),but)
+        evd ((if l2r then c1 else c2),but)
     with
 	Pretype_errors.PretypeError _ ->
 	  (* ~flags:(true,true) to make Ring work (since it really
              exploits conversion) *)
-	  Unification.w_unify_to_subterm
-	  ~flags:{ rewrite2_unif_flags with Unification.resolve_evars = true }
-	    env cl.evd ((if l2r then c1 else c2),but)
+	  Unification.w_unify_to_subterm 
+	  ~flags:{ flags with Unification.resolve_evars = true }
+	    env evd ((if l2r then c1 else c2),but)
   in
   let cl' = {cl with evd = evd'} in
   let cl' = Clenvtac.clenv_pose_dependent_evars true cl' in
@@ -1626,51 +1921,60 @@ let unification_rewrite l2r c1 c2 cl car rel but env =
   and car = nf car and rel = nf rel in
   check_evar_map_of_evars_defs cl'.evd;
   let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in
-  let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
-  let abs = (prf, prfty) in
-  abs, {cl=cl'; ext=Evar.Set.empty; prf=(mkRel 1); car=car; rel=rel;
-     c1=c1; c2=c2; c=None; abs=true; }
+  let sort = sort_of_rel env evd' (pf_concl gl) in
+  let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty;
+    evd = Evd.diff cl'.evd (project gl) } 
+  in
+    {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; 
+     c1=c1; c2=c2; c=None; abs=Some (prf, prfty); sort = Sorts.is_prop sort; flags = flags}
 
 let get_hyp gl evars (c,l) clause l2r =
-  let env = pf_env gl in
-  let hi = decompose_applied_relation env evars None (c,l) in
+  let flags = rewrite2_unif_flags in
+  let hi = decompose_applied_relation (pf_env gl) evars evars flags None (c,l) l2r in
   let but = match clause with
-    | Some id -> pf_get_hyp_typ gl id
+    | Some id -> pf_get_hyp_typ gl id 
     | None -> Evarutil.nf_evar evars (pf_concl gl)
   in
-  unification_rewrite l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but env
+  let unif = unification_rewrite flags hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl in
+    { unif with flags = rewrite_unif_flags }
 
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
+let apply_lemma gl (c,l) cl l2r occs =
+  let sigma = project gl in
+  let hypinfo = ref (get_hyp gl sigma (c,l) cl l2r) in
+  let app = apply_rule hypinfo None occs in
+  let rec aux () =
+    Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
+  in !hypinfo, aux ()
+
+
+let cl_rewrite_clause_tac abs strat meta cl gl =
+  cl_rewrite_clause_tac ~abs strat meta cl gl
+
+(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *)
+(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
+
 let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
-  let app = apply_rule l2r rewrite_unif_flags None occs in
-  let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
-  let substrat = Strategies.fix recstrat in
-  let abs, hypinfo = get_hyp gl (project gl) (c,l) cl l2r in
-  let strat () env avoid t ty cstr evars =
-    let _, res = substrat (hypinfo, 0) env avoid t ty cstr evars in
-    (), res
-  in
+  let meta = Evarutil.new_meta() in
+  let hypinfo, strat = apply_lemma gl (c,l) cl l2r occs in
     try
-      (tclWEAK_PROGRESS
+      tclWEAK_PROGRESS 
 	(tclTHEN
-           (Refiner.tclEVARS hypinfo.cl.evd)
-	   (cl_rewrite_clause_tac ~abs:(Some abs) strat cl))) gl
+           (Refiner.tclEVARS (Evd.merge (project gl) hypinfo.cl.evd))
+	   (cl_rewrite_clause_tac hypinfo.abs strat (mkMeta meta) cl)) gl
     with RewriteFailure e ->
-      let {c1=x; c2=y} = hypinfo in
+      let {l2r=l2r; c1=x; c2=y} = hypinfo in
 	raise (Pretype_errors.PretypeError
 		  (pf_env gl,project gl,
 		  Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl)))
 
-open Proofview.Notations
-
 let general_s_rewrite_clause x =
+  init_setoid ();
+  fun b occs cl ~new_goals ->
   match x with
-    | None -> general_s_rewrite None
-    | Some id -> general_s_rewrite (Some id)
-let general_s_rewrite_clause x y z w ~new_goals =
-  newtactic_init_setoid () <*>
-  Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals)
+    | None -> Proofview.V82.tactic (general_s_rewrite None b occs cl ~new_goals)
+    | Some id -> Proofview.V82.tactic (general_s_rewrite (Some id) b occs cl ~new_goals)
 
 let _ = Hook.set Equality.general_rewrite_clause general_s_rewrite_clause
 
@@ -1682,63 +1986,61 @@ let not_declared env ty rel =
 
 let setoid_proof ty fn fallback =
   Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
     let concl = Proofview.Goal.concl gl in
-    Proofview.tclORELSE
-      begin
-        try
-          let rel, args = decompose_app_rel env sigma concl in
-          let evm = sigma in
-          let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
-          fn env evm car rel
-        with e -> Proofview.tclZERO e
-      end
-      begin function
-        | e ->
-            Proofview.tclORELSE
-              fallback
-              begin function
-                | Hipattern.NoEquationFound ->
-                (* spiwack: [Errors.push] here is unlikely to do what
-                   it's intended to, or anything meaningful for that
-                   matter. *)
-                    let e = Errors.push e in
-	            begin match e with
-	            | Not_found ->
-	                let rel, args = decompose_app_rel env sigma concl in
-		        not_declared env ty rel
-	            | _ -> Proofview.tclZERO e
-                    end
-                | e' -> Proofview.tclZERO e'
-              end
-      end
+    try
+      let rel, args = decompose_app_rel env sigma concl in
+      let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env sigma rel)))) in
+      Proofview.V82.tactic (fn env sigma car rel)
+    with e when Errors.noncritical e ->
+      Proofview.tclORELSE fallback (function
+      | Hipattern.NoEquationFound ->
+          let e = Errors.push e in
+	  begin match e with
+	  | Not_found ->
+	      let rel, args = decompose_app_rel env sigma concl in
+		not_declared env ty rel
+	  | _ -> raise e
+          end
+      | e -> Proofview.tclZERO e)
   end
 
+let tac_open ((evm,_), c) tac = 
+  tclTHEN (Refiner.tclEVARS evm) (tac c)
+
+let poly_proof getp gett env evm car rel =
+  if Sorts.is_prop (sort_of_rel env evm rel) then
+    getp env (evm,Evar.Set.empty) car rel
+  else gett env (evm,Evar.Set.empty) car rel
+
 let setoid_reflexivity =
   setoid_proof "reflexive"
-    (fun env evm car rel -> Proofview.V82.tactic (apply (get_reflexive_proof env evm car rel)))
+    (fun env evm car rel -> 
+      tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof
+		  env evm car rel) apply)
     (reflexivity_red true)
 
 let setoid_symmetry =
   setoid_proof "symmetric"
-    (fun env evm car rel -> Proofview.V82.tactic (apply (get_symmetric_proof env evm car rel)))
+    (fun env evm car rel -> 
+      tac_open (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof
+		  env evm car rel) apply)
     (symmetry_red true)
 
 let setoid_transitivity c =
   setoid_proof "transitive"
     (fun env evm car rel ->
-      Proofview.V82.tactic begin
-        let proof = get_transitive_proof env evm car rel in
-        match c with
-        | None -> eapply proof
-        | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ])
-      end)
+      let proof = poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof
+	env evm car rel in
+	match c with
+	| None -> tac_open proof eapply
+	| Some c -> tac_open proof (fun t -> apply_with_bindings (t,ImplicitBindings [ c ])))
     (transitivity_red true c)
-
+    
 let setoid_symmetry_in id =
-  Proofview.Goal.enter begin fun gl ->
-  let ctype = Tacmach.New.of_old (fun gl -> pf_type_of gl (mkVar id)) gl in
+  Proofview.V82.tactic (fun gl ->
+  let ctype = pf_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum ctype in
   let (equiv, args) = decompose_app concl in
   let rec split_last_two = function
@@ -1750,12 +2052,81 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-    Tacticals.New.tclTHENS (Tactics.cut new_hyp)
-      [ Proofview.V82.tactic (intro_replacing id);
-	Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Tactics.assumption ] ]
-  end
+    tclTHENS (Proofview.V82.of_tactic (Tactics.cut new_hyp))
+      [ intro_replacing id;
+	tclTHENLIST [ Proofview.V82.of_tactic intros; Proofview.V82.of_tactic setoid_symmetry; apply (mkVar id); Proofview.V82.of_tactic Tactics.assumption ] ]
+      gl)
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
 let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
 let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
+
+let implify id gl =
+  let (_, b, ctype) = pf_get_hyp gl id in
+  let binders,concl = decompose_prod_assum ctype in
+  let evm, ctype' =
+    match binders with
+    | (_, None, ty as hd) :: tl when noccurn 1 concl ->
+	let env = Environ.push_rel_context tl (pf_env gl) in
+	let sigma = project gl in
+	let tyhd = Typing.type_of env sigma ty
+	and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in
+	let ((sigma,_), app), unfold = 
+	  PropGlobal.arrow_morphism (sigma, Evar.Set.empty) tyhd 
+	    (subst1 mkProp tyconcl) ty (subst1 mkProp concl) 
+	in
+	  sigma, it_mkProd_or_LetIn app tl
+    | _ -> project gl, ctype
+  in tclTHEN (Refiner.tclEVARS evm) (Tacmach.convert_hyp (id, b, ctype')) gl
+
+let rec fold_matches env sigma c =
+  map_constr_with_full_binders Environ.push_rel 
+    (fun env c ->
+      match kind_of_term c with
+      | Case _ ->
+          let cst, env, c', _eff = fold_match ~force:true env sigma c in
+	    fold_matches env sigma c'
+      | _ -> fold_matches env sigma c)
+    env c
+
+let fold_match_tac c gl =
+  let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in
+  let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in
+    change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl
+
+let fold_matches_tac c gl =
+  let c' = fold_matches (pf_env gl) (project gl) c in
+  (* let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in *)
+    change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl
+
+let myapply id l gl =
+  let gr = id in
+  let _, impls = List.hd (Impargs.implicits_of_global gr) in
+  let env = pf_env gl in
+  let evars = ref (project gl) in
+  let evd, ty = fresh_global env !evars gr in
+  let _ = evars := evd in
+  let app =
+    let rec aux ty impls args args' =
+      match impls, kind_of_term ty with
+      | Some (_, _, (_, _)) :: impls, Prod (n, t, t') ->
+	let arg = Evarutil.e_new_evar evars env t in
+	  aux (subst1 arg t') impls args (arg :: args')
+      | None :: impls, Prod (n, t, t') ->
+	(match args with
+	| [] ->
+	  if dependent (mkRel 1) t' then
+	    let arg = Evarutil.e_new_evar evars env t in
+	      aux (subst1 arg t') impls args (arg :: args')
+	  else
+	    let arg = Evarutil.mk_new_meta () in
+	      evars := meta_declare (destMeta arg) t !evars;
+	      aux (subst1 arg t') impls args (arg :: args')
+	| arg :: args -> 
+	  aux (subst1 arg t') impls args (arg :: args'))
+      | _, _ -> mkApp (Universes.constr_of_global gr, Array.of_list (List.rev args'))
+    in aux ty impls l []
+  in
+    tclTHEN (Refiner.tclEVARS !evars) (apply app) gl
+