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

Re: removing file from context



Hi Hanne,

This sounds like a bug to me; I'll try to recreate it.
In the meantime, you should be able to work around this problem
by exiting PVS and removing the .pvscontext file before restarting.

Regards,
Sam

> I saved a theory file under the wrong name (!) and now that I've got it
> with the right name and have deleted the wrongly named file, quit pvs,
> removed all the binaries and restarted pvs, it still insists that the
> theory already exists in another file. 
> 
> I guess I somehow need that wrongly named file out of the context, but
> how?
> 
> Thanks,
> Hanne
> ---------------------------------------------------------
> Hanne Gottliebsen		    Office P337
> Dept. of Computer Science	    Ph: +44 1334 46 3265
> University of St Andrews	    hago@dcs.st-and.ac.uk
>   - I want a single-skin cotton tent like Mr Weasley's
> ---------------------------------------------------------