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

---
 doc/sphinx/proof-engine/ltac.rst                     | 4 ++--
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 +++---
 doc/sphinx/proof-engine/tactics.rst                  | 4 ++--
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index bbd7e0ba3d..fed7111628 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -708,7 +708,7 @@ tactic
       for printing.
 
    By copying the definition of :tacn:`time_constr` from the standard library,
-   users can achive support for a fixed pattern of nesting by passing
+   users can achieve support for a fixed pattern of nesting by passing
    different :token:`string` parameters to :tacn:`restart_timer` and
    :tacn:`finish_timing` at each level of nesting.
 
@@ -1676,7 +1676,7 @@ It is possible to measure the time spent in invocations of primitive
 tactics as well as tactics defined in |Ltac| and their inner
 invocations. The primary use is the development of complex tactics,
 which can sometimes be so slow as to impede interactive usage. The
-reasons for the performence degradation can be intricate, like a slowly
+reasons for the performance degradation can be intricate, like a slowly
 performing |Ltac| match or a sub-tactic whose performance only
 degrades in certain situations. The profiler generates a call tree and
 indicates the time spent in a tactic depending on its calling context. Thus
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 75e019592f..b19b0742c1 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -853,7 +853,7 @@ An *occurrence switch* can be:
   algorithm in a local definition, instead of copying large terms by
   hand.
 
-It is important to remember that matching *preceeds* occurrence
+It is important to remember that matching *precedes* occurrence
 selection.
 
   .. example::
@@ -2455,7 +2455,7 @@ the holes are abstracted in term.
      Lemma test : True.
      have: _ * 0 = 0.
 
-  The invokation of ``have`` is equivalent to:
+  The invocation of ``have`` is equivalent to:
 
   .. coqtop:: reset none
 
@@ -4927,7 +4927,7 @@ bookkeeping steps.
      apply/PQequiv.
 
   thus in this case, the tactic ``apply/PQequiv`` is equivalent to
-  ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is tha analogue of
+  ``apply: (iffRL (PQequiv _ _))``, where ``iffRL`` is the analogue of
   ``iffRL`` for the converse implication.
 
 Any |SSR| term whose type coerces to a double implication can be
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4e47621938..2ee23df019 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3714,7 +3714,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
    .. cmdv:: Hint Resolve -> @term : @ident
 
       Adds the left-to-right implication of an equivalence as a hint (informally
-      the hint will be used as :n:`apply <- @term`, although as mentionned
+      the hint will be used as :n:`apply <- @term`, although as mentioned
       before, the tactic actually used is a restricted version of
       :tacn:`apply`).
 
@@ -3783,7 +3783,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
       This sets the transparency flag used during unification of
       hints in the database for all constants or all variables,
-      overwritting the existing settings of opacity. It is advised
+      overwriting the existing settings of opacity. It is advised
       to use this just after a :cmd:`Create HintDb` command.
 
    .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident
-- 
cgit v1.2.3