From 6cf8d80ac0a9869d97373d6813441eabebce8980 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Feb 2006 13:58:10 +0000
Subject: Nettoyage de l'archive doc et restructuration avant intégration à
 l'archive principale de Coq et publication des sources (HH)

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

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

diff --git a/doc/RefMan-add.tex b/doc/RefMan-add.tex
deleted file mode 100755
index d04d1468fe..0000000000
--- a/doc/RefMan-add.tex
+++ /dev/null
@@ -1,54 +0,0 @@
-\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