diff options
| author | Pierre-Marie Pédrot | 2014-09-21 20:11:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-21 22:30:45 +0200 |
| commit | eaf864354c3fda9ddc1f03f0b1c7807b6fd44322 (patch) | |
| tree | a84135f0438c2902145080242e6c9faa59b80b6d /kernel/nativelambda.ml | |
| parent | a30a8f484a478e04a7a42526cd6994310c59521d (diff) | |
More invariants in the code of Refine.
The hypinfo state is now refreshed at a proper time, which should reduce the
overall number of calls to [decompose_applied_relation]. The state passing
nature of the program is also more explicit, removing a use of Evd.merge.
This patch should preserve semantics and efficiency.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions