blob: a4fdf0cd805be361d049d04fdedb6e4aeb03b8aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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: RefMan-add.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
