From: Enrico Tassi Date: Thu, 10 Sep 2009 14:41:22 +0000 (+0000) Subject: to me, the problem: X-Git-Tag: make_still_working~3485 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=686f7f4f4444125885bc7ef9e8ec3e0b6f567137;hp=686f7f4f4444125885bc7ef9e8ec3e0b6f567137;p=helm.git to me, the problem: ? t ==?== ?->? where the first ? has an empty local context is always Uncertain... to be fully understood why unification gives Failure. It may be correct if t has type (Rel k). I wrap it in the refiner. ---