\documentclass[a4paper]{faq}
\pagestyle{plain}

% yay les symboles
\usepackage{stmaryrd}
\usepackage{amssymb}

% version et date
\def\faqversion{0.1}

% les macros d'amour
\def\Coq{\textsc{Coq }}

\begin{document}
\bibliographystyle{plain}

%%%%%%% Coq pour les nuls %%%%%%%

\title{Coq for the Clueless\\
  \large(\ifpdf\ref*{lastquestion}\else\protect\ref{lastquestion}\fi
  \ Hints)
}
\author{Florent Kirchner \and Julien Narboux}
\maketitle

%%%%%%%

\begin{abstract}
This note intends to provide an easy way to get aquainted with the
\Coq theorem prover. It tries to formulate appropriate answers
to some of the questions any newcommers will face, and to give
pointers to other references when possible.
\end{abstract}

%%%%%%%

\begin{multicols}{2}
\tableofcontents
\end{multicols}

%%%%%%%

\newpage
\section{Introduction}
This FAQ is the sum of the questions that came to mind as we developed
proofs in \Coq. Since we are singularly short-minded, we wrote the
answers we found on bits of papers to have them at hand whenever the
situation occurs again. This, is the result of that: a collection of
tips one can refer to when proofs become intricate. Yes, this means we
won't take the blame for the shortcomings of the following. But if you
want to contribute and send in your own tricks, feel free to write to
us...

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Presentation}

\Question[whatiscoq]{What is Coq?} 

\Question[theoremprovers]{What are the other theorem provers?} 

\Question[intuitionnisticlogic]{What is intuitionnistic logic ?}


\section{Documentation}

\Question[coqdocumentation]{Where can I find documentation about Coq ?} 

\Question[coqfaq]{Where can I find this faq on the web ?} 

\Question[coqmailinglist]{Is there any mailing list about Coq ?} 

\Question[coqbook]{Is there any book about Coq ?}


\section{Installation}

\Question[coqlicence]{What is the licence of Coq ?}

\Question[coqsources]{Where can I find the sources of Coq ?}

\Question[platform]{On which platform Coq is available ?}

\Question[nbusers]{How many Coq users are there ?}

\Question[howold]{How old is Coq ?}


\Question[coqexamples]{Where can I find some Coq examples?} 

\Question[relatedtools]{What are the Coq related tools?}

\Question[goal]{What is a goal?}

\Question[ltac]{What is Ltac?}

\Question[metavariable]{What is a meta variable?}

\Question[conjonction]{My goal is a conjonction, how can I prove it ?}

\Question[disjonction]{My goal is a disjonction, how can I prove it ?}

\Question[forall]{My goal is an universally quantified statement, how can I prove it ?}

\Question[exist]{My goal is an existential, how can I prove it ?}

\Question[type]{What is Type(i) ?}

\Question[dependanttype]{What is a dependent type ?}

\Question[subgoalsorder]{How can I change the order of the subgoals ?}

\Question[hyphotesisorder]]{How can I change the order of the hyphothesis ?}

\Question[ifsyntax]{What is the syntax for if ?}

\Question[letsyntax]{What is the syntax for let ?}

\Question[patternmatchingsyntax]{What is the syntax for pattern matching ?}


\Question[reflexivity]{What is reflexivity ?}




\section{Conclusion and Farewell.}
\label{ccl}

\Question[NoAns]{What if my question isn't answered here ?} 
\label{lastquestion}

Don't panic. You can try the \Coq manual~\cite{Coq:e} for a technical
description of the prover. The Coq'Art~\cite{Coq:coqart} is the first
book written on \Coq and provides a comprehensive review of the
theorem prover as well as a number of example and exercises. Finally,
the tutorial~\cite{Coq:Tutorial} provides a smooth introduction to
theorem proving in \Coq.

%%%%%%%
\newpage
\nocite{LaTeX:intro}
\nocite{LaTeX:symb}
\bibliography{fk}

%%%%%%%

\typeout{*** That makes \thequestion\space questions ***}
\end{document}