diff options
| author | notin | 2007-12-11 10:08:13 +0000 |
|---|---|---|
| committer | notin | 2007-12-11 10:08:13 +0000 |
| commit | 90e17b8f5c5494a41daf9f3a613e987b1515cbc3 (patch) | |
| tree | e740af79e261b4860630d305f711f1bc0a19daad | |
| parent | d0f57e4e8b9d8feaadf96a241d3546ba061eb20c (diff) | |
Modification de la question no 172 de la FAQ (cf bug #1755)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10363 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/faq/FAQ.tex | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 46351e23df..f40c28c4d4 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2445,11 +2445,12 @@ session began. It does not make sense in files to compile. This means that {\eauto} or {\eapply} didn't instantiate an 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. +You may backtrack to the faulty occurrence of {\eauto} or {\eapply} +and give the missing argument an explicit value. Alternatively, you +can use the commands \texttt{Show Existentials.} and +\texttt{Existential.} to display and instantiate the remainig +existential variables. -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. |