From c1a77be5df23c0a5b9f973c10b6fee42c42fec1b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 23 Dec 2001 13:27:44 +0000
Subject: 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
---
 doc/RefMan-lib.tex | 9 +++------
 1 file 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. 
-- 
cgit v1.2.3