Fix some typos in comments.

3 files changed, 9 insertions, 9 deletions

diff --git a/proofs/proof.mli b/proofs/proof.mli
index 4ae64ae65f..2b85ec8724 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 a25683bfcf..b6861fd499 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 ec255f6a1a..5a9e7f39f0 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