*** empty log message ***

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

1 files changed, 34 insertions, 1 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index d13ce7b8bb..b86a4ffade 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -268,18 +268,40 @@ 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*}
+Goal forall A B:Prop, A-> A\/B.
+intros.
+tauto.
+Qed.
+\end{coq_example*}
 
 \Question[firstorder]{My goal is a first order formula, how can I prove it ?}
 
 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*}
+Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
+intros.
+congruence.
+Qed.
+\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*}
+%Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
+%intros.
+%congruence.
+%Qed.
+%\end{coq_example*}
+
 
 \Question[ring]{My goal is an equality on some ring (e.g. natural numbers), how can I prove it ?}
 
@@ -311,9 +333,20 @@ Qed.
 \end{coq_example*}
 
 
-
 \Question[omega]{My goal is an inequality on R, how can I prove it ?}
 
+
+%\begin{coq_example*}
+%Require Import ZArith.
+%Require Omega.
+%Open Local Scope Z_scope.
+%Goal forall a : Z, a*a>0. 
+%intros.
+%omega.
+%Qed.
+%\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 ?}
 
 Just use the {\tt gb} tactic.