From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 24 Jul 2009 21:49:56 +0000 (+0000)
Subject: Beta-expansion was avoided as soon as one argument was flexible.
X-Git-Tag: make_still_working~3622
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53bd7590de050214164c4f6b5181699dc38056f6;hp=53bd7590de050214164c4f6b5181699dc38056f6;p=helm.git

Beta-expansion was avoided as soon as one argument was flexible.
This lead to a different behaviour in the following two unification problems:

   (\lambda_.?) ? =?= T         vs               ? ? =?= T
     or, equivalently
        ?[?] =?= T

The fix is very easy: we always perform beta-expansion and delifting will
take care of ignoring the flexible "arguments", both during beta-expansion
and during the unification that follows.
---