[Matita] speedup delift

Enrico Tassi tassi at cs.unibo.it
Thu Sep 23 15:00:34 CEST 2010


The delift function does a lot of work even if the metavariable is being
instantiated with a closed term. This is very often the case when the
term is suggested by hints. Hints may suggest constants in partially
unfolded form (see paper submitted to Type09), that can thus be very
big. This simple patch speeds up delift in this case.

Cheers
-- 
Enrico Tassi
-------------- next part --------------
A non-text attachment was scrubbed...
Name: a.diff
Type: text/x-diff
Size: 2029 bytes
Desc: not available
URL: <http://www.cs.unibo.it/pipermail/matita/attachments/20100923/756916c2/attachment.diff>


More information about the Matita mailing list