about summary refs log tree commit diff
path: root/scripts
diff options
context:
space:
mode:
authorEelco Dolstra <e.dolstra@tudelft.nl>2005-07-19T11·48+0000
committerEelco Dolstra <e.dolstra@tudelft.nl>2005-07-19T11·48+0000
commit0f827cc6076ae3c395537a0c9bd806b0d42947c2 (patch)
tree13c7e2090562d1e2cb02aade854a7599f4072275 /scripts
parent2135e7c0417b366b4161d01ebf794d25e96b61ba (diff)
* Prevent repeated wrapping of closed terms
  (closed(closed(closed(...)))) since this reduces performance by
  producing bigger terms and killing caching (which incidentally also
  prevents useful infinite recursion detection).

Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions