diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-03 18:23:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-03 18:47:57 +0200 |
| commit | 29697585836c6e0e4d91e28a13c3f40d2137208b (patch) | |
| tree | d9069da681f1e3ebfbaf7306a76baa2fe3551732 /interp/constrintern.mli | |
| 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 'interp/constrintern.mli')
0 files changed, 0 insertions, 0 deletions