aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
commit28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch)
tree63cdf18cd47260eb90550f62f7b22e2e2e208f6c /doc
parent744e7f6a319f4d459a3cc2309f575d43041d75aa (diff)
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rwxr-xr-xdoc/stdlib/Library.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index ee14589cf..fffcddc85 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -1,4 +1,4 @@
-\documentclass[11pt]{article}
+\documentclass[11pt]{report}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
@@ -19,7 +19,7 @@ General Public License Version 2.1.}
\tableofcontents
\newpage
-\section*{The \Coq\ standard library}
+% \section*{The \Coq\ standard library}
This document is a short description of the \Coq\ standard library.
This library comes with the system as a complement of the core library