Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).

It is in section "My goal is ..., how can I prove it?" of the FAQ.

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

1 files changed, 11 insertions, 0 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 0e5b00d37..080450745 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -96,6 +96,7 @@
 \def\symmetryin{{\tt symmetryin}}
 \def\instantiate{{\tt instantiate}}
 \def\inversion{{\tt inversion}}
+\def\specialize{{\tt specialize}}
 \def\Defined{{\tt Defined}}
 \def\Qed{{\tt Qed}}
 \def\pattern{{\tt pattern}}
@@ -867,6 +868,16 @@ provide names for these variables: {\Coq} will do it anyway, but such
 automatic naming decreases legibility and robustness.
 
 
+\Question{My goal contains an universally quantified statement, how can I use it?}
+
+If the universally quantified assumption matches the goal you can
+use the {\apply} tactic. If it is an equation you can use the
+{\rewrite} tactic. Otherwise you can use the {\specialize} tactic
+to instantiate the quantified variables with terms. The variant
+{\tt assert(Ht := H t)} makes a copy of assumption {\tt H} before
+instantiating it.
+
+
 \Question{My goal is an existential, how can I prove it?}
 
 Use some theorem or assumption or exhibit the witness using the {\existstac} tactic.