*** empty log message ***

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

1 files changed, 22 insertions, 6 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index f5e8fc69c9..7742eb7782 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -96,6 +96,7 @@ Cours de Gilles
 Manuel de Coq
 
 \item[Inductives]
+
 Habilitation Christine
 
 \item[Co-Inductives]
@@ -111,8 +112,8 @@ Pierre Letouzey
 \section{Documentation}
 
 \Question[coqdocumentation]{Where can I find documentation about \Coq ?} 
-All the documentation about \Coq, from the reference manual to
-friendly tutorials and documentation of the standard library, is
+All the documentation about \Coq, from the reference manual \cite{coqmanual} to
+friendly tutorials \cite{Coq:Tutorial} and documentation of the standard library, is
 available online at 
 \mbox{\tt http://pauillac.inria.fr/coq/doc-eng.html}.
 All these documents are viewable either in browsable html, or as
@@ -205,7 +206,6 @@ The goal is the statement to be proved.
 \Question[dependanttype]{What is a dependent type ?}
 
 
-
 \Question[conjonction]{My goal is a conjonction, how can I prove it ?}
 
 Use some theorem or assumption or use the {\tt split} tactic.
@@ -268,10 +268,16 @@ Use the {\tt assumption} 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.
+For instance :
+
 \Question[complete]{I want to execute the proofwith tactic only if it solves the goal, how can I do it ?}
 
+You need to use the {\tt solve} tactic.
+
 \Question[subgoalsorder]{How can I change the order of the subgoals ?}
 
+
 \Question[hyphotesisorder]{How can I change the order of the hypothesis ?}
 
 \Question[ifsyntax]{What is the syntax for if ?}
@@ -293,20 +299,30 @@ For more information see  \cite{howe,harrison,boutin} and the last chapter of th
 
 \Ltac is the tactic language for \Coq.
 
+\Question[ltacerror]{Why do I always get the same error message ?}
+
+
+\Question[ltacprint]{Is there any printing command in \Ltac ?}
+
+You can use the {\tt Idtac} tactic with a string argument. Thsi string
+will be printed out.
+The same applies to the 
+{\tt fail} tactic
+
 \Question[letltac]{What is the syntax for let in \Ltac ?}
 
 \Question[matchltac]{What is the syntax for pattern matching in \Ltac ?}
+
 \Question[matchsem]{What is the semantic for match context ?}
 
 \Question[fresh]{How can I generate a new name ?}
 
+You can use the following syntax :
+{\tt Let id:=fresh in }
 
 \Question[statdyn]{How can I define static and dynamic code ?}
 
 
-
-
-
 \section{Conclusion and Farewell.}
 \label{ccl}