From d5d177e02c40a5ddbc5939375b9b6cf88d3d0da1 Mon Sep 17 00:00:00 2001
From: narboux
Date: Mon, 5 Apr 2004 13:17:30 +0000
Subject: *** empty log message ***

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

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index a1b269e8b7..51f75cd119 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -631,7 +631,6 @@ You can use the \rewrite {\tt in} tactic.
 
 You can use the \unfold tactic.
 
-
 \Question{How can I reduce some term ?}
 
 You can use the \simpl tactic.
@@ -699,21 +698,6 @@ intros...
 Qed.
 \end{coq_example}
 
-
-
-\Question{How can I change the order of the subgoals ?}
-
-You can use the \Focus command to concentrate on some goal. When the goal is proved you will see the remaining goals.
-
-
-\Question{How can I change the order of the hypothesis ?}
-
-You can use the {\tt move ... after} command.
-
-\Question{How can I change the name of an hypothesis ?}
-
-You can use the {\tt rename ... into} command.
-
 \Question{How can I do the opposite of the \intro tactic ?}
 
 You can use the \generalize tactic.
@@ -746,6 +730,23 @@ You should use the \eapply tactic, this will generate some goals containing meta
 Sometime you can use the \abstractt tactic, which makes as if you had
 stated some local lemma, this speeds up the typing process.
 
+
+\section{Proof management}
+
+
+
+\Question{How can I change the order of the subgoals ?}
+
+You can use the \Focus command to concentrate on some goal. When the goal is proved you will see the remaining goals.
+
+\Question{How can I change the order of the hypothesis ?}
+
+You can use the {\tt move ... after} command.
+
+\Question{How can I change the name of an hypothesis ?}
+
+You can use the {\tt rename ... into} command.
+
 \Question{How can use a proof which is not finished ?}
 
 You can use the {\tt Admitted} command to state your current proof as an axiom.
@@ -754,6 +755,12 @@ You can use the {\tt Admitted} command to state your current proof as an axiom.
 
 You can use the {\tt Admitted} command to state your current proof as an axiom.
 
+
+
+\section{Inductives}
+
+
+
 \Question{How can I prove that two constructors are different ?}
 
 You can use the \discriminate tactic.
@@ -765,9 +772,13 @@ discriminate.
 Qed.
 \end{coq_example}
 
+
+
 \Question{Do you know a coq-error-to-english translator ?}
 
 
+
+
 \subsection{Notations}
 
 \subsection{Modules}
-- 
cgit v1.2.3