From beff9386b82c4aa6e066642d56a36c8034f54604 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 26 Jul 2015 07:44:45 +0200
Subject: Remove obsolete question about eta-conversion.

---
 doc/faq/FAQ.tex | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'doc/faq/FAQ.tex')

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 589933578a..d264ac62a5 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -2579,12 +2579,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
-- 
cgit v1.2.3


From 20147a19e9f9a2bbeab5612c7ac17baaaf810af5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 26 Jul 2015 08:38:05 +0200
Subject: Regenerate the axiom figure of the FAQ.

The .png was ugly (less than 400px wide) and did not match the content of
the .fig file (e.g. presence of '$'). To improve things a bit, text is now
rendered by latex.
---
 doc/faq/FAQ.tex | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

(limited to 'doc/faq/FAQ.tex')

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index d264ac62a5..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}?}
 
-- 
cgit v1.2.3