Fix misspellings in messages, man pages, and comments

This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.

21 files changed, 31 insertions, 31 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index cf62295d..13e14530 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -36,7 +36,7 @@ Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
 - a [Lbranch s] instruction.
 
   The [block_shape] type below describes all possible cases of structural
-  maching between an RTL instruction and an LTL basic block.
+  matching between an RTL instruction and an LTL basic block.
 *)
 
 Inductive move: Type :=
diff --git a/backend/Asmexpandaux.mli b/backend/Asmexpandaux.mli
index d80b4aec..e2320418 100644
--- a/backend/Asmexpandaux.mli
+++ b/backend/Asmexpandaux.mli
@@ -22,7 +22,7 @@ val emit: instruction -> unit
 val new_label: unit -> label
   (* Compute a fresh label *)
 val is_current_function_variadic: unit -> bool
-  (* Test wether the current function is a variadic function *)
+  (* Test whether the current function is a variadic function *)
 val get_current_function_args: unit -> typ list
   (* Get the types of the current function arguments *)
 val get_current_function_sig: unit -> signature
@@ -33,4 +33,4 @@ val get_current_function: unit -> coq_function
   (* Get the current function *)
 val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
   (* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
-     function to get the dwarf mapping of varibale names and for the expansion of simple instructions *)
+     function to get the dwarf mapping of variable names and for the expansion of simple instructions *)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 45051bcf..181f40bf 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -1249,7 +1249,7 @@ Proof.
     eapply external_call_nextblock; eauto.
     auto. auto.
 
-- (* return fron noninlined function *)
+- (* return from noninlined function *)
   inv MS0.
 + (* normal case *)
   left; econstructor; split.
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v
index 916e111b..8ac7c4ce 100644
--- a/backend/Unusedglob.v
+++ b/backend/Unusedglob.v
@@ -107,7 +107,7 @@ Definition used_globals (p: program) (pm: prog_map) : option IS.t :=
 
 (** * Elimination of unreferenced global definitions *)
 
-(** We also eliminate multiple definitions of the same global name, keeping ony
+(** We also eliminate multiple definitions of the same global name, keeping only
   the last definition (in program definition order). *)
 
 Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef unit)) :=
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 206ba421..5428d0cc 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -109,7 +109,7 @@ let atom_location a =
 
 let comp_env : composite_env ref = ref Maps.PTree.empty
 
-(** Hooks -- overriden in machine-dependent CPragmas module *)
+(** Hooks -- overridden in machine-dependent CPragmas module *)
 
 let process_pragma_hook = ref (fun (_: string) -> false)
 
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 7a4c49a2..8ab29fe9 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -84,7 +84,7 @@ Definition typeof (e: expr) : type :=
 (** ** Statements *)
 
 (** Clight statements are similar to those of Compcert C, with the addition
-  of assigment (of a rvalue to a lvalue), assignment to a temporary,
+  of assignment (of a rvalue to a lvalue), assignment to a temporary,
   and function call (with assignment of the result to a temporary).
   The three C loops are replaced by a single infinite loop [Sloop s1
   s2] that executes [s1] then [s2] repeatedly.  A [continue] in [s1]
diff --git a/common/AST.v b/common/AST.v
index 145f4919..a91138c9 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -432,12 +432,12 @@ Inductive external_function : Type :=
      (** A function from the run-time library.  Behaves like an
          external, but must not be redefined. *)
   | EF_vload (chunk: memory_chunk)
-     (** A volatile read operation.  If the adress given as first argument
+     (** A volatile read operation.  If the address given as first argument
          points within a volatile global variable, generate an
          event and return the value found in this event.  Otherwise,
          produce no event and behave like a regular memory load. *)
   | EF_vstore (chunk: memory_chunk)
-     (** A volatile store operation.   If the adress given as first argument
+     (** A volatile store operation.   If the address given as first argument
          points within a volatile global variable, generate an event.
          Otherwise, produce no event and behave like a regular memory store. *)
   | EF_malloc
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index cf67015a..7329767a 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -947,7 +947,7 @@ let binary_conversion env t1 t2 =
       end
   | _, _ -> assert false
 
-(* Conversion on function arguments (with protoypes) *)
+(* Conversion on function arguments (with prototypes) *)
 
 let argument_conversion env t =
   (* Arrays and functions degrade automatically to pointers *)
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index 2eaf6436..51dcab47 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -32,7 +32,7 @@ let max_error = ref 0
 let diagnostics_show_option = ref true
 
 (* Test if color diagnostics are available by testing if stderr is a tty
-   and if the environment varibale TERM is set
+   and if the environment variable TERM is set
 *)
 let color_diagnostics =
   let term = try Sys.getenv "TERM" with Not_found -> "" in
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index ded8019f..6a3c11c8 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -22,22 +22,22 @@ exception Abort
   (** Exception raised upon fatal errors *)
 
 val check_errors : unit -> unit
-  (** Check whether errors occured and raise abort if an error occured *)
+  (** Check whether errors occurred and raise abort if an error occurred *)
 
 type warning_type =
   | Unnamed                        (** warnings which cannot be turned off *)
   | Unknown_attribute              (** usage of unsupported/unknown attributes *)
-  | Zero_length_array              (** gnu extension for zero lenght arrays *)
+  | Zero_length_array              (** gnu extension for zero length arrays *)
   | Celeven_extension              (** C11 features *)
   | Gnu_empty_struct               (** gnu extension for empty struct *)
-  | Missing_declarations           (** declation which do not declare anything *)
+  | Missing_declarations           (** declaration which do not declare anything *)
   | Constant_conversion            (** dangerous constant conversions *)
   | Int_conversion                 (** pointer <-> int conversions *)
   | Varargs                        (** promotable vararg argument *)
   | Implicit_function_declaration  (** deprecated implicit function declaration *)
   | Pointer_type_mismatch          (** pointer type mismatch in ?: operator *)
   | Compare_distinct_pointer_types (** comparison between different pointer types *)
-  | Implicit_int                   (** implict int parameter or return type *)
+  | Implicit_int                   (** implicit int parameter or return type *)
   | Main_return_type               (** wrong return type for main *)
   | Invalid_noreturn               (** noreturn function containing return *)
   | Return_type                    (** void return in non-void function *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 13aab900..9cca930d 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -2632,7 +2632,7 @@ let elab_fundef genv spec name defs body loc =
      For prototyped functions this has been done by [elab_fundef_name]
      already, but some parameter may have been shadowed by the
      function name, while it should be the other way around, e.g.
-     [int f(int f) { return f+1; }], with [f] refering to the
+     [int f(int f) { return f+1; }], with [f] referring to the
      parameter [f] and not to the function [f] within the body of the
      function. *)
   let lenv =
diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages
index 95077739..6d972439 100644
--- a/cparser/handcrafted.messages
+++ b/cparser/handcrafted.messages
@@ -4477,7 +4477,7 @@ translation_unit_file: VOID PRE_NAME TYPEDEF_NAME PACKED LPAREN CONSTANT RPAREN
 ##
 
 # We have just parsed a list of attribute specifiers, but we cannot
-# print it because it is not available. We do not know wether it is
+# print it because it is not available. We do not know whether it is
 # part of the declaration or whether it is part of the first K&R parameter
 # declaration.
 
@@ -4599,7 +4599,7 @@ translation_unit_file: PACKED LPAREN BUILTIN_OFFSETOF XOR_ASSIGN
 ##
 
 Ill-formed __builtin_offsetof.
-At this point, an opening paranthesis '(' is expected.
+At this point, an opening parenthesis '(' is expected.
 
 #------------------------------------------------------------------------------
 
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 21c2ad19..3498a779 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -223,7 +223,7 @@ let name_to_definition: (string,int) Hashtbl.t = Hashtbl.create 7
 (* Mapping from atom to debug id *)
 let atom_to_definition: (atom, int) Hashtbl.t = Hashtbl.create 7
 
-(* Various lookup functions for defintions *)
+(* Various lookup functions for definitions *)
 let find_gvar_stamp id =
   let id = (Hashtbl.find stamp_to_definition id) in
   let var = Hashtbl.find definitions id in
@@ -342,7 +342,7 @@ let insert_global_declaration env dec =
           replace_var id ({var with gvar_declaration = false;})
         end
       end else begin
-        (* Implict declarations need special handling *)
+        (* Implicit declarations need special handling *)
         let id' = try Hashtbl.find name_to_definition id.name with Not_found ->
           let id' = next_id () in
           Hashtbl.add name_to_definition id.name id';id' in
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index c5df5637..bbfcf311 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -241,7 +241,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       let abbrev = !curr_abbrev in
       incr curr_abbrev;abbrev
 
-    (* Mapping from abbreviation string to abbreviaton id *)
+    (* Mapping from abbreviation string to abbreviation id *)
     let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7
 
     (* Mapping from abbreviation range id to label *)
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 0004e901..e1b71f13 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -595,7 +595,7 @@ let string_table: (string,int) Hashtbl.t = Hashtbl.create 7
 
 let gnu_string_entry s =
   if (String.length s < 4 && Configuration.system <> "macosx") (* macosx needs debug_str *)
-  || Configuration.system = "cygwin" then (*Cygwin does not use the debug_str seciton*)
+  || Configuration.system = "cygwin" then (*Cygwin does not use the debug_str section*)
     Simple_string s
   else
     try
diff --git a/doc/ccomp.1 b/doc/ccomp.1
index 1579beb9..7ccf97c8 100644
--- a/doc/ccomp.1
+++ b/doc/ccomp.1
@@ -430,7 +430,7 @@ Wrong return type for main.
 Enabled by default.
 .sp
 \fImissing\-declarations\fP:
-Declations which do not declare anything.
+Declarations which do not declare anything.
 Enabled by default.
 .sp
 \fIpointer\-type\-mismatch\fP:
diff --git a/driver/Commandline.mli b/driver/Commandline.mli
index 0f903af4..8bb6f18f 100644
--- a/driver/Commandline.mli
+++ b/driver/Commandline.mli
@@ -39,7 +39,7 @@ type action =
    patterns are tried in the order in which they appear in the list. *)
 
 exception CmdError of string
-(** Raise by [parse_cmdline] when an error occured *)
+(** Raise by [parse_cmdline] when an error occurred *)
 
 val parse_cmdline: (pattern * action) list -> unit
 (** [parse_cmdline actions] parses the command line (after @-file expansion)
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 929d9fd7..36b5c354 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -131,7 +131,7 @@ let gnu_prepro_opt_key key s =
 let gnu_prepro_opt s =
   prepro_options := s::!prepro_options
 
-(* Add gnu preprocessor option s and the implict -E *)
+(* Add gnu preprocessor option s and the implicit -E *)
 let gnu_prepro_opt_e s =
   prepro_options := s :: !prepro_options;
   option_E := true
@@ -171,7 +171,7 @@ let prepro_actions = [
   @ (if Configuration.gnu_toolchain then gnu_prepro_actions else [])
 
 let gnu_prepro_help =
-{|  -M            Ouput a rule suitable for make describing the
+{|  -M            Output a rule suitable for make describing the
                  dependencies of the main source file
   -MM            Like -M but do not mention system header files
   -MF <file>     Specifies file <file> as output file for -M or -MM
diff --git a/riscV/Asm.v b/riscV/Asm.v
index 1d8fda11..dc410a3b 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -369,7 +369,7 @@ lbl:
 - [Ploadfi rd fval]: similar to [Ploadli] but loads a double FP constant fval
   into a float register rd.
 
-- [Ploadsi rd fval]: similar to [Ploadli] but loads a singe FP constant fval
+- [Ploadsi rd fval]: similar to [Ploadli] but loads a single FP constant fval
   into a float register rd.
 
 - [Pallocframe sz pos]: in the formal semantics, this
diff --git a/test/c/chomp.c b/test/c/chomp.c
index c88cef5c..728e7a01 100644
--- a/test/c/chomp.c
+++ b/test/c/chomp.c
@@ -106,7 +106,7 @@ void dump_play(struct _play *play) /* and for the entire game tree */
 int get_value(int *data) /* get the value (0 or 1) for a specific _data */
 {
   struct _play *search;
-  search = game_tree; /* start at the begginig */
+  search = game_tree; /* start at the beginning */
   while (! equal_data(search -> state,data)) /* until you find a match */
       search = search -> next; /* take next element */
   return search -> value; /* return its value */
@@ -138,7 +138,7 @@ void show_list(struct _list *list) /* show the entire list of moves */
     }
 }
 
-void show_play(struct _play *play) /* to diplay the whole tree */
+void show_play(struct _play *play) /* to display the whole tree */
 {
   while (play != NULL)
     {
@@ -154,7 +154,7 @@ void show_play(struct _play *play) /* to diplay the whole tree */
 int in_wanted(int *data) /* checks if the current _data is in the wanted list */
 {
   struct _list *current;
-  current = wanted; /* start at the begginig */
+  current = wanted; /* start at the beginning */
   while (current != NULL) /* unitl the last one */
     {
       if (equal_data(current -> data,data)) break; /* break if found */
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 2e28e983..3025d2e7 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -103,7 +103,7 @@ let rec log2 n =
   assert (n > 0);
   if n = 1 then 0 else 1 + log2 (n lsr 1)
 
-(* System dependend printer functions *)
+(* System dependent printer functions *)
 module type SYSTEM =
     sig
       val raw_symbol: out_channel -> string -> unit