From 9b8b58dcd51b1ceebd2c73503477c9c20e980243 Mon Sep 17 00:00:00 2001
From: narboux
Date: Thu, 29 Apr 2004 12:22:59 +0000
Subject: nettoyage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8555 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/newfaq/main.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 08123b7da1..2277fc3f83 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 ?}
-- 
cgit v1.2.3