diff options
| author | Arnaud Spiwack | 2014-10-16 10:36:28 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 10:36:28 +0200 |
| commit | 2e4b5351c9bcca1ccba37075fe3873562969fd3e (patch) | |
| tree | cf425c23a29e1aaeaa0a81fddbbc9332e0705c37 /kernel/nativecode.ml | |
| parent | e86f8ef50b940435da2b238792dffd0f9755a78d (diff) | |
Make [Goal.goal] be exactly [Evar.t].
First step in removing the [Goal] module whose code is now essentially legacy.
Removes the cache attached to a goal, which was used to avoid unnecessary [nf_evar]. May have a performance cost, which is to be fixed later.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions