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