MAJ, divers + section axiomes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8568 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 295 insertions, 250 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 422356c0c..f91490845 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -10,6 +10,7 @@
 \usepackage{fullpage}
 \usepackage[latin1]{inputenc}
 \usepackage[english]{babel}
+\usepackage{graphics}
 
 %\input{../macros.tex}
 
@@ -19,12 +20,12 @@
 \def\faqversion{0.1}
 
 % les macros d'amour
-\def\Coq{\textsc{Coq }}
-\def\Why{\textsc{Why }}
-\def\Caduceus{\textsc{Caduceus }}
-\def\Krakatoa{\textsc{Krakatoa }}
-\def\Ltac{\textsc{Ltac }}
-\def\CoqIde{\textsc{CoqIde }}
+\def\Coq{\textsc{Coq}}
+\def\Why{\textsc{Why}}
+\def\Caduceus{\textsc{Caduceus}}
+\def\Krakatoa{\textsc{Krakatoa}}
+\def\Ltac{\textsc{Ltac}}
+\def\CoqIde{\textsc{CoqIde}}
 
 \newcommand{\coqtt}[1]{{\tt #1}}
 \newcommand{\coqimp}{{\mbox{\tt ->}}}
@@ -32,61 +33,61 @@
 
 
 % macro pour les tactics
-\def\split{{\tt split }}
-\def\assumption{{\tt assumption }}
-\def\auto{{\tt auto }}
-\def\trivial{{\tt trivial }}
-\def\tauto{{\tt tauto }}
-\def\left{{\tt left }}
-\def\right{{\tt right }}
-\def\decompose{{\tt decompose }}
-\def\intro{{\tt intro }}
-\def\intros{{\tt intros }}
-\def\field{{\tt field }}
-\def\ring{{\tt ring }}
-\def\apply{{\tt apply }}
-\def\exact{{\tt exact }}
-\def\cut{{\tt cut }}
-\def\assert{{\tt assert }}
-\def\solve{{\tt solve }}
-\def\idtac{{\tt idtac }}
-\def\fail{{\tt fail }}
-\def\exists{{\tt exists }}
-\def\firstorder{{\tt firstorder }}
-\def\congruence{{\tt congruence }}
-\def\gb{{\tt gb }}
-\def\generalize{{\tt generalize }}
-\def\abstractt{{\tt abstract }}
-\def\eapply{{\tt eapply }}
-\def\unfold{{\tt unfold }}
-\def\rewrite{{\tt rewrite }}
-\def\replace{{\tt replace }}
-\def\simpl{{\tt simpl }}
-\def\elim{{\tt elim }}
-\def\set{{\tt set }}
-\def\pose{{\tt pose }}
-\def\case{{\tt case }}
-\def\destruct{{\tt destruct }}
-\def\reflexivity{{\tt reflexivity }}
-\def\transitivity{{\tt transitivity }}
-\def\symmetry{{\tt symmetry }}
-\def\Focus{{\tt Focus }}
-\def\discriminate{{\tt discriminate }}
-\def\contradiction{{\tt contradiction }}
-\def\intuition{{\tt intuition }}
-\def\try{{\tt try }}
-\def\repeat{{\tt repeat }}
-\def\eauto{{\tt eauto }}
-\def\subst{{\tt subst }}
-\def\symmetryin{{\tt symmetryin }}
-\def\instantiate{{\tt instantiate }}
+\def\split{{\tt split}}
+\def\assumption{{\tt assumption}}
+\def\auto{{\tt auto}}
+\def\trivial{{\tt trivial}}
+\def\tauto{{\tt tauto}}
+\def\left{{\tt left}}
+\def\right{{\tt right}}
+\def\decompose{{\tt decompose}}
+\def\intro{{\tt intro}}
+\def\intros{{\tt intros}}
+\def\field{{\tt field}}
+\def\ring{{\tt ring}}
+\def\apply{{\tt apply}}
+\def\exact{{\tt exact}}
+\def\cut{{\tt cut}}
+\def\assert{{\tt assert}}
+\def\solve{{\tt solve}}
+\def\idtac{{\tt idtac}}
+\def\fail{{\tt fail}}
+\def\existstac{{\tt exists}}
+\def\firstorder{{\tt firstorder}}
+\def\congruence{{\tt congruence}}
+\def\gb{{\tt gb}}
+\def\generalize{{\tt generalize}}
+\def\abstracttac{{\tt abstract}}
+\def\eapply{{\tt eapply}}
+\def\unfold{{\tt unfold}}
+\def\rewrite{{\tt rewrite}}
+\def\replace{{\tt replace}}
+\def\simpl{{\tt simpl}}
+\def\elim{{\tt elim}}
+\def\set{{\tt set}}
+\def\pose{{\tt pose}}
+\def\case{{\tt case}}
+\def\destruct{{\tt destruct}}
+\def\reflexivity{{\tt reflexivity}}
+\def\transitivity{{\tt transitivity}}
+\def\symmetry{{\tt symmetry}}
+\def\Focus{{\tt Focus}}
+\def\discriminate{{\tt discriminate}}
+\def\contradiction{{\tt contradiction}}
+\def\intuition{{\tt intuition}}
+\def\try{{\tt try}}
+\def\repeat{{\tt repeat}}
+\def\eauto{{\tt eauto}}
+\def\subst{{\tt subst}}
+\def\symmetryin{{\tt symmetryin}}
+\def\instantiate{{\tt instantiate}}
 \def\inversion{{\tt inversion}}
-\def\Defined{{\tt Defined }}
-\def\Qed{{\tt Qed }}
-\def\pattern{{\tt pattern }}
-\def\Type{{\tt Type }}
-\def\Prop{{\tt Prop }}
-\def\Set{{\tt Set }}
+\def\Defined{{\tt Defined}}
+\def\Qed{{\tt Qed}}
+\def\pattern{{\tt pattern}}
+\def\Type{{\tt Type}}
+\def\Prop{{\tt Prop}}
+\def\Set{{\tt Set}}
 
 
 \newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}}
@@ -126,7 +127,7 @@
 
 \begin{abstract}
 This note intends to provide an easy way to get acquainted with the
-\Coq theorem prover. It tries to formulate appropriate answers
+{\Coq} theorem prover. It tries to formulate appropriate answers
 to some of the questions any newcomers will face, and to give
 pointers to other references when possible.
 \end{abstract}
@@ -155,16 +156,16 @@ answers, feel free to write to us\ldots
 
 \section{Presentation}
 
-\Question{What is \Coq ?}\label{whatiscoq} 
-The Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. 
-In particular, Coq allows:
+\Question{What is {\Coq} ?}\label{whatiscoq} 
+The {\Coq} tool is a formal proof management system: a proof done with {\Coq} is mechanically checked by the machine. 
+In particular, {\Coq} allows:
 \begin{itemize}
     \item the definition of functions or predicates,
     \item to state mathematical theorems and software specifications,
     \item to develop interactively formal proofs of these theorems,
     \item to check these proofs by a small certification "kernel".
 \end{itemize}
-Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.
+{\Coq} is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.
 
 \Question{Did you really need to name it like that ?}
 Some French computer scientists have a tradition of naming their
@@ -173,10 +174,10 @@ of this tacit convention. In French, ``coq'' means rooster, and it
 sounds like the initials of the Calculus of Constructions CoC on which
 it is based.
 
-\Question{Is \Coq a theorem prover?}
+\Question{Is {\Coq} a theorem prover?}
 
-\Coq comes with a few decision procedures (on propositional
-calculus, Presburger arithmetic, ring and field simplification,
+{\Coq} comes with a few decision procedures (on propositional
+calculus, Presburger's arithmetic, ring and field simplification,
 resolution, ...) but the main style for proving theorems is
 interactively by using LCF-style tactics.
 
@@ -184,8 +185,8 @@ interactively by using LCF-style tactics.
 \Question{What are the other theorem provers ?} 
 Many other theorem provers are available for use nowadays. 
 Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar
-to \Coq by the way they interact with the user. Other relatives of
-\Coq are ACL2, Alfa, Elf, Kiv, Mizar, NqThm, $\Omega$mega\ldots
+to {\Coq} by the way they interact with the user. Other relatives of
+{\Coq} are ACL2, Alfa, Elf, Kiv, Mizar, NqThm, $\Omega$mega\ldots
 
 \Question{What's the status of proofs in \Coq}
 
@@ -194,8 +195,8 @@ reasoning (stating
 
 cannot be accepted without a proof expressed in the Calculus of
 Inductive Constructions. The correctness of a proof relies on a
-relatively small proof-checker at the kernel of \Coq (8000 lines of ML
-code). Even \Coq decision procedures are producing proofs which are
+relatively small proof-checker at the kernel of {\Coq} (8000 lines of ML
+code). Even {\Coq} decision procedures are producing proofs which are
 double-checked by the kernel.
 
 \Question{Who do I have to trust when I see a proof checked by Coq ?}
@@ -212,10 +213,10 @@ You can check your proof using different computers if you feel the need to.
 \end{description}
 
 
-\Question{Where can I find information about the theory behind \Coq ?}
+\Question{Where can I find information about the theory behind {\Coq}?}
 \begin{description}
 \item[Type theory] A book~\cite{ProofsTypes}, some lecture
-notes~\cite{Types:Dowek} and the \Coq manual~\cite{Coq:manual}
+notes~\cite{Types:Dowek} and the {\Coq} manual~\cite{Coq:manual}
 \item[Inductive types]
 Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}
 \item[Co-Inductive types]
@@ -223,32 +224,32 @@ Eduardo Giménez' thesis~\cite{EGThese}
 \end{description}
 
 
-\Question{How can I use \Coq to prove programs ?}
+\Question{How can I use {\Coq} to prove programs ?}
 
 You can either extract a program from a proof use the extraction
 mechanism or use dedicated tools, such as \Why, \Krakatoa, \Caduceus, to prove
 annotated programs written in other languages.
 
-\Question{How many \Coq users are there ?}
+\Question{How many {\Coq} users are there ?}
 
 Estimation is about 100 regular users.
 
-\Question{How old is \Coq ?}
-The first official release of \Coq (v. 4.10) was distributed in 1989.
+\Question{How old is {\Coq} ?}
+The first official release of {\Coq} (v. 4.10) was distributed in 1989.
 
 \Question{What are the \Coq-related tools ?}
 
 \begin{description}
 \item[Coqide] A GTK based gui for \Coq.
-\item[Pcoq] A gui for \Coq with proof by pointing and pretty printing.
+\item[Pcoq] A gui for {\Coq} with proof by pointing and pretty printing.
 \item[Helm/Mowgli] A rendering, searching and publishing tool.
 \item[Why] A back-end generator of verification conditions.
-\item[Krakatoa] A Java code certification tool that uses both \Coq and \Why to verify the soundness of implementations with regards to the specifications.
-\item[Caduceus] A C code certification tool that uses both \Coq and \Why.
-\item[coqwc] A tool similar to {\tt wc} to count lines in \Coq files.
-\item[coq-tex] A tool to insert \Coq examples within .tex files. 
+\item[Krakatoa] A Java code certification tool that uses both {\Coq} and {\Why} to verify the soundness of implementations with regards to the specifications.
+\item[Caduceus] A C code certification tool that uses both {\Coq} and \Why.
+\item[coqwc] A tool similar to {\tt wc} to count lines in {\Coq} files.
+\item[coq-tex] A tool to insert {\Coq} examples within .tex files. 
 \item[coqdoc] A documentation tool for \Coq.
-\item[Proof General] A emacs mode for \Coq and many other proof assistants.
+\item[Proof General] A emacs mode for {\Coq} and many other proof assistants.
 \item[Foc] The Foc project aims at building an environment to develop certified computer algebra libraries. 
 \end{description}
 
@@ -273,13 +274,13 @@ The first official release of \Coq (v. 4.10) was distributed in 1989.
 \end{itemize}
 
 
-\Question{What are the academic applications for \Coq ?}
+\Question{What are the academic applications for {\Coq} ?}
 
-Coq is used by mathematicians for formalizing large parts of mathematics, by teachers, and computer scientists to prove programs and APIs.
+{\Coq} is used by mathematicians for formalizing large parts of mathematics, by teachers, and computer scientists to prove programs and APIs.
 
-\Question{What are the industrial applications for \Coq ?}
+\Question{What are the industrial applications for {\Coq} ?}
 
-Coq is used by Trusted Logic to prove properties of the JavaCard system.
+{\Coq} is used by Trusted Logic to prove properties of the JavaCard system.
 
 todo christine compilo lustre ?
 
@@ -288,7 +289,7 @@ todo christine compilo lustre ?
 
 \section{Documentation}
 
-\Question{Where can I find documentation about \Coq ?} 
+\Question{Where can I find documentation about {\Coq} ?} 
 All the documentation about \Coq, from the reference manual~\cite{Coq:manual} to
 friendly tutorials~\cite{Coq:Tutorial} and documentation of the standard library, is available online at 
 \ahref{http://coq.inria.fr/coq/doc-eng.html}{\url{http://coq.inria.fr/coq/doc-eng.html}}.
@@ -304,39 +305,39 @@ This FAQ is available online at \ahref{http://coq.inria.fr/faq.html}{\url{http:/
 This FAQ is unfinished (in the sense that there are some obvious
 sections that are missing). Please send contributions to \texttt{Florent.Kirchner at lix.polytechnique.fr} and \texttt{Julien.Narboux at inria.fr}.
 
-\Question{Is there any mailing list about \Coq ?} 
-The main \Coq mailing list is \url{coq-club@coq.inria.fr}, which
+\Question{Is there any mailing list about {\Coq} ?} 
+The main {\Coq} mailing list is \url{coq-club@coq.inria.fr}, which
 broadcasts questions and suggestions about the implementation, the
 logical formalism or proof developments. See
 \ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://coq.inria.fr/mailman/listinfo/coq-club}} for
 subsription. For bugs reports see question \ref{coqbug}.
 
 \Question{Where can I find an archive of the list?}
-The archives of the \Coq mailing list are available at
+The archives of the {\Coq} mailing list are available at
 \ahref{http://coq.inria.fr/pipermail/coq-club}{\url{http://coq.inria.fr/pipermail/coq-club}}.
 
 
-\Question{How can I be kept informed of new releases of \Coq ?}
+\Question{How can I be kept informed of new releases of {\Coq} ?}
 
-New versions of \Coq are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to \Coq on \ahref{http://freshmeat.net/projects/coq/}{\url{http://freshmeat.net/projects/coq/}}.
+New versions of {\Coq} are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to {\Coq} on \ahref{http://freshmeat.net/projects/coq/}{\url{http://freshmeat.net/projects/coq/}}.
 
 
-\Question{Is there any book about \Coq ?}
+\Question{Is there any book about {\Coq} ?}
 The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been published by Springer-Verlag in 2004:
 \begin{quote}
 ``This book provides a pragmatic introduction to the development of
-proofs and certified programs using Coq. With its large collection of
+proofs and certified programs using \Coq. With its large collection of
 examples and exercises it is an invaluable tool for researchers,
 students, and engineers interested in formal methods and the
 development of zero-default software.''
 \end{quote}
 
-\Question{Where can I find some \Coq examples ?} 
+\Question{Where can I find some {\Coq} examples ?} 
 
 There are examples in the manual~\cite{Coq:manual} and in the
 Coq'Art~\cite{Coq:coqart} exercises \ahref{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}.
 You can also find large developments using
-\Coq in the \Coq user contributions :
+{\Coq} in the {\Coq} user contributions :
 \ahref{http://coq.inria.fr/distrib-eng.html}{\url{http://coq.inria.fr/distrib-eng.html}}.
 
 \Question{How can I report a bug ?}\label{coqbug}
@@ -349,15 +350,15 @@ You can use the web interface at \ahref{http://coq.inria.fr/bin/coq-bugs}{\url{h
 
 \section{Installation}
 
-\Question{What is the license of \Coq ?}
+\Question{What is the license of {\Coq} ?}
 It is distributed under the GNU Lesser General License (LGPL).
 
-\Question{Where can I find the sources of \Coq ?}
-The sources of \Coq can be found online in the tar.gz'ed packages
+\Question{Where can I find the sources of {\Coq} ?}
+The sources of {\Coq} can be found online in the tar.gz'ed packages
 (\ahref{http://coq.inria.fr/distrib-eng.html}{\url{http://coq.inria.fr/distrib-eng.html}}). Development sources can
 be accessed via anonymous CVS : \ahref{http://coqcvs.inria.fr/}{\url{http://coqcvs.inria.fr/}}
 
-\Question{On which platform \Coq is available ?}
+\Question{On which platform {\Coq} is available ?}
 Compiled binaries are available for Linux, MacOS X, Solaris, and
 Windows. The sources can be easily adapted to all platforms supporting Objective Caml.
 
@@ -365,11 +366,11 @@ Windows. The sources can be easily adapted to all platforms supporting Objective
 
 \section{Logic}
 
-
+\subsection{The logic of {\Coq}}
 
 \Question{What is the logic of \Coq?}
 
-\Coq is based on an axiom-free type theory called
+{\Coq} is based on an axiom-free type theory called
 the Calculus of Inductive Constructions (see Coquand \cite{CoHu86}
 and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order
 functions and predicates, inductive and co-inductive datatypes and
@@ -377,17 +378,59 @@ predicates, and a stratified hierarchy of sets.
 
 \Question{Is \Coq's logic intuitionistic or classical?}
 
-\Coq theory is basically intuitionistic
+{\Coq} theory is basically intuitionistic
 (i.e. excluded-middle $A\lor\neg A$ is not granted by default) with
 the possibility to reason classically on demand by requiring an
 optional module stating $A\lor\neg A$.
 
-
 \Question{Can I define non-terminating programs in \Coq?}
 
-No, all programs in \Coq are terminating. Especially, loops
+No, all programs in {\Coq} are terminating. Especially, loops
 must come with an evidence of their termination.
 
+\subsection{Axioms}
+
+\Question{What axioms can be safely added to {\Coq}?}
+
+There are a few typical useful axioms that are independent from the
+Calculus of Inductive Constructions and that can be safely added to
+{\Coq}. These axioms are stated in the directory {\tt Logic} of the
+standard library of {\Coq}. The most interesting ones are
+
+\begin{itemize}
+\item Excluded-middle: $\forall A:Prop, A \lor \neg A$
+\item Proof-irrelevance: $\forall A:Prop, \forall p_1 p_2:A, p_1=p_2$
+\item Streicher's axiom $K$ stating the unicity of equality proofs
+\item The principle of description: $\forall x, \exists! y, R(x,y) \rightarrow \exists f, \forall x, R(x,f(x))$
+\item The functional axiom of choice: $\forall x, \exists y, R(x,y) \rightarrow \exists f, \forall x, R(x,f(x))$
+\item Extensionality of predicates: $\forall P Q:A\rightarrow Prop, (\forall x, P(x) \leftrightarrow Q(x)) \rightarrow P=Q$
+\item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$
+\end{itemize}
+
+Here is a summary of the relative strength of these axioms, most
+proofs can be found in directory {\tt Logic} of the standard library.
+
+%\include{axioms}
+\includegraphics{axioms}
+
+\Question{What standard axioms are inconsistent with {\Coq}?}
+
+The axiom of description together with classical logic
+(e.g. excluded-middle) are inconsistent in the variant of the Calculus
+of Inductive Constructions where {\Set} is impredicative.
+
+As a consequence, the functional form of the axiom of choice and
+excluded-middle, or any form of the axiom of choice together with
+predicate extensionality are inconsistent in the {\Set}-impredicative
+version of the Calculus of Inductive Constructions.
+
+The main purpose of the \Set-predicative restriction of the Calculus
+of Inductive Constructions is precisely to accomodate these axioms
+which are quite standard in mathematical usage.
+
+The $\Set$-predicative system is commonly considered consistent by
+interpreting it in a standard set-theoretic boolean model, even with
+classical logic, axiom of choice and predicate extensionality added.
 
 \Question{What is Streicher's axiom $K$}
 \label{Streicher}
@@ -441,52 +484,6 @@ Axiom
       eq_dep U P u p1 u p2 -> p1 = p2.
 \end{coq_example*}
 
-\subsection{Impredicativity}
-
-\Question{Why Injection does not work on impredicative {\tt Set}?}
-
- E.g. in this case (this occurs only in the {\tt Set}-impredicative
- variant of \Coq:
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Inductive I : Type :=
-  intro : forall k:Set, k -> I.
-Lemma eq_jdef : 
-   forall x y:nat, intro _ x = intro _ y -> x = y.
-Proof.
-   intros x y H; injection H.
-\end{coq_example*}
-
- Injectivity of constructors is restricted to predicative types. If
-injectivity on large inductive types were not restricted, we would be
-allowed to derive an inconsistency (e.g. following the lines of
-Burali-Forti paradox). The question remains open whether injectivity
-is consistent on some large inductive types not expressive enough to
-encode known paradoxes (such as type I above).
-
-
-\Question{What is a "large inductive definition"?}
-
- An inductive definition in {\Prop} pr {\Set} is called large
-if its constructors embed sets or propositions. As an example, here is
-a large inductive type:
-
-\begin{coq_example*}
-Inductive sigST (P:Set -> Set) : Type :=
-  existST : forall X:Set, P X -> sigST P.
-\end{coq_example*}
-
-In the {\tt Set} impredicative variant of {\Coq}, large inductive
-definitions in {\tt Set} have restricted elimination schemes to
-prevent inconsistencies. Especially, projecting the set or the
-proposition content of a large inductive definition is forbidden. If
-it were allowed, it would be possible to encode e.g. Burali-Forti
-paradox \cite{Gir70,Coq85}.
-
 \Question{Why is dependent elimination in Prop not
 available by default?}
 
@@ -537,13 +534,13 @@ Hurkens and Miquel that systems $U-$ and $U$ are inconsistent [Girard
 found in file {\tt Logic/Hurkens.v} of {\Coq} standard library.
 
   For instance, when the user see {\tt forall (X:Type), X->X : Type}, each
-occurrence of \Type is implicitly bound to a different level, say
+occurrence of {\Type} is implicitly bound to a different level, say
 $\alpha$ and $\beta$ and the actual statement is {\tt
 forall X:Type($\alpha$), X->X : Type($\beta$)} with the constraint
 $\alpha<\beta$.
 
   When a statement violates a constraint, the message {\tt Universe
-inconsistency} appears. Example: {\tt fun (x:Type) (y:forall X:Type, X \coqimp X) => z x x}.
+inconsistency} appears. Example: {\tt fun (x:Type) (y:forall X:Type, X {\coqimp} X) => z x x}.
 
 
 \Question{I have two proofs of the same proposition. Can I prove they are equal?}
@@ -561,7 +558,7 @@ More precisely, the equality of all proofs of a given proposition is called
   \vfile{\LogicProofIrrelevance}{ProofIrrelevance} and \vfile{\LogicBerardi}{Berardi}.
 
   Alternatively, propositional extensionality (i.e.  \coqtt{(A
-  \coqequiv B) \coqimp A=B}, defined in \vfile{\LogicClassicalFacts}{ClassicalFacts}),
+  {\coqequiv} B) {\coqimp} A=B}, defined in \vfile{\LogicClassicalFacts}{ClassicalFacts}),
   also implies proof-irrelevance.
 
 %  It is an ongoing work of research to natively include proof
@@ -594,7 +591,7 @@ All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}.
 
 \Question{How is equational reasoning working in {\Coq}?}
 
- \Coq comes with an internal notion of computation called
+ {\Coq} comes with an internal notion of computation called
 {\em conversion} (e.g. $(x+1)+y$ is internally equivalent to
 $(x+y)+1$; similarly applying argument $a$ to a function mapping $x$
 to some expression $t$ converts to the expression $t$ where $x$ is
@@ -604,6 +601,51 @@ equational reasoning but is limited to sequential evaluation of
 expressions of (not necessarily closed) programs. Besides conversion,
 equations have to be treated by hand or using specialised tactics.
 
+\subsection{Impredicativity}
+
+\Question{Why Injection does not work on impredicative {\tt Set}?}
+
+ E.g. in this case (this occurs only in the {\tt Set}-impredicative
+ variant of \Coq:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Inductive I : Type :=
+  intro : forall k:Set, k -> I.
+Lemma eq_jdef : 
+   forall x y:nat, intro _ x = intro _ y -> x = y.
+Proof.
+   intros x y H; injection H.
+\end{coq_example*}
+
+ Injectivity of constructors is restricted to predicative types. If
+injectivity on large inductive types were not restricted, we would be
+allowed to derive an inconsistency (e.g. following the lines of
+Burali-Forti paradox). The question remains open whether injectivity
+is consistent on some large inductive types not expressive enough to
+encode known paradoxes (such as type I above).
+
+
+\Question{What is a "large inductive definition"?}
+
+ An inductive definition in {\Prop} pr {\Set} is called large
+if its constructors embed sets or propositions. As an example, here is
+a large inductive type:
+
+\begin{coq_example*}
+Inductive sigST (P:Set -> Set) : Type :=
+  existST : forall X:Set, P X -> sigST P.
+\end{coq_example*}
+
+In the {\tt Set} impredicative variant of {\Coq}, large inductive
+definitions in {\tt Set} have restricted elimination schemes to
+prevent inconsistencies. Especially, projecting the set or the
+proposition content of a large inductive definition is forbidden. If
+it were allowed, it would be possible to encode e.g. Burali-Forti
+paradox \cite{Gir70,Coq85}.
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -616,7 +658,7 @@ equations have to be treated by hand or using specialised tactics.
 
 \Question{My goal is a conjunction, how can I prove it ?}
 
-Use some theorem or assumption or use the \split tactic.
+Use some theorem or assumption or use the {\split} tactic.
 \begin{coq_example}
 Goal forall A B:Prop, A->B-> A/\B.
 intros.
@@ -628,7 +670,7 @@ Qed.
 
 \Question{My goal contains a conjunction as an hypothesis, how can I use it ?}
 
-If you want to decompose your hypothesis into other hypothesis you can use the \decompose tactic :
+If you want to decompose your hypothesis into other hypothesis you can use the {\decompose} tactic :
 
 \begin{coq_example}
 Goal forall A B:Prop, A/\B-> B.
@@ -642,7 +684,7 @@ Qed.
 \Question{My goal is a disjonction, how can I prove it ?}
 
 You can prove the left part or the right part of the disjunction using
-\left or \right tactics. If you want to do a classical
+{\left} or {\right} tactics. If you want to do a classical
 reasoning step, use the {\tt classic} axiom to prove the right part with the assumption
 that the left part of the disjunction is false.
 
@@ -680,15 +722,15 @@ Qed.
 \Question{My goal is an universally quantified statement, how can I prove it ?}
 
 Use some theorem or assumption or introduce the quantified variable in
-the context using the \intro tactic. If there are several
-variables you can use the \intros tactic. A good habit is to
-provide names for these variables: \Coq will do it anyway, but such
+the context using the {\intro} tactic. If there are several
+variables you can use the {\intros} tactic. A good habit is to
+provide names for these variables: {\Coq} will do it anyway, but such
 automatic naming decreases legibility and robustness.
 
 
 \Question{My goal is an existential, how can I prove it ?}
 
-Use some theorem or assumption or exhibit the witness using the \exists tactic.
+Use some theorem or assumption or exhibit the witness using the {\existstac} tactic.
 \begin{coq_example}
 Goal exists x:nat, forall y, x+y=y.
 exists 0.
@@ -700,7 +742,7 @@ Qed.
 
 \Question{My goal is solvable by  some lemma, how can I prove it ?}
 
-Just use the \apply tactic.
+Just use the {\apply} tactic.
 
 \begin{coq_eval}
 Reset Initial.
@@ -720,12 +762,12 @@ Qed.
 
 \Question{My goal contains False as an hypotheses, how can I prove it ?}
 
-You can use the \contradiction or \intuition tactics.
+You can use the {\contradiction} or {\intuition} tactics.
 
 
 \Question{My goal is an equality of two convertible terms, how can I prove it ?}
 
-Just use the \reflexivity tactic.
+Just use the {\reflexivity} tactic.
 
 \begin{coq_example}
 Goal forall x, 0+x = x.
@@ -736,17 +778,17 @@ Qed.
 
 \Question{My goal is a {\tt let x := a in ...}, how can I prove it ?}
 
-Just use the \intro tactic.
+Just use the {\intro} tactic.
 
 
 \Question{My goal is a {\tt let (a, ..., b) := c in}, how can I prove it ?}
 
-Just use the \destruct c as (a,...,b) tactic.
+Just use the {\destruct} c as (a,...,b) tactic.
 
 
 \Question{My goal contains some existential hypotheses, how can I use it ?}
 
-You can use the tactic \elim with you hypotheses as an argument.
+You can use the tactic {\elim} with you hypotheses as an argument.
 
 \Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses ?}
 
@@ -757,7 +799,7 @@ Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H
 
 \Question{My goal is an equality, how can I swap the left and right hand terms ?}
 
-Just use the \symmetry tactic.
+Just use the {\symmetry} tactic.
 \begin{coq_example}
 Goal forall x y : nat, x=y -> y=x.
 intros.
@@ -768,7 +810,7 @@ Qed.
 
 \Question{My hypothesis is an equality, how can I swap the left and right hand terms ?}
 
-Just use the \symmetryin tactic.
+Just use the {\symmetryin} tactic.
 
 \begin{coq_example}
 Goal forall x y : nat, x=y -> y=x.
@@ -781,7 +823,7 @@ Qed.
 
 \Question{My goal is an equality, how can I prove it by transitivity ?}
 
-Just use the \transitivity tactic.
+Just use the {\transitivity} tactic.
 \begin{coq_example}
 Goal forall x y z : nat, x=y -> y=z -> x=z.
 intros.
@@ -856,7 +898,7 @@ Qed.
 
 \Question{My goal is one of the hypotheses, how can I prove it ?}
 
-Use the \assumption tactic.
+Use the {\assumption} tactic.
 
 \begin{coq_example}
 Goal 1=1 -> 1=1.
@@ -868,7 +910,7 @@ Qed.
 
 \Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it ?}
 
-Use the \exact tactic.
+Use the {\exact} tactic.
 \begin{coq_example}
 Goal 1=1 -> 1=1 -> 1=1.
 intros.
@@ -885,7 +927,7 @@ programs.
 
 \Question{My goal is a propositional tautology, how can I prove it ?}
 
-Just use the \tauto tactic.
+Just use the {\tauto} tactic.
 \begin{coq_example}
 Goal forall A B:Prop, A-> (A\/B) /\ A.
 intros.
@@ -901,7 +943,7 @@ todo : demander un exemple à Pierre
 
 \Question{My goal is solvable by a sequence of rewrites, how can I prove it ?}
 
-Just use the \congruence tactic.
+Just use the {\congruence} tactic.
 \begin{coq_example}
 Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
 intros.
@@ -912,7 +954,7 @@ Qed.
 
 \Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it ?}
 
-Just use the \congruence tactic.
+Just use the {\congruence} tactic.
 
 \begin{coq_example}
 Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
@@ -924,7 +966,7 @@ Qed.
 
 \Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it ?}
 
-Just use the \ring tactic.
+Just use the {\ring} tactic.
 
 \begin{coq_example}
 Require Import ZArith.
@@ -938,7 +980,7 @@ Qed.
 
 \Question{My goal is an equality on some field (e.g. real numbers), how can I prove it ?}
 
-Just use the \field tactic.
+Just use the {\field} tactic.
 
 \begin{coq_example}
 Require Import Reals.
@@ -952,7 +994,7 @@ Qed.
 \end{coq_example}
 
 
-\Question{My goal is an inequality on integers in Presburger arithmetic (an expression build from +,-,constants and variables), how can I prove it ?}
+\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it ?}
 
 
 \begin{coq_example}
@@ -968,16 +1010,16 @@ Qed.
 
 \Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it ?}
 
-You need the \gb tactic (see Loïc Pottier's homepage).
+You need the {\gb} tactic (see Loïc Pottier's homepage).
 
 \subsection{Tactics usage}
 
 \Question{I want to state a fact that I will use later as an hypothesis, how can I do it ?}
 
 If you want to use forward reasoning (first proving the fact and then
-using it) you just need to use the \assert tactic. If you want to use
+using it) you just need to use the {\assert} tactic. If you want to use
 backward reasoning (proving your goal using an assumption and then
-proving the assumption) use the \cut tactic.
+proving the assumption) use the {\cut} tactic.
 
 \begin{coq_example}
 Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. 
@@ -1002,14 +1044,14 @@ Qed.
 
 \Question{I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it ?}
 
-You can use \cut followed by \intro or you can use the following \Ltac command :
+You can use {\cut} followed by {\intro} or you can use the following {\Ltac} command :
 \begin{verbatim}
 Ltac assert_later t := cut t;[intro|idtac]. 
 \end{verbatim}
 
-\Question{What is the difference between \Qed and \Defined ?}
+\Question{What is the difference between {\Qed} and {\Defined} ?}
 
-These two commands perform type checking, but when \Defined is used the new definition is set as transparent, otherwise it is defined as opaque (see \ref{opaque}).
+These two commands perform type checking, but when {\Defined} is used the new definition is set as transparent, otherwise it is defined as opaque (see \ref{opaque}).
 
 
 \Question{How can I know what a tactic does ?}
@@ -1018,65 +1060,65 @@ You can use the {\tt info} command.
 
 
 
-\Question{Why \auto does not work ? How can I fix it ?}
+\Question{Why {\auto} does not work ? How can I fix it ?}
 
 You can increase the depth of the proof search or add some lemmas in the base of hints.
 Perhaps you may need to use \eauto.
 
-\Question{What is \eauto ?}
+\Question{What is {\eauto} ?}
 
-This is the same tactic as \auto, but it does some \eapply instead of \apply.
+This is the same tactic as \auto, but it does some {\eapply} instead of \apply.
 
 todo les espaces
 
 
-\Question{How can I speed up \auto ?}
+\Question{How can I speed up {\auto} ?}
 
-You can use \texttt{info }\auto to replace \auto by the tactics it generates.
+You can use \texttt{info }\auto to replace {\auto} by the tactics it generates.
 You can split your hint bases into smaller ones.
 
 
-\Question{What is the equivalent of \tauto for classical logic ?}
+\Question{What is the equivalent of {\tauto} for classical logic ?}
 
 Currently there are no equivalent tactic for classical logic. You can use Gödel's ``not not'' translation.
 
 
 \Question{I want to replace some term with another in the goal, how can I do it ?}
 
-If one of your hypothesis (say {\tt H}) states that the terms are equal you can use the \rewrite tactic. Otherwise you can use the \replace {\tt with} tactic. 
+If one of your hypothesis (say {\tt H}) states that the terms are equal you can use the {\rewrite} tactic. Otherwise you can use the {\replace} {\tt with} tactic. 
 
 \Question{I want to replace some term with another in an hypothesis, how can I do it ?}
 
-You can use the \rewrite {\tt in} tactic.
+You can use the {\rewrite} {\tt in} tactic.
 
 \Question{I want to replace some symbol with its definition, how can I do it ?}
 
-You can use the \unfold tactic.
+You can use the {\unfold} tactic.
 
 \Question{How can I reduce some term ?}
 
-You can use the \simpl tactic.
+You can use the {\simpl} tactic.
 
 \Question{How can I declare a shortcut for some term ?}
 
-You can use the \set or \pose tactics.
+You can use the {\set} or {\pose} tactics.
 
 \Question{How can I perform case analysis ?}
 
-You can use the \case or \destruct tactics.
+You can use the {\case} or {\destruct} tactics.
 
 
 \Question{Why should I name my intros ?}
 
-When you use the \intro tactic you don't have to give a name to your
-hypothesis. If you do so the name will be generated by \Coq but your
+When you use the {\intro} tactic you don't have to give a name to your
+hypothesis. If you do so the name will be generated by {\Coq} but your
 scripts may be less robust. If you add some hypothesis to your theorem
 (or change their order), you will have to change your proof to adapt
 to the new names.
 
 \Question{How can I automatize the naming ?}
 
-You can use the {\tt Show Intro.} or  {\tt Show Intros.} commands to generate the names and use your editor to generate a fully named \intro tactic. 
+You can use the {\tt Show Intro.} or  {\tt Show Intros.} commands to generate the names and use your editor to generate a fully named {\intro} tactic. 
 This can be automatized within {\tt xemacs}.
 
 \begin{coq_example}
@@ -1093,7 +1135,7 @@ Qed.
 
 \Question{I want to automatize the use of some tactic, how can I do it ?}
 
-You need to use the {\tt proof with T} command and add \ldots at the
+You need to use the {\tt proof with T} command and add {\ldots} at the
 end of your sentences.
 
 For instance :
@@ -1107,7 +1149,7 @@ Qed.
 
 \Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it ?}
 
-You need to use the \try and \solve tactics. For instance :
+You need to use the {\try} and {\solve} tactics. For instance :
 \begin{coq_example}
 Require Import ZArith.
 Require Ring.
@@ -1118,9 +1160,9 @@ intros...
 Qed.
 \end{coq_example}
 
-\Question{How can I do the opposite of the \intro tactic ?}
+\Question{How can I do the opposite of the {\intro} tactic ?}
 
-You can use the \generalize tactic.
+You can use the {\generalize} tactic.
 
 \begin{coq_example}
 Goal forall A B : Prop, A->B-> A/\B.
@@ -1133,33 +1175,33 @@ Qed.
 
 \Question{One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it ?}
 
-You can use the \subst tactic. This will rewrite the equality everywhere and clear the assumption.
+You can use the {\subst} tactic. This will rewrite the equality everywhere and clear the assumption.
 
 \Question{What can I do if I get ``{\tt generated subgoal term has metavariables in it }'' ?}
 
-You should use the \eapply tactic, this will generate some goals containing metavariables. 
+You should use the {\eapply} tactic, this will generate some goals containing metavariables. 
 
 \Question{How can I instantiate some metavariable ?}
 
-Just use the \instantiate tactic.
+Just use the {\instantiate} tactic.
 
 
-\Question{What is the use of the \pattern tactic ?}
+\Question{What is the use of the {\pattern} tactic ?}
 
-The \pattern tactic transforms the current goal, performing
+The {\pattern} tactic transforms the current goal, performing
 beta-expansion on all the applications featuring this tactic's
 argument. For instance, if the current goal includes a subterm {\tt
 phi(t)}, then {\tt pattern t} transforms the subterm into {\tt (fun
-x:A => phi(x)) t}. This can be useful when \apply fails on matching,
+x:A => phi(x)) t}. This can be useful when {\apply} fails on matching,
 to abstract the appropriate terms.
 
 \Question{What is the difference between assert, cut and generalize ?}
 
 PS: Notice for people that are interested in proof rendering that \assert
-and \pose (and \cut) are not rendered the same as \generalize (see the
+and {\pose} (and \cut) are not rendered the same as {\generalize} (see the
 HELM experimental rendering tool at \ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}, link
-HELM, link COQ Online). Indeed \generalize builds a beta-expanded term
-while \assert, \pose and \cut uses a let-in.
+HELM, link COQ Online). Indeed {\generalize} builds a beta-expanded term
+while \assert, {\pose} and {\cut} uses a let-in.
 
 \begin{verbatim}
   (* Goal is T *)
@@ -1191,8 +1233,8 @@ is rendered into something like
   ... the proof of T ...
   we proved T
 \end{verbatim}
-Otherwise said, \generalize is not rendered in a forward-reasoning way,
-while \assert is.
+Otherwise said, {\generalize} is not rendered in a forward-reasoning way,
+while {\assert} is.
 
 \Question{Is there anyway to do pattern matching with dependent types ?}
 
@@ -1205,7 +1247,7 @@ todo
 
 \Question{How can I change the order of the subgoals ?}
 
-You can use the \Focus command to concentrate on some goal. When the goal is proved you will see the remaining goals.
+You can use the {\Focus} command to concentrate on some goal. When the goal is proved you will see the remaining goals.
 
 \Question{How can I change the order of the hypothesis ?}
 
@@ -1229,7 +1271,7 @@ You can use the {\tt Admitted} command to state your current proof as an axiom.
 
 \Question{What is the difference between a lemma, a fact and a theorem ?}
 
-From \Coq point of view there are no difference. But some tools can
+From {\Coq} point of view there are no difference. But some tools can
 have a different behaviour when you use a lemma rather than a
 theorem. For instance {\tt coqdoc} will not generate documentation for
 the lemmas within your development.
@@ -1247,7 +1289,7 @@ a look at the manual for further information.
 
 \Question{How can I prove that two constructors are different ?}
 
-You can use the \discriminate tactic.
+You can use the {\discriminate} tactic.
 
 \begin{coq_example}
 Inductive toto : Set := | C1 : toto | C2 : toto.
@@ -1258,7 +1300,7 @@ Qed.
 
 \Question{During an inductive proof, how to get rid of impossible cases of an inductive definition ?}
 
-Use the \inversion tactic.
+Use the {\inversion} tactic.
 
 
 \Question{How can I prove that 2 terms in an inductive set are equal? Or different?}
@@ -1274,7 +1316,7 @@ trivial but the proof of \coqtt{n+0=n} is not?}
 Print plus.
 \end{coq_example}
 
-\noindent the expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons
+{\noindent} the expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons
 modulo evaluation of expressions, \coqtt{0+n} and \coqtt{n} are
 considered equal and the theorem \coqtt{0+n=n} is an instance of the
 reflexivity of equality. On the other side, \coqtt{n+0} does not
@@ -1441,8 +1483,8 @@ Require Import Arith.
 \end{coq_eval}
 
 \begin{coq_example}
-Infix "<" := lt (at level 50, no associativity).
-Infix "<=" := le (at level 50, no associativity).
+Infix "<" := lt (at level 70, no associativity).
+Infix "<=" := le (at level 70, no associativity).
 Lemma le_or_lt : forall n n0:nat, n0 < n \/ n <= n0.
 induction n; destruct n0; auto with arith.
 destruct (IHn n0); auto with arith.
@@ -1476,6 +1518,9 @@ the simplest way?}
  Just case-expand F(t) then complete by a trivial case analysis.
 Here is what it gives on e.g. the type of streams on naturals
 
+\begin{coq_eval}
+Set Implicit Arguments.
+\end{coq_eval}
 \begin{coq_example}
 CoInductive Stream (A:Set) : Set :=
   Cons : A -> Stream A -> Stream A.
@@ -1502,7 +1547,7 @@ You can define your own notation for forall :
 \begin{verbatim}
 Notation "fa x : t, P" := (forall x:t, P) (at level 200, x ident).
 \end{verbatim}
-or if your are using \CoqIde you can define a pretty symbol for for all and an input method (see \ref{forallcoqide}).
+or if your are using {\CoqIde} you can define a pretty symbol for for all and an input method (see \ref{forallcoqide}).
 
 
 
@@ -1528,20 +1573,20 @@ because ``$^2$'' is an iso-latin character. If you really want this kind of nota
 %%%%%%%
 \section{\Ltac}
 
-\Question{What is \Ltac ?}
+\Question{What is {\Ltac} ?}
 
-\Ltac is the tactic language for \Coq. It provides the user with a
+{\Ltac} is the tactic language for \Coq. It provides the user with a
 high-level ``toolbox'' for tactic creation.
 
 \Question{Why do I always get the same error message ?}
 
 
-\Question{Is there any printing command in \Ltac ?}
+\Question{Is there any printing command in {\Ltac} ?}
 
-You can use the \idtac tactic with a string argument. This string
-will be printed out. The same applies to the \fail tactic
+You can use the {\idtac} tactic with a string argument. This string
+will be printed out. The same applies to the {\fail} tactic
 
-\Question{What is the syntax for let in \Ltac ?}
+\Question{What is the syntax for let in {\Ltac} ?}
 
 If $x_i$ are identifiers and $e_i$ and $expr$ are tactic expressions, then let reads:
 \begin{center}
@@ -1554,7 +1599,7 @@ should be added around it. For example:
 Ltac twoIntro := let x:=intro in (x;x).
 \end{coq_example}
 
-\Question{What is the syntax for pattern matching in \Ltac ?}
+\Question{What is the syntax for pattern matching in {\Ltac} ?}
 
 Pattern matching on a term $expr$ (non-linear first order unification)
 with patterns $p_i$ and tactic expressions $e_i$ reads:
@@ -1574,7 +1619,7 @@ Underscore matches all terms.
 \Question{What is the semantics for match goal ?}
 
 {\tt match goal} matches the current goal against a series of
-patterns: {$hyp_1 \ldots hyp_n$ \textbar- $ccl$}. It uses a
+patterns: {$hyp_1 {\ldots} hyp_n$ \textbar- $ccl$}. It uses a
 first-order unification algorithm, and tries all the possible
 combinations of $hyp_i$ before dropping the branch and moving to the
 next one. Underscore matches all terms.
@@ -1600,7 +1645,7 @@ todo
 
 \Question{Can you show me an example of a tactic writen in OCaml ?}
 
-You have some examples of tactics written in Ocaml in the ``contrib'' directory of \Coq sources. 
+You have some examples of tactics written in Ocaml in the ``contrib'' directory of {\Coq} sources. 
 
 
 
@@ -1748,11 +1793,11 @@ You can use {\tt coqdoc}.
 
 \Question{How can I generate some dependency graph from my development ?}
 
-\Question{How can I cite some \Coq in my latex document ?}
+\Question{How can I cite some {\Coq} in my latex document ?}
 
 You can use {\tt coq\_tex}.
 
-\Question{How can I cite the \Coq reference manual ?}
+\Question{How can I cite the {\Coq} reference manual ?}
 
 You can use this bibtex entry :
 \begin{verbatim}
@@ -1769,9 +1814,9 @@ You can use this bibtex entry :
 
 \section{\CoqIde}
 
-\Question{What is \CoqIde ?}
+\Question{What is {\CoqIde} ?}
 
-\CoqIde is a gtk based gui for \Coq.
+{\CoqIde} is a gtk based gui for \Coq.
 
 \Question{How to enable Emacs keybindings ?}
  Insert \texttt{gtk-key-theme-name = "Emacs"}
@@ -1787,7 +1832,7 @@ You can use this bibtex entry :
 
 \Question{How to use those Forall and Exists pretty symbols ?}\label{forallcoqide}
  Thanks to the notation features in \Coq, you just need to insert these
-lines in your \Coq buffer :\\
+lines in your {\Coq} buffer :\\
 \begin{texttt}
 Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident).
 \end{texttt}\\
@@ -1803,7 +1848,7 @@ To enable these notations automatically start coqide with
 \begin{verbatim}
 	coqide -l utf8
 \end{verbatim}
-In the ide subdir of \Coq library, you will find a sample utf8.v with some 
+In the ide subdir of {\Coq} library, you will find a sample utf8.v with some 
 pretty simple notations.
 
 \Question{How to define an input method for non ASCII symbols ?}\label{inputmeth}
@@ -1835,7 +1880,7 @@ Glib.Utf8.from_unichar 0x2200;;
 	do not need .
 \end{itemize}
 
-\Question{How to build a custom \CoqIde with user ml code ?}
+\Question{How to build a custom {\CoqIde} with user ml code ?}
  Use 
 	coqmktop -ide -byte m1.cmo...mi.cmo
     or 
@@ -1891,7 +1936,7 @@ The goal is the statement to be proved.
 
 \Question{What is a meta variable ?}
 
-A meta variable in \Coq represents a ``hole'', i.e. a part of a proof
+A meta variable in {\Coq} represents a ``hole'', i.e. a part of a proof
 that is still unknown. 
 
 \Question{What is Gallina ?}  
@@ -1901,7 +1946,7 @@ of this language can be found in the Reference Manual.
 
 \Question{What is The Vernacular ?}  
 
-It is the language of commands of Gallina i.e. definitions, lemmas, \ldots  
+It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots}  
 
 
 \Question{What is a dependent type ?}
@@ -1913,10 +1958,10 @@ of size $n$. Theis type depends on $n$
 \Question{What is a proof by reflection ?}
 
 This is a proof generated by some computation which is done using the
-internal reduction of \Coq (not using the tactic language of \Coq
+internal reduction of {\Coq} (not using the tactic language of \Coq
 (\Ltac) nor the implementation language for \Coq).  An example of
-tactic using the reflection mechanism is the \ring tactic. The
-reflection method consist in reflecting a subset of \Coq language (for
+tactic using the reflection mechanism is the {\ring} tactic. The
+reflection method consist in reflecting a subset of {\Coq} language (for
 example the arithmetical expressions) into an object of the \Coq
 language itself (in this case an inductive type denoting arithmetical
 expressions).  For more information see~\cite{howe,harrison,boutin}
@@ -1941,12 +1986,12 @@ Opaque definitions can not be unfolded but transparent ones can.
 
 \Question{What can I do when {\tt Qed.} is slow ?}
 
-Sometime you can use the \abstractt tactic, which makes as if you had
+Sometime you can use the {\abstracttac} tactic, which makes as if you had
 stated some local lemma, this speeds up the typing process.
 
 \Question{What can I do if I get ``Cannot solve a second-order unification problem'' ?}
 
-You can help coq using the \pattern tactic.
+You can help {\Coq} using the {\pattern} tactic.
 
 \Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?}
 
@@ -1984,9 +2029,9 @@ again the missing coercion.
 \Question{What if my question isn't answered here ?} 
 \label{lastquestion}
 
-Don't panic. You can try the \Coq manual~\cite{Coq:manual} for a technical
+Don't panic. You can try the {\Coq} manual~\cite{Coq:manual} 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
+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.