From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 6 Apr 2009 15:43:14 +0000 (+0000)
Subject: unification:
X-Git-Tag: make_still_working~4115
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d174e54c365ab9df38367de9336c213a03be3c27;hp=d174e54c365ab9df38367de9336c213a03be3c27;p=helm.git

unification:
 - the case

    (? args) v.s. ?(tag:OUT_SCOPE)

   is considered as a pattern-driven delifting.
 - the case ? args v.s. t is reduced to ?[args] v.s. t
 - eta-contraction reimplemented
 - beta-expand no longer used

delift:
 - handle out/in scope tag

ntactics:
 - elim sets the out_scope tag for 1 entry
---