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 /parsing | |
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 'parsing')
0 files changed, 0 insertions, 0 deletions