diff options
author | 2016-06-24 21:23:16 +0200 | |
---|---|---|
committer | 2016-06-24 21:24:39 +0200 | |
commit | a553126c9e0984f38b1a15f2db60458813a177c9 (patch) | |
tree | 3a493b094eeb86d741a38836563f40aa0798d4ed /interp/notation_ops.mli | |
parent | 922ad0c1cb4a4badf4c9c2cd098285a008495519 (diff) | |
parent | 4d4e2f421c1a4f0339568d3c96ff2459a027aa09 (diff) |
Several easy but efficient optimizations for subst and clear tactics.
They were spotted by profiling tactics manipulating huge terms, provided by
Jason Gross.
Diffstat (limited to 'interp/notation_ops.mli')
0 files changed, 0 insertions, 0 deletions