Fix some typos in comments.

19 files changed, 41 insertions, 41 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 473b8dc82..973ff0b77 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -285,7 +285,7 @@ let default_logger level message =
 
 (** {6 File operations} *)
 
-(** A customized [stat] function. Exceptions are catched. *)
+(** A customized [stat] function. Exceptions are caught. *)
 
 type stats = MTime of float | NoSuchFile | OtherError
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 8269582df..c2b51dd39 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -71,7 +71,7 @@ val default_logger : Pp.message_level -> string -> unit
 
 (** {6 I/O operations} *)
 
-(** A customized [stat] function. Exceptions are catched. *)
+(** A customized [stat] function. Exceptions are caught. *)
 
 type stats = MTime of float | NoSuchFile | OtherError
 val stat : string -> stats
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d6c160c3d..3b0c93b32 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -38,7 +38,7 @@ open Pre_env
 (* In the function body [arg1] is represented by de Bruijn [n], and       *)
 (* [argn] by de Bruijn [1]                                                *)
 
-(* Representation of environements of mutual fixpoints :                  *)
+(* Representation of environments of mutual fixpoints :                  *)
 (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
 (*                ^<----------offset--------->                            *)
 (* type = [Ct1 | .... | Ctn]                                              *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 65d1de7e1..d762a246e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -823,7 +823,7 @@ let retroknowledge f senv =
 let register field value by_clause senv =
   (* todo : value closed, by_clause safe, by_clause of the proper type*)
   (* spiwack : updates the safe_env with the information that the register
-     action has to be performed (again) when the environement is imported *)
+     action has to be performed (again) when the environment is imported *)
   { senv with
     env = Environ.register senv.env field value;
     local_retroknowledge =
diff --git a/kernel/uint31.ml b/kernel/uint31.ml
index 3a0da2f62..d9c723c24 100644
--- a/kernel/uint31.ml
+++ b/kernel/uint31.ml
@@ -1,7 +1,7 @@
   (* Invariant: For arch64 all extra bytes are set to 0 *)
 type t = int 
     
-  (* to be used only on 32 bits achitectures *)
+  (* to be used only on 32 bits architectures *)
 let maxuint31 = Int32.of_string "0x7FFFFFFF"
 let uint_32 i =  Int32.logand (Int32.of_int i) maxuint31
     
@@ -16,7 +16,7 @@ let of_int_64 i = i land 0x7FFFFFFF
 let of_int = select of_int_32 of_int_64
 let of_uint i = i
  	
-    (* convertion of an uint31 to a string *)
+    (* conversion of an uint31 to a string *)
 let to_string_32 i = Int32.to_string (uint_32 i)
 let to_string_64 = string_of_int 
 
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
index e8b980809..d1f933cc4 100644
--- a/kernel/uint31.mli
+++ b/kernel/uint31.mli
@@ -5,7 +5,7 @@ val to_int : t -> int
 val of_int : int -> t
 val of_uint : int -> t
 
-     (* convertion to a string *)
+     (* conversion to a string *)
 val to_string : t -> string
 val of_string : string -> t
 
diff --git a/lib/errors.ml b/lib/errors.ml
index ab331d6a4..a4ec357ee 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -108,7 +108,7 @@ let _ = register_handler begin function
   | _ -> raise Unhandled
 end
 
-(** Critical exceptions shouldn't be catched and ignored by mistake
+(** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user. *)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index e4096a7ef..03caa6a9f 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -81,7 +81,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
 
-(** Critical exceptions shouldn't be catched and ignored by mistake
+(** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user.
     Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
diff --git a/library/assumptions.mli b/library/assumptions.mli
index 809e536b4..bb36a9725 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -27,7 +27,7 @@ module ContextObjectMap : Map.ExtS
 (** Collects all the objects on which a term directly relies, bypassing kernel
     opacity, together with the recursive dependence DAG of objects.
 
-    WARNING: some terms may not make sense in the environement, because they are
+    WARNING: some terms may not make sense in the environment, because they are
     sealed inside opaque modules. Do not try to do anything fancy with those
     terms apart from printing them, otherwise demons may fly out of your nose.
 *)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index a2577e2b0..f6a543a1c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -252,7 +252,7 @@ let coq_False_ref =
 
 (*
   [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
-  (the list of expresions on which we will do the matching)
+  (the list of expressions on which we will do the matching)
  *)
 let make_discr_match_el  =
   List.map (fun e -> (e,(Anonymous,None)))
@@ -674,7 +674,7 @@ and build_entry_lc_from_case env funname make_discr
 	   match el with brl end
 	   we first compute the list of lists corresponding to [el] and
 	   combine them .
-	   Then for each elemeent of the combinations,
+	   Then for each element of the combinations,
 	   we compute the result we compute one list per branch in [brl] and
 	   finally we just concatenate those list
 	*)
@@ -720,9 +720,9 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
-	(* alpha convertion to prevent name clashes *)
+	(* alpha conversion to prevent name clashes *)
 	let _,idl,patl,return = alpha_br avoid br in
-	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an indentifier *)
+	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
 	(* building a list of precondition stating that we are not in this branch
 	   (will be used in the following recursive calls)
 	*)
@@ -1149,7 +1149,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
 
-(* debuging wrapper *)
+(* debugging wrapper *)
 let rebuild_cons env nb_args relname args crossed_types rt =
 (*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
 (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
@@ -1163,7 +1163,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 (* naive implementation of parameter detection.
 
    A parameter is an argument which is only preceded by parameters and whose
-   calls are all syntaxically equal.
+   calls are all syntactically equal.
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
@@ -1178,7 +1178,7 @@ let rec compute_cst_params relnames params = function
       compute_cst_params relnames t_params b
   | GCases _ ->
       params  (* If there is still cases at this point they can only be
-		 discriminitation ones *)
+		 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
@@ -1272,7 +1272,7 @@ let do_build_inductive
   in
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
-    let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
+    let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
       let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
 	funargs
       in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b9d7e0d90..0ee887708 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -45,7 +45,7 @@ let pr_with_bindings prc prlc (c,bl) =
 let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
   pr_with_bindings prc prc  (c,bl)
 
-(* The local debuging mechanism *)
+(* The local debugging mechanism *)
 (* let msgnl = Pp.msgnl *)
 
 let observe strm =
@@ -255,12 +255,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig princ_type in
-    (* The number of args of the function is then easilly computable *)
+    (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
-    (* Since we cannot ensure that the funcitonnal principle is defined in the
-       environement and due to the bug #1174, we will need to pose the principle
+    (* Since we cannot ensure that the functional principle is defined in the
+       environment and due to the bug #1174, we will need to pose the principle
        using a name
     *)
     let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
@@ -522,12 +522,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig princ_type in
-    (* The number of args of the function is then easilly computable *)
+    (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
-    (* Since we cannot ensure that the funcitonnal principle is defined in the
-       environement and due to the bug #1174, we will need to pose the principle
+    (* Since we cannot ensure that the functional principle is defined in the
+       environment and due to the bug #1174, we will need to pose the principle
        using a name
     *)
     let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3dba232b..0cadffa4f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs =
        iraise (e, info));
     indexes
   else
-    (* we now search recursively amoungst all combinations *)
+    (* we now search recursively among all combinations *)
     (try
        List.iter
 	 (fun l ->
@@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
-(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
 (* Utilisé pour inférer le prédicat des Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7d1e0c9b5..142b54513 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags
 
 val all_and_fail_flags : inference_flags
 
-(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
 (** Generic call to the interpreter from glob_constr to open_constr, leaving
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 4ae64ae65..2b85ec872 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -134,7 +134,7 @@ exception FullyUnfocused
 exception CannotUnfocusThisWay
 
 (* This is raised when trying to focus on non-existing subgoals. It is
-   handled by an error message but one may need to catched it and
+   handled by an error message but one may need to catch it and
    settle a better error message in some case (suggesting a better
    bullet for example), see proof_global.ml function Bullet.pop and
    Bullet.push. *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a25683bfc..b6861fd49 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -192,8 +192,8 @@ let unfocus c sp =
     succeed).  Another benefit is that it is possible to write tactics
     that can be executed even if there are no focused goals.
     - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seens as a function (without argument) which returns a value of
-    type 'a and modifies the environement (in our case: the view).
+    seen as a function (without argument) which returns a value of
+    type 'a and modifies the environment (in our case: the view).
     Tactics of course have arguments, but these are given at the
     meta-level as OCaml functions.  Most tactics in the sense we are
     used to return [()], that is no really interesting values. But
@@ -1126,7 +1126,7 @@ module V82 = struct
     
 
   (* Returns the open goals of the proofview together with the evar_map to 
-     interprete them. *)
+     interpret them. *)
   let goals { comb = comb ; solution = solution; } =
    { Evd.it = comb ; sigma = solution }
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index ec255f6a1..5a9e7f39f 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -37,7 +37,7 @@ type entry
 val compact : entry -> proofview -> entry * proofview
 
 (** Initialises a proofview, the main argument is a list of
-    environements (including a [named_context] which are used as
+    environments (including a [named_context] which are used as
     hypotheses) pair with conclusion types, creating accordingly many
     initial goals. Because a proof does not necessarily starts in an
     empty [evar_map] (indeed a proof can be triggered by an incomplete
@@ -114,8 +114,8 @@ val unfocus : focus_context -> proofview -> proofview
     succeed).  Another benefit is that it is possible to write tactics
     that can be executed even if there are no focused goals.
     - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seens as a function (without argument) which returns a value of
-    type 'a and modifies the environement (in our case: the view).
+    seen as a function (without argument) which returns a value of
+    type 'a and modifies the environment (in our case: the view).
     Tactics of course have arguments, but these are given at the
     meta-level as OCaml functions.  Most tactics in the sense we are
     used to return [()], that is no really interesting values. But
@@ -230,7 +230,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
     [i] to [j] (see {!focus}). The rest of the goals is restored after
     the tactic action. If the specified range doesn't correspond to
     existing goals, fails with [NoSuchGoals] (a user error). this
-    exception is catched at toplevel with a default message + a hook
+    exception is caught at toplevel with a default message + a hook
     message that can be customized by [set_nosuchgoals_hook] below.
     This hook is used to add a suggestion about bullets when
     applicable. *)
@@ -547,7 +547,7 @@ module V82 : sig
   val grab : proofview -> proofview
 
   (* Returns the open goals of the proofview together with the evar_map to 
-     interprete them. *)
+     interpret them. *)
   val goals : proofview -> Evar.t list Evd.sigma
 
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
diff --git a/tactics/dnet.ml b/tactics/dnet.ml
index 61a358662..bb71620c0 100644
--- a/tactics/dnet.ml
+++ b/tactics/dnet.ml
@@ -121,7 +121,7 @@ struct
 	     Idset.union acc s2
 	 ) t Idset.empty)
 
-(*   (\* optimization hack: Not_found is catched in fold_pattern *\) *)
+(*   (\* optimization hack: Not_found is caught in fold_pattern *\) *)
 (*   let fast_inter s1 s2 = *)
 (*     if Idset.is_empty s1 || Idset.is_empty s2 then raise Not_found *)
 (*     else Idset.inter s1 s2 *)
@@ -176,7 +176,7 @@ struct
     let is_empty : t -> bool = function 
       | None -> false
       | Some s -> S.is_empty s
-    (* optimization hack: Not_found is catched in fold_pattern *)
+    (* optimization hack: Not_found is caught in fold_pattern *)
     let fast_inter s1 s2 =
       if is_empty s1 || is_empty s2 then raise Not_found
       else let r = inter s1 s2 in 
diff --git a/test-suite/bugs/closed/2406.v b/test-suite/bugs/closed/2406.v
index 1bd66ffcc..3766e795a 100644
--- a/test-suite/bugs/closed/2406.v
+++ b/test-suite/bugs/closed/2406.v
@@ -1,6 +1,6 @@
 (* Check correct handling of unsupported notations *)
 Notation "'’'" := (fun x => x) (at level 20).
 
-(* This fails with a syntax error but it is not catched by Fail
+(* This fails with a syntax error but it is not caught by Fail
 Fail Definition crash_the_rooster f := ’.
 *)
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index e39128cb8..65fe87801 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Various syntaxic shortands that are useful with [Program]. *)
+(** Various syntactic shorthands that are useful with [Program]. *)
 
 Require Export Coq.Program.Tactics.