diff options
| author | herbelin | 2001-12-23 13:06:57 +0000 |
|---|---|---|
| committer | herbelin | 2001-12-23 13:06:57 +0000 |
| commit | e0f4ef6c39d77f9c7dcb1f7e91432c92ccd4bc42 (patch) | |
| tree | 375167cdaf4c67b7add7b4ae01d8f3b364e096a9 | |
| parent | e720440da85b92f8a8b8e6c1964737340702559a (diff) | |
MAJ 7.2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8262 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |