Merge branch 'v8.5'

2 files changed, 2 insertions, 2 deletions

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index 9e243eead..6a69c5793 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -167,7 +167,7 @@ kernel/univ.ml was modified. The new API forces every universe to be
 declared before it is mentionned in any constraint. This forces to
 declare every universe to be >= Set or > Set. Every universe variable
 introduced during elaboration is >= Set. Every _global_ universe is now
-declared explicitely > Set, _after_ typechecking the definition. In
+declared explicitly > Set, _after_ typechecking the definition. In
 polymorphic definitions Type@{i} ranges over Set and any other universe
 j. However, at instantiation time for polymorphic references, one can
 try to instantiate a universe parameter with Prop as well, if the
diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex
index 8d116de26..ae4b569b3 100644
--- a/dev/v8-syntax/memo-v8.tex
+++ b/dev/v8-syntax/memo-v8.tex
@@ -253,7 +253,7 @@ became \TERM{context}. Syntax is unified with subterm matching.
 \subsection{Occurrences}
 
 To avoid ambiguity between a numeric literal and the optionnal
-occurence numbers of this term, the occurence numbers are put after
+occurrence numbers of this term, the occurrence numbers are put after
 the term itself. This applies to tactic \TERM{pattern} and also
 \TERM{unfold}
 \begin{transbox}