From b6018c78b25da14d4f44cf10de692f968cba1e98 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 12 Dec 2000 22:36:15 +0000
Subject: Initial revision

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-add.tex | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)
 create mode 100755 doc/RefMan-add.tex

(limited to 'doc/RefMan-add.tex')

diff --git a/doc/RefMan-add.tex b/doc/RefMan-add.tex
new file mode 100755
index 0000000000..d04d1468fe
--- /dev/null
+++ b/doc/RefMan-add.tex
@@ -0,0 +1,54 @@
+\chapter{List of additional documentation}\label{Addoc}
+
+\section{Tutorials}\label{Tutorial}
+A companion volume to this reference manual, the \Coq\ Tutorial, is
+aimed at gently introducing new users to developing proofs in \Coq\
+without assuming prior knowledge of type theory. In a second step, the
+user can read also the tutorial on recursive types (document {\tt
+RecTutorial.ps}).
+
+\section{The \Coq\ standard library}\label{Addoc-library}
+A brief description of the \Coq\ standard library is given in the additional
+document {\tt Library.dvi}.
+
+\section{Installation and un-installation procedures}\label{Addoc-install}
+A \verb!INSTALL! file in the distribution explains how to install
+\Coq.
+
+\section{{\tt Extraction} of programs}\label{Addoc-extract}
+{\tt Extraction} is a package offering some special facilities to
+extract ML program files. It is described in the separate document
+{\tt Extraction.dvi}
+\index{Extraction of programs}
+
+\section{Proof printing in {\tt Natural} language}\label{Addoc-natural}
+{\tt Natural} is a tool to print proofs in natural language.
+It is described in the separate document {\tt Natural.dvi}.
+\index{Natural@{\tt Print Natural}}
+\index{Printing in natural language}
+
+\section{The {\tt Omega} decision tactic}\label{Addoc-omega}
+{\bf Omega} is a tactic to automatically solve arithmetical goals in
+Presburger arithmetic (i.e. arithmetic without multiplication). 
+It is described in the separate document {\tt Omega.dvi}.
+\index{Omega@{\tt Omega}}
+
+\section{Simplification on rings}\label{Addoc-polynom}
+A documentation of the package {\tt polynom} (simplification on rings)
+can be found in the document {\tt Polynom.dvi}
+\index{Polynom@{\tt Polynom}}
+\index{Simplification on rings}
+
+%\section{Anomalies}\label{Addoc-anomalies}
+%The separate document {\tt Anomalies.*} gives a list of known
+%anomalies and bugs of the system.  Before communicating us an
+%anomalous behavior, please check first whether it has been already
+%reported in this document.
+
+% $Id$ 
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
-- 
cgit v1.2.3

