diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:36:28 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:36:28 +0200 |
commit | 2e4b5351c9bcca1ccba37075fe3873562969fd3e (patch) | |
tree | cf425c23a29e1aaeaa0a81fddbbc9332e0705c37 /proofs/goal.mli | |
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 'proofs/goal.mli')
0 files changed, 0 insertions, 0 deletions