diff options
| author | Pierre-Marie Pédrot | 2017-03-27 11:35:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-03-27 12:04:16 +0200 |
| commit | 7fbf2a541fcc36e08ce595b482c2f257f171ab3d (patch) | |
| tree | 9d58edee7156fb10e36e42dec2ee7a082ff516dc /kernel/nativecode.mli | |
| parent | ff996b19faeff112a156f5db6c9ab9f26e855145 (diff) | |
Adding the size of the opaquetab in its representation.
This turned out to be costly in proofs with many abstracted lemmas, as an
important part of the time was passed in the computation of the size of the
opaquetab.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions