[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