diff options
| -rw-r--r-- | doc/newfaq/main.tex | 7 |
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} |