From e0f4ef6c39d77f9c7dcb1f7e91432c92ccd4bc42 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 23 Dec 2001 13:06:57 +0000
Subject: MAJ 7.2

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8262 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-syn.tex | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 790c7c27c3..569ca5c041 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -587,6 +587,11 @@ Reset Initial.
 forbid blanks with a rule that declares ``\verb+|-+'' as a single
 token:
 
+\begin{coq_eval}
+(********** The following is not correct and should produce **********)
+(*************** Syntax error: illegal begin of vernac ***************)
+(* Just to adjust the prompt: *) Set Printing Depth 50.
+\end{coq_eval}
 \begin{coq_example}
 Grammar vernac vernac := 
   thesis [ "|-" constr:constr($term) "." ]
@@ -868,7 +873,7 @@ ne\_identarg\_list} is already defined with type {\tt ast list} but the
 % Test failure
 \begin{coq_example}           
 Grammar tactic ne_identarg_list :=
-  list_two [ identarg($id1) identarg($id2) ] -> [ $id1 $id2 ]. 
+  list_two [ identarg($id1) identarg($id2) ] -> [ $id1 ; $id2 ]. 
 \end{coq_example}
 
 All rules of a same grammar must have the same type. For instance, the
-- 
cgit v1.2.3