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

Re: [PVS-Help] theory not found error


> The file ln_series.pvs is not in lib/analysis with the latest NASA
> release.  It is in lnexp and lnexp_fnd.  Does your theory say:
>   IMPORTING analysis@ln_series
> ?  If so, you will have to change "analysis" to "lnexp" or "lnexp_fnd",
> whichever is appropriate for you.  If not, you may need to remove
> your .bin files and reprove everything.

As I'm not importing the analysis@ln_series theory, then I removed
the .bin files of my theory and the problem persisted, then
I erased the .bin and reprove the files:


and the problem is solved

(I imported the theory interval_approx that imports ln_approx and the
last one imports ln_series. When I tried to shows the tccs of those
files, I had the same problem than in my theory file, for that reason I
erased his .bin files and reprove them.)

Thank you


Francisco José Cháves (ENS-LIP) 
mailto: Francisco.Jose.Chaves.Alonso@ens-lyon.fr
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36