search

abella-prover / abella

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

fix: damf context elements from local imports #150

Closed innofarah closed 1 year ago

innofarah commented 1 year ago

relevant damf context elements (Kind, Type, Define, etc..) were not being considered and added to the compiled damf formulas contexts if they're introduced in locally imported files (for example, when we import "ccs_sig", all damf context elements in it were not being considered)

chaudhuri commented 1 year ago

I am not sure this is correct. CImport will pull in the transitive dependencies.

chaudhuri commented 1 year ago

Fixed in c7285e0