Merge branch 'v8.5'

1 files changed, 22 insertions, 13 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 589933578a..8495156ca1 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -503,19 +503,34 @@ $\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$
 \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.
-The justification of their validity relies on the interpretability in
-set theory.
-
+Figure~\ref{fig:axioms} is a summary of the relative strength of these
+axioms, most proofs can be found in directory {\tt Logic} of the standard
+library. (Statements in boldface are the most ``interesting'' ones for
+Coq.) The justification of their validity relies on the interpretability
+in set theory.
+
+% fig2dev -m 2 -L png axioms.fig axioms.png
+% fig2dev -L pdftex axioms.fig axioms.pdf
+% fig2dev -L pdftex_t -p axioms.pdf axioms.fig axioms.pdf_t
+% fig2dev -L pstex axioms.fig axioms.eps
+% fig2dev -L pstex_t -p axioms.eps axioms.fig axioms.eps_t
+
+\begin{figure}[htbp]
 %HEVEA\imgsrc{axioms.png}
 %BEGIN LATEX
+\begin{center}
 \ifpdf   % si on est en pdflatex
-\includegraphics[width=1.0\textwidth]{axioms.png}
+\scalebox{0.65}{\input{axioms.pdf_t}}
+%\includegraphics[width=1.0\textwidth]{axioms.png}
 \else
-\includegraphics[width=1.0\textwidth]{axioms.eps}
+\scalebox{0.65}{\input{axioms.eps_t}}
+%\includegraphics[width=1.0\textwidth]{axioms.eps}
 \fi
+\end{center}
 %END LATEX
+\caption{The dependency graph of axioms in the Calculus of Inductive Constructions}
+\label{fig:axioms}
+\end{figure}
 
 \Question{What standard axioms are inconsistent with {\Coq}?}
 
@@ -2579,12 +2594,6 @@ Qed.
 
 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)}?}
-
- This is because \texttt{\{x:A|P x\}} is a notation for
-\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to
-$\eta$-conversion, this is different from \texttt{sig P}.
-
 
 \Question{I copy-paste a term and {\Coq} says it is not convertible
   to the original term. Sometimes it even says the copied term is not