abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Fix tactic tests #62

Closed robblanco closed 8 years ago

robblanco commented 8 years ago

Continuing the work described in #57, this series of commits revisits the tests on tactics to make them build and run once again. Each commit focuses on one separate problem, and should be easy to review separately.

The sub-collections of tests on search and unfold deserve special mention. Here, changes to module interfaces have been more profound than elsewhere. In general, the simplest reasonable conversions suffice to get the code to compile and all affected tests to pass, but may not exercise all possible paths and tests to ensure the correctness of these conversions in the general case may be added. See (*TODO*) markers for details.

Once integrated, issues for the new regressions will follow.