Mise en place avertissements pour rep�rer les erreurs volontaires de coq-tex

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

1 files changed, 5 insertions, 0 deletions

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index a83a2a74ef..e127a0d791 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -503,6 +503,11 @@ This command gives the status of the \Coq\ module {\dirpath}. If the module is l
 This command displays the full name of the qualified identifier {\qualid}
 and consequently the \Coq\ module in which it is defined.
 
+\begin{coq_eval}
+(***************** The last line should produce **************************)
+(************* Error: I.Dont.Exist not a defined object ******************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Locate nat.
 Locate Datatypes.O.