*** empty log message ***

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

1 files changed, 11 insertions, 3 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index dd2f437090..d13ce7b8bb 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -234,7 +234,8 @@ Qed.
 \Question[conjonctionhyp]{My goal contains a conjunction as an hypothesis, how can I use it ?}
 
 If you want to decompose your hypohtesis into other hypothesis you can use the {\tt decompose} tactic :
- \begin{coq_example*}
+
+\begin{coq_example*}
 Goal forall A B:Prop, A/\B-> B.
 intros.
 decompose [and] H.
@@ -348,12 +349,19 @@ Qed.
 
 \Question[trivial]{My goal is ???, how can I prove it ?}
 
+
+\Question[namedintros]{Why should I name my intros ?}
+
+When you use the {\tt intro} tactic you don't have to give a name to your hyphothesis. If you do so the names will be generated by \Coq but your scripts won't be modular. If you add some hyphothesis to your theorem (or change their order), you will have to change your proof to adapt to the new names.
+
+
 \Question[assert]{I want to state a fact that I will use later as an hypothesis, how can I do it ?}
 
 If you want to use forward reasoning (first proving the fact and then using it) You just need to use the {\tt assert} tactic. If you want to use backward reasoning (proving your goal using an assumption and then proving the assumption) use the {\tt cut} tactic.
 
-\begin{coq_example*}
-\end{coq_example*}
+
+
+
 
 \Question[proofwith]{I want to automatize the use of some tactic how can I do it ?}