From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 May 2008 12:39:00 +0000 (+0000)
Subject: Major code semplification and bugs removed (thanks to a better invariant):
X-Git-Tag: make_still_working~5201
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=8097a4b158730b042f2d00bc91419ccae6bb71d5;hp=8097a4b158730b042f2d00bc91419ccae6bb71d5;p=helm.git

Major code semplification and bugs removed (thanks to a better invariant):
small_delta_step always put the terms in WHNF, even if it can do that with delta > 0.
Terms in WHNF, delta=0 that are not head-alpha convertible and tail-machine convertible
are not convertible.
---