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

Latex printing. a problem.


I have problem to transform the .tex file generated by pvs in .dvi files.
iI use the PVS > PRINTING > LATEX-PVS-FILE to generate the pvs, than I lunch "latex  filename.tex" and the latex program starts to complain that

This is TeX, Version 3.14159 (Web2C 7.3.1)
LaTeX2e <2000/06/01>
Babel <v3.7h> and hyphenation patterns for american, french, german, ngerman, n
ohyphenation, loaded.

! LaTeX Error: Environment alltt undefined.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H <return>  for immediate help.
l.35 \begin{alltt}
! Emergency stop.
l.35 \begin{alltt}
No pages of output.
Transcript written on spec_u7.log.
Can you please explain me what is the procedure to produce the dvi file from the tex file generated by PVS?

thanks in advance.