diff options
Diffstat (limited to 'dev/v8-syntax')
| -rw-r--r-- | dev/v8-syntax/memo-v8.tex | 4 | ||||
| -rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 1 |
2 files changed, 2 insertions, 3 deletions
diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex index ae4b569b36..84894b6f7c 100644 --- a/dev/v8-syntax/memo-v8.tex +++ b/dev/v8-syntax/memo-v8.tex @@ -55,7 +55,7 @@ _ are allowed after the first character. Quoted strings are used typically to give a filename (which may not be a regular identifier). As before they are written between double quotes ("). Unlike for V7, there is no escape character: characters -are written normaly but the double quote which is doubled. +are written normally but the double quote which is doubled. \section{Main changes in terms w.r.t. V7} @@ -252,7 +252,7 @@ became \TERM{context}. Syntax is unified with subterm matching. \subsection{Occurrences} -To avoid ambiguity between a numeric literal and the optionnal +To avoid ambiguity between a numeric literal and the optional occurrence numbers of this term, the occurrence numbers are put after the term itself. This applies to tactic \TERM{pattern} and also \TERM{unfold} diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index dd3908c25f..601d52ddda 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1167,7 +1167,6 @@ $$ \nlsep \TERM{Show}~\OPT{\NT{num}} \nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}} \nlsep \TERM{Show}~\TERM{Node} -\nlsep \TERM{Show}~\TERM{Script} \nlsep \TERM{Show}~\TERM{Existentials} \nlsep \TERM{Show}~\TERM{Tree} \nlsep \TERM{Show}~\TERM{Conjecture} |