aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar kirchner <kirchner@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-29 11:23:41 +0000
committerGravatar kirchner <kirchner@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-29 11:23:41 +0000
commitea220e2f442c392a2f9a9178476b186a83e44510 (patch)
tree3af23c668a1b464e141173a18588a9303f4606f0
parent33bdcfd5787d5200c8c568083278122fa66d63e9 (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8522 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/newfaq/main.tex3
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 3bb6ecf06..3102302b9 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -676,6 +676,8 @@ Ltac introIdGen := let id:=fresh in intro id.
\Question[statdyn]{How can I define static and dynamic code ?}
+
+
%%%%%%%
\subsection{Glossary}
@@ -732,7 +734,6 @@ and the last chapter of the Coq'Art.
\Question[coqidedescr]{What is \CoqIde ?}
-
\section{Extraction}
\Question[extraction]{What is program extraction ?}