search

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

Regression: Ensure should error on implicit subordination #60

Closed robblanco closed 8 years ago

robblanco commented 8 years ago

From test/test_subordination.ml:

Failure: Abella:3:Subordination:7:Ensure should error on implicit subordination

OUnit: expected exception Failure("Type tm cannot be made subordinate to tp without explicit declaration"), but no exception was not raised.
chaudhuri commented 8 years ago

This is not a bug. We no longer do "implicit subordination" (since a7df40b7e45b8).

chaudhuri commented 8 years ago

Err, maybe we close this after we update the test.

robblanco commented 8 years ago

So the solution is simply to remove that test?

chaudhuri commented 8 years ago

Yeah, perhaps this particular issue is solved by removing the test. However, we need to think up some new tests to cover the new subordination mechanisms. I'll think about it when I have a bit less blood in my caffeine stream.

chaudhuri commented 8 years ago

Ping @yvting in case he is interested.