aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-04-10 09:37:16 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-04-10 09:37:16 +0000
commitc0ba300887e44e507a0d1a7e5d642820d76f883f (patch)
treee5bfb86a3c97b2cc286b3a89d4d1ab851c42d5ce /doc
parent969494210a800c9c106829341b7659213396c404 (diff)
package camlindent inutilise
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r--doc/newsyntax.tex1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex
index a85a1fe37..0e2c096f5 100644
--- a/doc/newsyntax.tex
+++ b/doc/newsyntax.tex
@@ -4,7 +4,6 @@
\documentclass{article}
\usepackage{verbatim}
-\usepackage{camlindent}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage[french]{babel}