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

Latex printing. a problem.



Hello,

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)
(spec_u7.tex
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.
Mauro.