v8.4: Turning proofs of well-ordering of lexicographic product transparent
(see discussion on coq-club 5-6 Feb 2012).

(backport of r15059)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15149 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Reorganizing the structure of evarutil.ml (only restructuration, no
change of semantics).

(backport of r15060)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15150 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Generalized the use of evar candidates in type inference unification:
- use evar candidates instead of postponed conversion problems when
  it is known (according to the projection heuristic used) that an
  evar has only a fixed number of possible instances (as e.g. in
  equation ?n[x,x] = x, with x a variable);
- this allows to be more robust in solving remaining problems: if
  several instanciations exist, and one is not compatible with a previous
  instantiation made among several choices for another evar,
  backtracking is now possible;
- this allows in particular to fix regression #2670 (two postponed
  conversion problems solved in an inconsistent way);
- but this requires more code.

At the same time, a refactoring of the code has been made so as to
hopefully clarify the elementary pieces of the algorithm. For
instance, there are now generic functions for both applying a filter
and giving candidates. The filter is systematically generalized so as
to have the ccl of the evar well-typed even in situations where we
could try on the contrary to restrict the evars occurring in the
ccl.

Anyway, when the representation of instances will be optimized using
identity substitutions, it will no longer be useful to use the filter
to shorten the size of the instances. Then, the filters will have,
like candidates, the only role of restricting the search space for
potential solutions to the unification problems.

Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un]
up to conversion instead of up to unification. This (potententially)
looses constraints but this avoids looping at the time of considering
remaining problems and applying heuristics to them.

Also added printing of evar candidates in debugging evar printers

(backport of 15061)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15151 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep a
candidate for the possible projection (as was introduced in 8.4beta)
but try also to imitate (as was done before 8.4beta but not done in
8.4beta).

(backport of r15062)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15152 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Force Check (which, from 8.4beta, accepts unresolved evars) to however
try to solve remaining constraints.

(backport of r15063)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15153 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Use a careful analysis of dependencies in restricting instances to
solve the following kind of code broken by being less restrictive on
projecting:

Set Printing Existential Instances.
Parameter f : forall x, x=0 -> x=0 -> x=1 /\ x=2.
Parameter g : forall y, y=0 /\ y=0.
Check match g _ with conj a b => f _ a b end.
(* and the return clause should not depend on the "_" *)

(backport of r15064)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15154 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Unification: Added a heuristic to solve problems of the form
?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to
know if it occurs in rigid position or not. Such equations typically
come from matching problems such as "match a return ?T[a] with pair a1
a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the
return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified
with ?A.  This possible dependency is kept since commits r15060-15062.
The heuristic is to restrict ?T so that the dependency is removed,
leading to a behavior similar to the one existing before these commits.

This allows BGsection15.v, from contrib Ssreflect, to compile as it
did before these commits.

Also, removed one function exported without true need in r15061.

(backport of r15092)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15155 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Unification: Fixing bug in materialize_evar (spotted by MathClasses).
Also fixed apparent other bug in the presence of let-ins.

(backport of r15099)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15156 85f007b7-540e-0410-9357-904b9bb8a0f7