diff options
| -rwxr-xr-x | doc/RefMan-syn.tex | 7 |
1 files changed, 6 insertions, 1 deletions
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 |