Partly reverting r14539 about fully expanding "let-in"s and not just

expanding them up to the last Var/Rel they are aliased to.

The analysis made in r14539 about ill-typed pattern-unification in bug
however, when abstracting over a "let-in" (in solve_pattern_eqn), the
alias must be preserved for ensuring the correctness of typing.

In short, "let-in"s are back considered for pattern-unification as
constants of which we don't want to know the content but
solve_pattern_eqn now takes into account that they have a value.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14568 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions