blob: 446ad12848955e1f6b72f05afde62070148826ba (
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
|
TUTORIAL N. Oury
GUIDE PASSAGE V7-V8 BB
MANUEL DE REFERENCE
\include{RefMan-int}% Introduction HH - relu CP
\include{RefMan-pre}% Credits HH - relu CP
\tableofcontents
\part{The language}
\defaultheaders
\include{RefMan-gal.v}% Gallina BB
\include{RefMan-ext.v}% Gallina extensions HH -fait
\include{RefMan-lib.v}% The coq library BB
\include{RefMan-cic.v}% The Calculus of Constructions CP -fait
\include{RefMan-modr}% The module system Jacek
\part{The proof engine}
\include{RefMan-oth.v}% Vernacular commands JCF -fait
\include{RefMan-pro}% Proof handling Clement
\include{RefMan-tac.v}% Tactics and tacticals JCF - fait
%% ajouter JProver/Ground/CC Pierre C -fait
\include{RefMan-tacex.v}% Detailed Examples of tactics JCF - fait
\part{User extensions}
\include{RefMan-syn.v}% The Syntax and the Grammar commands HH
%%SUPPRIME \include{RefMan-tus.v}% Writing tactics
%%REMPLACE PAR
\include{RefMan-ltac.v}% Writing tactics BB -fait
\part{Practical tools}
\include{RefMan-com}% The coq commands (coqc coqtop) HH -fait
%%ajouter nouvelles options -v7 -translate au document de passage
\include{RefMan-uti}% utilities (gallina, do_Makefile, etc) JCF -fait
\include{RefMan-ide}%CoqIde CM
\include{AddRefMan-pre}% CP
\include{Cases.v}% CP -fait
\include{Coercion.v}% HH -fait
%%SUPPRIME \include{Natural.v}%
\include{Omega.v}% JCF - fait
%%Nouvelle version ROmega Pierre Cregut
%%SUPPRIME \include{Program.v}%
%% A SUPPRIMER
%% \include{Correctness.v}% = preuve de pgms imperatifs
\include{Extraction.v}% Pierre L
\include{Polynom.v}% = Ring Julien N
\include{Setoid.v}% Tactique pour les setoides Clement
\addtocontents{sh}{ENDADDENDUM=\thepage}
\nocite{*}
\bibliographystyle{plain}
\bibliography{biblio}
\addtocontents{sh}{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
\addtocontents{sh}{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps}
\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-}
\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM}
\printindex
\printindex[tactic]
\printindex[command]
\printindex[error]
\end{document}
% $Id$
|
