The Coq mailing list

[Aurore Collomb <aurorecollomb AT chez.com>]

Bonsoir,

Excusez par avance la question sans interet que je vais pose :

je voudrais utiliser coq-tex . ..

j'ai fait le fichier suivant  test.tex:

\documentclass{llncs}
\begin{document}
\\begin{coq_example}
Require Arith.
Print nat.
\\end{coq_example}
\end{document}

j'ai lance :
  coq-tex test.tex

il m'a dit
Warning: preprocessing with default image "coqtop"
Your version of coqtop seems OK

J'ai obtenu un fichier test.v.tex
mais identique a l'original...

Ou es l'erreur ?
Merci.

Aurore Collomb

--
INRIA - VASY
655 av. de l'Europe
F-38330 Montbonnot Saint-Martin
Tel : 04.76.61.53.37
http://www.inrialpes.fr/vasy/people/Aurore.Collomb/