[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Parsing after changing imported theory
Hi, when I'm editing a theory A that imports B (in a different
file), if I edit B (and typecheck) then return to A, type checking A
sometimes gives the error
Error: the assertion (singleton? resolutions) failed.
and I am prompted
SPC-scroll: I-ignore, K-keep, ..... or B-break:
I usually just press 'I'. Then I make some syntactic error in A
which forces a re-parse of the file. After that type checking works
fine.
Is this perhaps something to do with the way I switch between files
in PVS/emacs?
Thanks,
Rob