coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Aurore Collomb <aurorecollomb AT chez.com>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] coq-tex
- Date: Thu, 22 Jan 2004 19:42:32 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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/
- [Coq-Club] coq-tex, Aurore Collomb
Archive powered by MhonArc 2.6.16.