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$