diff options
Diffstat (limited to 'src/Transfer/Syntax/Doc.tex')
| -rw-r--r-- | src/Transfer/Syntax/Doc.tex | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/Transfer/Syntax/Doc.tex b/src/Transfer/Syntax/Doc.tex index 9005ffcd0..46716f164 100644 --- a/src/Transfer/Syntax/Doc.tex +++ b/src/Transfer/Syntax/Doc.tex @@ -93,7 +93,6 @@ All other symbols are terminals.\\ \begin{tabular}{lll} {\nonterminal{ListImport}} & {\arrow} &{\emptyP} \\ - & {\delimit} &{\nonterminal{Import}} \\ & {\delimit} &{\nonterminal{Import}} {\terminal{;}} {\nonterminal{ListImport}} \\ \end{tabular}\\ @@ -106,7 +105,6 @@ All other symbols are terminals.\\ \begin{tabular}{lll} {\nonterminal{ListDecl}} & {\arrow} &{\emptyP} \\ - & {\delimit} &{\nonterminal{Decl}} \\ & {\delimit} &{\nonterminal{Decl}} {\terminal{;}} {\nonterminal{ListDecl}} \\ \end{tabular}\\ |