add a comment about Show Existentials and a question about case_eq

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

1 files changed, 18 insertions, 0 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 2b5d898fd..0856377ea 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1231,6 +1231,9 @@ You can use the {\set} or {\pose} tactics.
 
 You can use the {\case} or {\destruct} tactics.
 
+\Question{How can I prevent the case tactic from losing information ?}
+
+You may want to use the (now standard) {\tt case\_eq} tactic. See the Coq'Art page 159.
 
 \Question{Why should I name my intros?}
 
@@ -2417,6 +2420,21 @@ existential variable which eventually got erased by some computation.
 You have to backtrack to the faulty occurrence of {\eauto} or
 {\eapply} and give the missing argument an explicit value.
 
+Note that you can see what the current existential are using the {\tt
+  Show Existentials} command.
+
+\begin{coq_example}
+Lemma example_show_existentials :  forall a b c:nat, a=b -> b=c -> a=c.
+Proof.
+intros.
+eapply trans_equal.
+Show Existentials.
+eassumption.
+assumption.
+Qed.
+\end{coq_example}
+
+
 \Question{What can I do if I get ``Cannot solve a second-order unification problem''?}
 
 You can help {\Coq} using the {\pattern} tactic.