← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/refman/RefMan-add.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/refman/RefMan-add.tex
 
1
\chapter[List of additional documentation]{List of additional documentation\label{Addoc}}
 
2
 
 
3
\section[Tutorials]{Tutorials\label{Tutorial}}
 
4
A companion volume to this reference manual, the \Coq\ Tutorial, is
 
5
aimed at gently introducing new users to developing proofs in \Coq\
 
6
without assuming prior knowledge of type theory. In a second step, the
 
7
user can read also the tutorial on recursive types (document {\tt
 
8
RecTutorial.ps}).
 
9
 
 
10
\section[The \Coq\ standard library]{The \Coq\ standard library\label{Addoc-library}}
 
11
A brief description of the \Coq\ standard library is given in the additional
 
12
document {\tt Library.dvi}.
 
13
 
 
14
\section[Installation and un-installation procedures]{Installation and un-installation procedures\label{Addoc-install}}
 
15
A \verb!INSTALL! file in the distribution explains how to install
 
16
\Coq.
 
17
 
 
18
\section[{\tt Extraction} of programs]{{\tt Extraction} of programs\label{Addoc-extract}}
 
19
{\tt Extraction} is a package offering some special facilities to
 
20
extract ML program files. It is described in the separate document
 
21
{\tt Extraction.dvi}
 
22
\index{Extraction of programs}
 
23
 
 
24
\section[{\tt Program}]{A tool for {\tt Program}-ing\label{Addoc-program}}
 
25
{\tt Program} is a package offering some special facilities to
 
26
extract ML program files. It is described in the separate document
 
27
{\tt Program.dvi}
 
28
\index{Program-ing}
 
29
 
 
30
\section[Proof printing in {\tt Natural} language]{Proof printing in {\tt Natural} language\label{Addoc-natural}}
 
31
{\tt Natural} is a tool to print proofs in natural language.
 
32
It is described in the separate document {\tt Natural.dvi}.
 
33
\index{Natural@{\tt Print Natural}}
 
34
\index{Printing in natural language}
 
35
 
 
36
\section[The {\tt Omega} decision tactic]{The {\tt Omega} decision tactic\label{Addoc-omega}}
 
37
{\bf Omega} is a tactic to automatically solve arithmetical goals in
 
38
Presburger arithmetic (i.e. arithmetic without multiplication). 
 
39
It is described in the separate document {\tt Omega.dvi}.
 
40
\index{Omega@{\tt Omega}}
 
41
 
 
42
\section[Simplification on rings]{Simplification on rings\label{Addoc-polynom}}
 
43
A documentation of the package {\tt polynom} (simplification on rings)
 
44
can be found in the document {\tt Polynom.dvi}
 
45
\index{Polynom@{\tt Polynom}}
 
46
\index{Simplification on rings}
 
47
 
 
48
%\section[Anomalies]{Anomalies\label{Addoc-anomalies}}
 
49
%The separate document {\tt Anomalies.*} gives a list of known
 
50
%anomalies and bugs of the system.  Before communicating us an
 
51
%anomalous behavior, please check first whether it has been already
 
52
%reported in this document.
 
53
 
 
54
% $Id: RefMan-add.tex 10061 2007-08-08 13:14:05Z msozeau $ 
 
55
 
 
56
 
 
57
%%% Local Variables: 
 
58
%%% mode: latex
 
59
%%% TeX-master: "Reference-Manual"
 
60
%%% End: