From e6322e23958a937fa01960f8ce320717b9863253 Mon Sep 17 00:00:00 2001
From: JPR
Date: Tue, 21 May 2019 23:07:55 +0200
Subject: Fixing typos - Part 1

---
 dev/v8-syntax/memo-v8.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/v8-syntax')

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}
-- 
cgit v1.2.3