diff options
| author | JPR | 2019-05-21 23:07:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-21 23:07:55 +0200 |
| commit | e6322e23958a937fa01960f8ce320717b9863253 (patch) | |
| tree | 79e2a8c8e7c953c44b3880fa683d82f2a6e6cc85 /dev/v8-syntax | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Fixing typos - Part 1
Diffstat (limited to 'dev/v8-syntax')
| -rw-r--r-- | dev/v8-syntax/memo-v8.tex | 4 |
1 files changed, 2 insertions, 2 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} |