Avertissement de la non- gravit� du message d'erreur de parsing de \/ et /\

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

1 files changed, 3 insertions, 6 deletions

diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 89895a8a31..9677d3b5fd 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -102,12 +102,9 @@ First, we find propositional calculus connectives:
 \ttindex{proj2}
 
 \begin{coq_eval}
-(* We restate the grammar rule for /\ and \/ since *)
-(* it is only valid to parce Coq.Init.Logic.and *)
-Grammar constr constr6 :=
-  myand [ constr5($c1) "/\\" constr6($c2) ] -> [ (and $c1 $c2) ]
-with constr7 :=
-  myor [ constr6($c1) "\\/" constr7($c2) ] -> [ (or $c1 $c2) ].
+(********** Next parsing errors for /\ and \/ are harmless ***********)
+(******************* since output is not displayed *******************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
 \end{coq_eval}
 \begin{coq_example*}
 Inductive True : Prop := I : True.