From 212215f774d4945f5adaa2319488e5b8859daaf6 Mon Sep 17 00:00:00 2001
From: kirchner
Date: Fri, 12 Mar 2004 13:52:04 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8491 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/newfaq/core.tex |  8 ++++++--
 doc/newfaq/main.tex | 10 +++++++++-
 2 files changed, 15 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/newfaq/core.tex b/doc/newfaq/core.tex
index 0ab238f59c..2e65ea7f19 100644
--- a/doc/newfaq/core.tex
+++ b/doc/newfaq/core.tex
@@ -1,2 +1,6 @@
-Gallina ? \\
-tactiques, tacticals, par cas (logique, entiers, constructeurs...)
+\subsection{Predicate Calculus}
+
+\subsection{Induction}
+
+\subsection{Modules}
+
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 023202a623..a49d1dcd2c 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -1,5 +1,6 @@
 
 \documentclass[a4paper]{faq}
+\pagestyle{plain}
 
 % yay les symboles
 \usepackage{stmaryrd}
@@ -42,7 +43,14 @@ pointers to other references when possible.
 
 \newpage
 \section{Introduction}
-
+This FAQ is the sum of the questions that came to mind as we developed
+proofs in \Coq. Since we are singularly short-minded, we wrote the
+answers we found on bits of papers to have them at hand whenever the
+situation occurs again. This, is the result of that: a collection of
+tips one can refer to when proofs become intricate. Yes, this means we
+won't take the blame for the shortcomings of the following. But if you
+want to contribute and send in your own tricks, feel free to write to
+us...
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 								     %
-- 
cgit v1.2.3