[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Parsing after changing imported theory

Hi Rob,

This is clearly a bug - could you send me the specs, so I can recreate and
fix it?


> From:    "R. Colvin" <robert@itee.uq.edu.au>
> Subject: [PVS-Help] Parsing after changing imported theory
> Date:    Tue, 26 Oct 2004 12:47:26 +1000
> To:      pvs-help@csl.sri.com
> 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