*** empty log message ***

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

1 files changed, 8 insertions, 8 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 9f1b796930..5c26a19d3e 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -756,15 +756,15 @@ 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.
+\begin{coq_example}
+Inductive toto : Set := 
+	C1 : toto
+      | C2 : toto.
 
-%Goal C1 <> C2.
-%discriminate.
-%Qed.
-%\end{coq_example}
+Goal C1 <> C2.
+discriminate.
+Qed.
+\end{coq_example}
 
 
 \Question[coqccoqtop]{What is the difference between coqc et coqtop ?}