diff options
| author | Pierre-Marie Pédrot | 2016-05-03 18:23:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-03 18:47:57 +0200 |
| commit | 29697585836c6e0e4d91e28a13c3f40d2137208b (patch) | |
| tree | d9069da681f1e3ebfbaf7306a76baa2fe3551732 /kernel/nativecode.ml | |
| parent | b6e796a8ef956fa25bfeba84545f25b2cfb3aaf9 (diff) | |
Fix bug #4707: clearbody much slower in 8.5pl1.
We only retype hypotheses and conclusion when they do depend on the cleared
identifier. This saves a lot of time.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions