Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).

Use two ways to solve it:
- added a whd_betaiota in solve_simple_eqn (since evarconv itself
  refuses beta to preserve the opportunities of first-order-matching
  expressions of the form "(fun x => P) t"; an advantage of this
  whd_betaiota is also that it may simplify K-redexes.
- also added a last-chance test in case of failing occur-check by
  trying to fully head-normalize (with delta) the right-hand-side
  (allows to solve for instance "?n = id ?n" where id is a constant
  (a bridled form of solve_refl that use fconv instead of evar_conv_x).
Incidentally improved a bit the rendering of the type of generalized
terms in pattern-matching by using whd_betaiota.

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

0 files changed, 0 insertions, 0 deletions