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(-)

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