Fix typos

3 files changed, 25 insertions, 25 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index a15db325..4d2d2d0e 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -124,7 +124,7 @@
     ["Double Hit Electric Terminator" coq-double-hit-toggle
      :style toggle
      :selected coq-double-hit-enable
-     :help "Automatically send commands when terminator typed twiced quickly."]
+     :help "Automatically send commands when terminator is typed twice quickly."]
     ("Auto Compilation"
      ["Compile Before Require"
       coq-compile-before-require-toggle
@@ -153,7 +153,7 @@
        :selected (eq coq-compile-quick 'no-quick)
        :active (and coq-compile-before-require
 		    coq-compile-parallel-in-background)
-       :help "Compile without -quick but accept existion .vio's"]
+       :help "Compile without -quick but accept existing .vio's"]
       ["quick no vio2vo"
        (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
        :style radio
@@ -202,7 +202,7 @@
        :active coq-compile-before-require
        :help "Save all buffers without confirmation"]
       )
-     ["Lock Ancesotors"
+     ["Lock Ancestors"
       coq-lock-ancestors-toggle
       :style toggle
       :selected coq-lock-ancestors
diff --git a/coq/coq.el b/coq/coq.el
index 662cc2e8..3eb5f0cb 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1225,7 +1225,7 @@ be called and no command will be sent to Coq."
 
 (defpacustom auto-adapt-printing-width t
   "If non-nil, adapt automatically printing width of goals window.
-Each timme the user sends abunch of commands to Coq, check if the
+Each time the user sends a bunch of commands to Coq, check if the
 width of the goals window changed, and adapt coq printing width.
 WARNING: If several windows are displaying the goals buffer, one
 is chosen arbitrarily.  WARNING 2: when backtracking the printing
@@ -1483,7 +1483,7 @@ fold/unfold cross.  Return the list of mappings hypname -> overlays."
   (cadr (assoc h coq-hyps-positions)))
 
 ;;;;;;;;;;;;;; Highlighting hypothesis ;;;;;;;;
-;; Feature: highlighting of hyptohesis that remains when the cript is played
+;; Feature: highlighting of hypothesis that remains when the script is played
 ;; (and goals buffer is updated).
 
 ;; On by default. This only works with the SearchAbout function for now.
@@ -1493,7 +1493,7 @@ fold/unfold cross.  Return the list of mappings hypname -> overlays."
 (defvar coq-highlight-hyps-sticky nil
   "If non-nil, try to make hypothesis highlighting sticky.
 The is try to re-highlight the hypothesis with same names
-after a refeshing of the response buffer.")
+after a refreshing of the response buffer.")
 
 ;; We maintain a list of hypothesis names that must be highlighted at each
 ;; regeneration of goals buffer.
@@ -1524,7 +1524,7 @@ buffer is updated."
 
 (defun coq-highlight-hyp (h)
   "Highlight hypothesis named H (sticky).
-use `coq-unhighlight-hyp' to unhilight."
+use `coq-unhighlight-hyp' to unhighlight."
   (unless (member h coq-highlighted-hyps)
     (setq coq-highlighted-hyps (cons h coq-highlighted-hyps)))
   (coq-highlight-hyp-aux h))
@@ -1801,7 +1801,7 @@ See  `coq-fold-hyp'."
 ;; Set to t to bring it back%%
 ;;
 ;; FIXME: this always sets proof-output-tooltips to nil, even if the user puts
-;; explicitely the reverse in it sconfig file. I just want to change the
+;; explicitly the reverse in it sconfig file. I just want to change the
 ;; *default* value to nil.
 (custom-set-default 'proof-output-tooltips nil)
 
@@ -2230,7 +2230,7 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 ;; after the proof, the evar line must be set back to what it was before the
 ;; proof. I therefore look in the urgent action hook if proof display is
 ;; switched on or off. When switched on, I test the current evar printing
-;; status with the undodumented command "Test Printing Dependent Evars Line" to
+;; status with the undocumented command "Test Printing Dependent Evars Line" to
 ;; remember if I have to switch evar printing off eventually.
 
 (defvar coq--proof-tree-must-disable-evars nil
@@ -2282,7 +2282,7 @@ properly after the proof and enable the evar printing."
   "Disable evar printing if necessary.
 This function switches off evar printing after the proof, if it
 was off before the proof.  For undo commands, we rely on the fact
-that Coq itself undos the effect of the evar printing change that
+that Coq itself undoes the effect of the evar printing change that
 we inserted after the goal statement.  We also rely on the fact
 that Proof General never backtracks into the middle of a
 proof.  (If this would happen, Coq would switch evar printing on
@@ -2299,7 +2299,7 @@ result of `coq-proof-tree-get-proof-info'."
 (defun coq-proof-tree-evar-display-toggle ()
   "Urgent action hook function for changing the evar printing status in Coq.
 This function is for `proof-tree-urgent-action-hook' (which is
-called only if external proof disaply is switched on).  It checks
+called only if external proof display is switched on).  It checks
 whether a proof was started or stopped and inserts commands for
 enableing and disabling the evar status line for Coq 8.6 or
 later.  Without the evar status line being enabled, prooftree
@@ -2779,7 +2779,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
   "Last error from `coq-get-last-error-location' and `coq-highlight-error'.")
 
 
-;; I don't use proof-shell-last-ouput here since it is not always set to the
+;; I don't use proof-shell-last-output here since it is not always set to the
 ;; really last output (specially when a *tactic* gives an error) instead I go
 ;; directly to the response buffer. This allows also to clean the response
 ;; buffer (better to only scroll it?)
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 56b9bbc6..b3026608 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -455,7 +455,7 @@ proof script@footnote{A @dfn{proof script} is a sequence of commands
  which constructs a proof, usually stored in a file.}
  in-place rather than line-by-line and later reassembling the pieces.
 Proof General keeps track of which proof steps have been processed by
-the prover, and prevents you editing them accidently.  You can undo
+the prover, and prevents you editing them accidentally.  You can undo
 steps as usual.
 
 The aim of Proof General is to provide a powerful and configurable
@@ -465,7 +465,7 @@ should be useful for large proof developments.
 
 Please help us!
 
-Send us comments, suggestsions, or (the best) patches to improve support
+Send us comments, suggestions, or (the best) patches to improve support
 for your chosen proof assistant.  Contact us at
 @uref{https://github.com/ProofGeneral/PG/issues}.
 
@@ -931,7 +931,7 @@ is, you can find the option anyway on the menu:
 which also shows the key binding.
 
 If you want to use electric terminator, you can customize Proof
-General to enable it everytime if you want, @xref{Customizing Proof
+General to enable it every time if you want, @xref{Customizing Proof
 General}.  For the common options, customization is easy: just
 use the menu item @code{Proof General -> Quick Options} to make your choices,
 and @code{Proof-General -> Quick Options -> Save Options} to
@@ -1614,7 +1614,7 @@ key-bindings and functions.
 
 @c TEXI DOCSTRING MAGIC: proof-display-some-buffers
 @deffn Command proof-display-some-buffers 
-Display the reponse, trace, goals, or shell buffer, rotating.@*
+Display the response, trace, goals, or shell buffer, rotating.@*
 A fixed number of repetitions of this command switches back to
 the same buffer.
 Also move point to the end of the response buffer if it's selected.
@@ -1914,7 +1914,7 @@ an error, you might want to see that.  You can select
 @lisp
 Proof-General -> Quick Options -> Display -> Sticky Errors
 @end lisp
-to add a higlight for regions which did not successfully process
+to add a highlight for regions which did not successfully process
 on the last attempt.  Whenever the region is edited, the
 highlight is removed. 
 
@@ -2005,7 +2005,7 @@ interactive command processed some text (i.e., wasn't an undo step
 backwards into the buffer) and processing didn't stop with an error.  To
 start automatic processing again after an error, simply hit @kbd{C-c
 C-n} after editing the buffer.  To turn the automatic processing on or
-off from the keyboard, you can use the keybinding:
+off from the keyboard, you can use the key binding:
 
 @table @kbd
 @item C-c >
@@ -3452,7 +3452,7 @@ buffers or refresh the window layout.  These are on the menu:
 
 @c TEXI DOCSTRING MAGIC: proof-display-some-buffers
 @deffn Command proof-display-some-buffers 
-Display the reponse, trace, goals, or shell buffer, rotating.@*
+Display the response, trace, goals, or shell buffer, rotating.@*
 A fixed number of repetitions of this command switches back to
 the same buffer.
 Also move point to the end of the response buffer if it's selected.
@@ -4427,13 +4427,13 @@ Documentation of the user option @code{coq-project-filename}:
 @c TEXI DOCSTRING MAGIC: coq-project-filename
 @defvar coq-project-filename 
 The name of coq project file.@*
-The coq project file of a coq developpement (Cf Coq documentation
+The coq project file of a coq development (Cf Coq documentation
 on "makefile generation") should contain the arguments given to
 coq_makefile. In particular it contains the -I and -R
 options (preferably one per line). If @samp{coq-use-coqproject} is
-t (default) the content of this file will be used by proofgeneral
+t (default) the content of this file will be used by Proof General
 to infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables
-that set the coqtop invocation by proofgeneral. This is now the
+that set the coqtop invocation by Proof General. This is now the
 recommended way of configuring the coqtop invocation. Local file
 variables may still be used to override the coq project file's
 configuration. .dir-locals.el files also work and override
@@ -5077,7 +5077,7 @@ one.  This is supported to any nesting depth that Coq allows.
 
 Warning! Using Coq commands for navigating inside the different proofs
 (@code{Resume} and especially @code{Suspend}) are not supported,
-backtracking will break syncronization.
+backtracking will break synchronization.
 
 @b{Special note:} The old feature that moved nested proofs outside the
 current proof is disabled.
@@ -5244,7 +5244,7 @@ keyboard command @code{isabelle-chose-logic} to choose from the list.
 
 The logics list is refreshed dynamically so you can select any newly
 built heap images in the same Emacs session.  However, notice that the
-choices are greyed out while Isabelle is actually runnning --- you can
+choices are greyed out while Isabelle is actually running --- you can
 only switch to a new logic if you first exit Isabelle (similarly to
 Proof General, Isabelle operates with only one logic at a time).
 
@@ -6139,7 +6139,7 @@ There was no 3.6 release of Proof General.
 Proof General version 3.7.1 is an updated and enhanced version
 of Proof General 3.7.  See  @file{CHANGES} for more details.
 
-Proof General version 3.7 collects together a cummulative set of
+Proof General version 3.7 collects together a cumulative set of
 improvements to Proof General 3.5.  There are compatibility fixes for
 newer Emacs versions, and particularly for GNU Emacs: credit is due to
 Stefan Monnier for an intense period of debugging and patching.  The