[Matita] speedup delift
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2029 bytes
Desc: not available
More information about the Matita