summaryrefslogtreecommitdiff
path: root/toplevel/doc.tex
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/doc.tex')
-rw-r--r--toplevel/doc.tex10
1 files changed, 10 insertions, 0 deletions
diff --git a/toplevel/doc.tex b/toplevel/doc.tex
new file mode 100644
index 00000000..f2550fda
--- /dev/null
+++ b/toplevel/doc.tex
@@ -0,0 +1,10 @@
+
+\newpage
+\section*{The Coq toplevel}
+
+\ocwsection \label{toplevel}
+This chapter describes the highest modules of the \Coq\ system.
+They are organized as follows:
+
+\bigskip
+\begin{center}\epsfig{file=toplevel.dep.ps,width=\linewidth}\end{center}