*** empty log message ***

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

1 files changed, 31 insertions, 5 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index b0c248f65..eac92da90 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -519,17 +519,25 @@ You can use the \case or \destruct tactics.
 
 \Question[namedintros]{Why should I name my intros ?}
 
-When you use the \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.
+When you use the \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 \assert tactic. If you want to use backward reasoning (proving your goal using an assumption and then proving the assumption) use the \cut tactic.
+If you want to use forward reasoning (first proving the fact and then
+using it) You just need to use the \assert tactic. If you want to use
+backward reasoning (proving your goal using an assumption and then
+proving the assumption) use the \cut tactic.
 
 
 \Question[proofwith]{I want to automatize the use of some tactic how can I do it ?}
 
-You need to use the {\tt proof with T} command and add \ldots at the end of your sentences.
+You need to use the {\tt proof with T} command and add \ldots at the
+end of your sentences.
 
 For instance :
 \begin{coq_example}
@@ -589,7 +597,8 @@ You should use the \eapply tactic.
 
 \Question[abstract]{What can I do when {\tt Qed.} is slow ?}
 
-Sometime you can use the \abstractt tactic, which makes as if you had stated one intermediated lemmas, this speeds up the typing process.  
+Sometime you can use the \abstractt tactic, which makes as if you had
+stated one intermediated lemmas, this speeds up the typing process.
 
 
 %%%%%%%
@@ -663,10 +672,27 @@ The goal is the statement to be proved.
 A meta variable in \Coq represents a ``hole'', i.e. a part of a proof
 that is still unknown. 
 
-\Question[type]{What is Type(i) ?}
+\Question[constr]{What is a constr ?}
+
+\Question[gallina]{What is Gallina ?}
+
+\Question[command]{What is a command ?}
+
+\Question[lemmasvstheorem]{What is difference between a lemma, a fact  and a theorem ?}
+
+\Question[organize]{How can I organize my proofs ?}
 
 \Question[dependanttype]{What is a dependent type ?}
 
+\Question[coqlatex]{How can I generate some latex from my development ?}
+
+\Question[coqhtml]{How can I generate some HTML from my development ?}
+
+\Question[coqtex]{How can I cite some \Coq in my latex document ?}
+
+\Question[coqidedescr]{What is \CoqIde ?}
+
+
 
 \Question[reflection]{What is a proof by reflection ?}