[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: latex problem
> The enclosed file does not compile under latex.
> Latexing the pvs-files.tex file, which includes Track.tex, produces:
As you can see by looking at the LaTeX code it produces, the
ERGO-generated PVS LaTeX-printer is pretty messy. We're going to
replace it completely in the next release and I'm afraid we're not
going to fix problems in the current one. If you ignore the error
messages, the output is usually ok, and imperfections can be edited by
hand for the final run.
Depending on the LaTeX you're using, you may need the variant
pvs.sty file that is in the help archive.