Skip to content

Commit

Permalink
fix: locally imported lemmas not being tracked.
Browse files Browse the repository at this point in the history
if a theorem uses a lemma that was locally imported (not previously existing as damf assertion, neither in the same file; but imported from a local file), this lemma was not being tracked as a damf dependency in the published theorem of the main file
  • Loading branch information
innofarah committed Nov 16, 2023
1 parent 11fb44e commit eb49e2c
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/abella.ml
Original file line number Diff line number Diff line change
Expand Up @@ -769,6 +769,7 @@ let import pos filename withs =
| decl :: decls -> begin
match decl with
| CTheorem(name, tys, thm, _) ->
compile (CTheorem (name, tys, thm, Finished)) ;
add_lemma name tys thm ;
process_decls decls
| CDefine(flav, tyargs, idtys, clauses) ->
Expand Down

0 comments on commit eb49e2c

Please sign in to comment.