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

Dead or untested code in unification with conflict pairs on the left #74

Open robblanco opened 7 years ago

robblanco commented 7 years ago

As I have written elsewhere, during my inspection of the Unify interface I found this condition regarding the treatment of unification errors and their handling, or not, in the various flavors of calls to the main unification function.

My local branch cpairs-error-dead-or-untested illustrates the issue. If everything works, tests should be added to specify when this is exercised.