Merge PR #10203: Fixing typos - Part 1

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: gares
Reviewed-by: jfehrle
Reviewed-by: vbgl

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}