From 59ebf574a127e660d0293fc736ac5de8f98e89ff Mon Sep 17 00:00:00 2001
From: narboux
Date: Mon, 5 Apr 2004 10:20:13 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8532 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/newfaq/main.tex | 16 ++++++++--------
 1 file 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 ?}
-- 
cgit v1.2.3