From f8d503e1696329f886f7f58fde4597066e68c524 Mon Sep 17 00:00:00 2001
From: kirchner
Date: Mon, 5 Apr 2004 10:49:02 +0000
Subject: *** empty log message ***

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

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 5c26a19d3e..7af94ca003 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -501,7 +501,9 @@ Qed.
 
 \Question[assumption2bis]{What can be the difference between applying one hypotheses or another in the context of the last question ?}
 
-From a proof point of view it is equivalent but if you want to extract a program from your proof, the two hyphoteses can lead to different programs.
+From a proof point of view it is equivalent but if you want to extract
+a program from your proof, the two hyphoteses can lead to different
+programs.
 
 
 \subsubsection{Automation}
@@ -755,18 +757,13 @@ You can use the {\tt Admitted} command to state your current proof as an axiom.
 
 You can use the \discriminate tactic.
 
-
 \begin{coq_example}
-Inductive toto : Set := 
-	C1 : toto
-      | C2 : toto.
-
+Inductive toto : Set := C1 : toto | C2 : toto.
 Goal C1 <> C2.
 discriminate.
 Qed.
 \end{coq_example}
 
-
 \Question[coqccoqtop]{What is the difference between coqc et coqtop ?}
 
 \Question[coqerror]{Do you know a coq-error-to-english translator ?}
@@ -861,7 +858,7 @@ You can increase the depth of the proof search or add some lemmas in the base of
 
 PS: Notice for people that are interested in proof rendering that Assert
 and Pose (and Cut) are not rendered the same as Generalize (see the
-HELM experimental rendering tool at http://mowgli.cs.unibo.it, link
+HELM experimental rendering tool at \url{http://mowgli.cs.unibo.it}, link
 HELM, link COQ Online). Indeed Generalize builds a beta-expanded term
 while Assert, Pose and Cut uses a let-in.
 
@@ -987,7 +984,7 @@ Program extraction consist in generating a program from a constructive proof.
 
 You can extract your programs to Objective Caml and Haskell.
 
-\Question[extraaxiom]{How can I change extract an incomplete proof ?}
+\Question[extraaxiom]{How can I extract an incomplete proof ?}
 
 You can provide programs for your axioms.
 
-- 
cgit v1.2.3