proof irre

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

1 files changed, 5 insertions, 2 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 8905ff0d86..1fb5a81139 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -1916,13 +1916,14 @@ This is any logic which does not assume that ``A or not A''.
 
 \Question{What is proof-irrelevance ?}
 
+See question \ref{proof-irrelevance}
+
 
 \Question{What is the difference between opaque and transparent ?}{\label{opaque}}	
 
 Opaque definitions can not be unfolded but transparent ones can.
 
 
-
 \section{Troubleshooting}
 
 \Question{What can I do when {\tt Qed.} is slow ?}
@@ -1985,6 +1986,8 @@ theorem proving in \Coq.
 \bibliography{fk}
 
 %%%%%%%
+\typeout{*********************************************}
+\typeout{********* That makes \thequestion\space questions **********}
+\typeout{*********************************************}
 
-%\typeout{*** That makes \thequestion\space questions ***}
 \end{document}