diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-24 21:23:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 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