*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8514 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 22 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index c77b948675..2eddaa202e 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -220,26 +220,26 @@ Windows. The sources can be easily adapted to all platforms supporting Objective
 \Question[conjonction]{My goal is a conjunction, how can I prove it ?}
 
 Use some theorem or assumption or use the {\tt split} tactic.
-\begin{coq_example*}
+\begin{coq_example}
 Goal forall A B:Prop, A->B-> A/\B.
 intros.
 split.
 assumption.
 assumption.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 \Question[conjonctionhyp]{My goal contains a conjunction as an hypothesis, how can I use it ?}
 
 If you want to decompose your hypohtesis into other hypothesis you can use the {\tt decompose} tactic :
 
-\begin{coq_example*}
+\begin{coq_example}
 Goal forall A B:Prop, A/\B-> B.
 intros.
 decompose [and] H.
 assumption.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 
 \Question[disjonction]{My goal is a disjonction, how can I prove it ?}
@@ -249,13 +249,13 @@ You can prove the left part or the right part of the disjunction using
 reasoning step, use {\tt } to prove the right part with the assumption
 that the left part of the disjunction is false.
 
-\begin{coq_example*}
+\begin{coq_example}
 Goal forall A B:Prop, A-> A\/B.
 intros.
 left.
 assumption.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 
 
@@ -274,12 +274,12 @@ Use some theorem or assumption or exhibits the witness using {\tt exists} tactic
 \Question[taut]{My goal is a propositional tautology, how can I prove it ?}
 
 Just use the {\tt tauto} tactic.
-\begin{coq_example*}
+\begin{coq_example}
 Goal forall A B:Prop, A-> A\/B.
 intros.
 tauto.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 \Question[firstorder]{My goal is a first order formula, how can I prove it ?}
 
@@ -290,30 +290,30 @@ Just use the {\tt firstorder} tactic.
 \Question[cong]{My goal is solvable by a sequence of rewrites, how can I prove it ?}
 
 Just use the {\tt congruence} tactic.
-\begin{coq_example*}
+\begin{coq_example}
 Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
 intros.
 congruence.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 
 \Question[congnot]{My goal is disequality solvable by a sequence of rewrites, how can I prove it ?}
 
 Just use the {\tt congruence} tactic.
-%\begin{coq_example*}
+%\begin{coq_example}
 %Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
 %intros.
 %congruence.
 %Qed.
-%\end{coq_example*}
+%\end{coq_example}
 
 
 \Question[ring]{My goal is an equality on some ring (e.g. natural numbers), how can I prove it ?}
 
 Just use the {\tt ring} tactic.
 
-\begin{coq_example*}
+\begin{coq_example}
 Require Import ZArith.
 Require Ring.
 Open Local Scope Z_scope.
@@ -321,13 +321,13 @@ Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b.
 intros.
 ring.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 \Question[field]{My goal is an equality on some field (e.g. reals), how can I prove it ?}
 
 Just use the {\tt field} tactic.
 
-\begin{coq_example*}
+\begin{coq_example}
 Require Import Reals.
 Require Ring.
 Open Local Scope R_scope.
@@ -336,13 +336,13 @@ intros.
 field.
 assumption.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 
 \Question[omega]{My goal is an inequality on R, how can I prove it ?}
 
 
-%\begin{coq_example*}
+%\begin{coq_example}
 %Require Import ZArith.
 %Require Omega.
 %Open Local Scope Z_scope.
@@ -350,7 +350,7 @@ Qed.
 %intros.
 %omega.
 %Qed.
-%\end{coq_example*}
+%\end{coq_example}
 
 
 \Question[gb]{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it ?}
@@ -361,7 +361,7 @@ Just use the {\tt gb} tactic.
 
 Just use the {\tt apply} tactic.
 
-\begin{coq_example*}
+\begin{coq_example}
 Lemma mylemma : forall x, x+0 = x.
 auto.
 Qed.
@@ -369,7 +369,7 @@ Qed.
 Goal 3+0 = 3.
 apply mylemma.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 \Question[autowith]{My goal is solvable by  some lemma within a set of lemmas and I don't want to remember which one, how can I prove it ?}
 
@@ -379,12 +379,12 @@ Use a base of Hints.
 
 Use the {\tt assumption} tactic.
 
-\begin{coq_example*}
+\begin{coq_example}
 Goal 1=1 -> 1=1.
 intro.
 assumption.
 Qed.
-\end{coq_example*}
+\end{coq_example}
 
 \Question[trivial]{My goal is ???, how can I prove it ?}