← Back to branch summary

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

« back to all changes in this revision

Viewing changes to 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:
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
 
 
18
 
\usepackage{ifpdf}
19
 
 
20
 
% for coqide
21
 
\ifpdf   % si on est pas en pdflatex
22
 
  \usepackage[pdftex]{graphicx}
23
 
\else
24
 
  \usepackage[dvips]{graphicx}
25
 
\fi
26
 
 
27
 
 
28
 
%\includeonly{RefMan-gal.v,RefMan-ltac.v,RefMan-lib.v,Cases.v}
29
 
 
30
 
\input{../common/version.tex}
31
 
\input{../common/macros.tex}% extension .tex pour htmlgen
32
 
\input{../common/title.tex}% extension .tex pour htmlgen
33
 
\input{./headers.tex}% extension .tex pour htmlgen
34
 
 
35
 
\begin{document}
36
 
%BEGIN LATEX
37
 
\sloppy\hbadness=5000
38
 
%END LATEX
39
 
 
40
 
\tophtml{}
41
 
%BEGIN LATEX
42
 
\coverpage{Reference Manual}{The Coq Development Team}
43
 
  {This material may be distributed only subject to the terms and
44
 
   conditions set forth in the Open Publication License, v1.0 or later
45
 
   (the latest version is presently available at
46
 
   \ahrefurl{http://www.opencontent.org/openpub}).
47
 
   Options A and B of the licence are {\em not} elected.}
48
 
%END LATEX
49
 
 
50
 
%\defaultheaders
51
 
\include{RefMan-int}% Introduction
52
 
\include{RefMan-pre}% Credits
53
 
 
54
 
%BEGIN LATEX
55
 
\tableofcontents
56
 
%END LATEX
57
 
 
58
 
\part{The language}
59
 
\defaultheaders
60
 
\include{RefMan-gal.v}% Gallina
61
 
\include{RefMan-ext.v}% Gallina extensions
62
 
\include{RefMan-lib.v}% The coq library
63
 
\include{RefMan-cic.v}% The Calculus of Constructions
64
 
\include{RefMan-modr}% The module system
65
 
 
66
 
 
67
 
\part{The proof engine}
68
 
\include{RefMan-oth.v}% Vernacular commands
69
 
\include{RefMan-pro}% Proof handling
70
 
\include{RefMan-tac.v}% Tactics and tacticals
71
 
\include{RefMan-ltac.v}% Writing tactics
72
 
\include{RefMan-tacex.v}% Detailed Examples of tactics
73
 
 
74
 
\part{User extensions}
75
 
\include{RefMan-syn.v}% The Syntax and the Grammad commands
76
 
%%SUPPRIME \include{RefMan-tus.v}% Writing tactics
77
 
 
78
 
\part{Practical tools}
79
 
\include{RefMan-com}% The coq commands (coqc coqtop)
80
 
\include{RefMan-uti}% utilities (gallina, do_Makefile, etc)
81
 
\include{RefMan-ide}% Coq IDE
82
 
 
83
 
%BEGIN LATEX
84
 
\RefManCutCommand{BEGINADDENDUM=\thepage}
85
 
%END LATEX
86
 
\part{Addendum to the Reference Manual}
87
 
\include{AddRefMan-pre}%
88
 
\include{Cases.v}%
89
 
\include{Coercion.v}%
90
 
%%SUPPRIME \include{Natural.v}%
91
 
\include{Omega.v}%
92
 
%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs
93
 
\include{Extraction.v}%
94
 
\include{Program.v}%
95
 
\include{Polynom.v}%  = Ring
96
 
\include{Setoid.v}% Tactique pour les setoides
97
 
%BEGIN LATEX
98
 
\RefManCutCommand{ENDADDENDUM=\thepage}
99
 
%END LATEX
100
 
\nocite{*}
101
 
\bibliographystyle{plain}
102
 
\bibliography{biblio}
103
 
\cutname{biblio.html}
104
 
 
105
 
\printindex
106
 
\cutname{general-index.html}
107
 
 
108
 
\printindex[tactic]
109
 
\cutname{tactic-index.html}
110
 
 
111
 
\printindex[command]
112
 
\cutname{command-index.html}
113
 
 
114
 
\printindex[error]
115
 
\cutname{error-index.html}
116
 
 
117
 
%BEGIN LATEX
118
 
\listoffigures
119
 
\addcontentsline{toc}{chapter}{\listfigurename}
120
 
%END LATEX
121
 
 
122
 
\end{document}
123
 
 
124
 
 
125
 
% $Id: Reference-Manual.tex 9038 2006-07-11 13:53:53Z herbelin $