diff options
| author | Pierre-Marie Pédrot | 2016-06-20 08:40:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-20 08:53:39 +0200 |
| commit | b0ffad7f20114875611132dfffb9517d6f5b9ff9 (patch) | |
| tree | 7b9eef41c1d081e1ab21aad510d03c5ad3b77641 /dev | |
| parent | a7d95a6923960ad551314d3e72715f9ad766cffd (diff) | |
Small optimization in clear_body.
We do not check that an hypothesis is used in context declarations that
occur before it.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions