nettoyage

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

1 files changed, 5 insertions, 3 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 08123b7da..2277fc3f8 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -1161,6 +1161,8 @@ You can provide programs for your axioms.
 
 \Question{Can you explain me what an evaluable constant is ?}
 
+An evaluable constant is a constant which is unfoldable.
+
 \Question{What is a goal ?}
 
 The goal is the statement to be proved.
@@ -1170,14 +1172,14 @@ 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{What is a constr ?}
-
 \Question{What is Gallina ?}  
 
 Gallina is the specification language of \Coq. Complete documentation
 of this language can be found in the Reference Manual.
 
-\Question{What is a command ?}
+\Question{What is The Vernacular ?}  
+
+It is the language of commands of Gallina i.e. definitions, lemmas, \ldots  
 
 
 \Question{What is a dependent type ?}