← Back to branch summary

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

« back to all changes in this revision

Viewing changes to doc/refman/Reference-Manual.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/Reference-Manual.tex
 
1
%\RequirePackage{ifpdf}
 
2
%\ifpdf
 
3
%  \documentclass[11pt,a4paper,pdftex]{book}
 
4
%\else
 
5
  \documentclass[11pt,a4paper]{book}
 
6
%\fi
 
7
 
 
8
\usepackage[latin1]{inputenc}
 
9
\usepackage[T1]{fontenc}
 
10
\usepackage{times}
 
11
\usepackage{url}
 
12
\usepackage{verbatim}
 
13
\usepackage{amsmath}
 
14
\usepackage{amssymb}
 
15
\usepackage{alltt}
 
16
\usepackage{hevea}
 
17
\usepackage{ifpdf}
 
18
\usepackage[headings]{fullpage}
 
19
\usepackage{headers} % in this directory
 
20
\usepackage{multicol}
 
21
\usepackage{xspace}
 
22
 
 
23
% for coqide
 
24
\ifpdf   % si on est pas en pdflatex
 
25
  \usepackage[pdftex]{graphicx}
 
26
\else
 
27
  \usepackage[dvips]{graphicx}
 
28
\fi
 
29
 
 
30
 
 
31
%\includeonly{Setoid}
 
32
 
 
33
\input{../common/version.tex}
 
34
\input{../common/macros.tex}% extension .tex pour htmlgen
 
35
\input{../common/title.tex}% extension .tex pour htmlgen
 
36
%\input{headers}
 
37
 
 
38
\usepackage[linktocpage,colorlinks,bookmarks=false]{hyperref}
 
39
% The manual advises to load hyperref package last to be able to redefine
 
40
% necessary commands.
 
41
% The above should work for both latex and pdflatex. Even if PDF is produced
 
42
% through DVI and PS using dvips and ps2pdf, hyperlinks should still work.
 
43
% linktocpage option makes page numbers, not section names, to be links in
 
44
% the table of contents.
 
45
% colorlinks option colors the links instead of using boxes.
 
46
\begin{document}
 
47
%BEGIN LATEX
 
48
\sloppy\hbadness=5000
 
49
%END LATEX
 
50
 
 
51
%BEGIN LATEX
 
52
\coverpage{Reference Manual}
 
53
{The Coq Development Team}
 
54
{This material may be distributed only subject to the terms and
 
55
conditions set forth in the Open Publication License, v1.0 or later
 
56
(the latest version is presently available at
 
57
\url{http://www.opencontent.org/openpub}).
 
58
Options A and B of the licence are {\em not} elected.}
 
59
%END LATEX
 
60
 
 
61
%\defaultheaders
 
62
\include{RefMan-int}% Introduction
 
63
\include{RefMan-pre}% Credits
 
64
 
 
65
%BEGIN LATEX
 
66
\tableofcontents
 
67
%END LATEX
 
68
 
 
69
\part{The language}
 
70
%BEGIN LATEX
 
71
\defaultheaders
 
72
%END LATEX
 
73
\include{RefMan-gal.v}% Gallina
 
74
\include{RefMan-ext.v}% Gallina extensions
 
75
\include{RefMan-lib.v}% The coq library
 
76
\include{RefMan-cic.v}% The Calculus of Constructions
 
77
\include{RefMan-modr}% The module system
 
78
 
 
79
 
 
80
\part{The proof engine}
 
81
\include{RefMan-oth.v}% Vernacular commands
 
82
\include{RefMan-pro}% Proof handling
 
83
\include{RefMan-tac.v}% Tactics and tacticals
 
84
\include{RefMan-ltac.v}% Writing tactics
 
85
\include{RefMan-tacex.v}% Detailed Examples of tactics
 
86
\include{RefMan-decl.v}% The mathematical proof language
 
87
 
 
88
\part{User extensions}
 
89
\include{RefMan-syn.v}% The Syntax and the Grammad commands
 
90
%%SUPPRIME \include{RefMan-tus.v}% Writing tactics
 
91
 
 
92
\part{Practical tools}
 
93
\include{RefMan-com}% The coq commands (coqc coqtop)
 
94
\include{RefMan-uti}% utilities (gallina, do_Makefile, etc)
 
95
\include{RefMan-ide}% Coq IDE
 
96
 
 
97
%BEGIN LATEX
 
98
\RefManCutCommand{BEGINADDENDUM=\thepage}
 
99
%END LATEX
 
100
\part{Addendum to the Reference Manual}
 
101
\include{AddRefMan-pre}%
 
102
\include{Cases.v}%
 
103
\include{Coercion.v}%
 
104
\include{Classes.v}%
 
105
%%SUPPRIME \include{Natural.v}%
 
106
\include{Omega.v}%
 
107
\include{Micromega.v}
 
108
%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs
 
109
\include{Extraction.v}%
 
110
\include{Program.v}%
 
111
\include{Polynom.v}%  = Ring
 
112
\include{Setoid.v}% Tactique pour les setoides
 
113
\include{ExternalProvers}% Tactiques appelant des prouveurs externes
 
114
%BEGIN LATEX
 
115
\RefManCutCommand{ENDADDENDUM=\thepage}
 
116
%END LATEX
 
117
\nocite{*}
 
118
\bibliographystyle{plain}
 
119
\bibliography{biblio}
 
120
\cutname{biblio.html}
 
121
 
 
122
\printindex
 
123
\cutname{general-index.html}
 
124
 
 
125
\printindex[tactic]
 
126
\cutname{tactic-index.html}
 
127
 
 
128
\printindex[command]
 
129
\cutname{command-index.html}
 
130
 
 
131
\printindex[error]
 
132
\cutname{error-index.html}
 
133
 
 
134
%BEGIN LATEX
 
135
\listoffigures
 
136
\addcontentsline{toc}{chapter}{\listfigurename}
 
137
%END LATEX
 
138
 
 
139
\end{document}
 
140
 
 
141
 
 
142
% $Id: Reference-Manual.tex 11306 2008-08-05 16:51:08Z notin $