Fixing typos - Part 3

9 files changed, 9 insertions, 9 deletions

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 635751bb24..c37e90650a 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -146,7 +146,7 @@ let do_assumptions ~program_mode kind nl l =
         l []
     else l
   in
-  (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
+  (* We interpret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
     let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
     let r = Retyping.relevance_of_type env sigma t in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 00f19f545c..a428c42e49 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -333,7 +333,7 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v
   | CStructRec na -> na
   | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
   | CMeasureRec (None,_,_) when not structonly ->
-    user_err Pp.(str "Decreasing argument must be specificed in measure clause.")
+    user_err Pp.(str "Decreasing argument must be specified in measure clause.")
   | _ -> user_err Pp.(str
            "Well-founded induction requires Program Fixpoint or Function.")
 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 642695bda4..6ac259b1fe 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -219,7 +219,7 @@ let declare_one_case_analysis_scheme ind =
   let kelim = elim_sorts (mib,mip) in
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
-       apropriate type *)
+       appropriate type *)
   if Sorts.List.mem InType kelim then
     ignore (define_individual_scheme dep UserAutomaticRequest None ind)
 
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index 1bb44d0ef1..f5e8b6d12f 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -206,7 +206,7 @@ let try_locate_absolute_library dir =
 type add_ml = AddNoML | AddTopML | AddRecML
 
 type vo_path_spec = {
-  unix_path : string;  (* Filesystem path contaning vo/ml files *)
+  unix_path : string;  (* Filesystem path containing vo/ml files *)
   coq_path  : DP.t;    (* Coq prefix for the path *)
   implicit  : bool;    (* [implicit = true] avoids having to qualify with [coq_path] *)
   has_ml    : add_ml;  (* If [has_ml] is true, the directory will also be search for plugins *)
diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli
index d393fc35b5..6605daa8d2 100644
--- a/vernac/loadpath.mli
+++ b/vernac/loadpath.mli
@@ -68,7 +68,7 @@ type add_ml = AddNoML | AddTopML | AddRecML
 
 type vo_path_spec = {
   unix_path : string;
-  (** Filesystem path contaning vo/ml files *)
+  (** Filesystem path containing vo/ml files *)
   coq_path  : Names.DirPath.t;
   (** Coq prefix for the path *)
   implicit  : bool;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 46c4422d17..ad175511b9 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -331,7 +331,7 @@ let default_tactic = ref (Proofview.tclUNIT ())
 let get_hide_obligations =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"Hidding of Program obligations"
+    ~name:"Hiding of Program obligations"
     ~key:["Hide";"Obligations"]
     ~value:false
 
diff --git a/vernac/search.ml b/vernac/search.ml
index e41378908f..a5663d65ef 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -28,7 +28,7 @@ type display_function = GlobRef.t -> env -> constr -> unit
 [SearchAbout ...], etc. to the names of the symbols matching the
 query, separated by a newline. This type of output is useful for
 editors (like emacs), to generate a list of completion candidates
-without having to parse thorugh the types of all symbols. *)
+without having to parse through the types of all symbols. *)
 
 type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b9d1326ba5..5ae572541e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -622,7 +622,7 @@ let vernac_end_proof ?pstate ?proof = function
 
 let vernac_exact_proof ~pstate c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
-     called only at the begining of a proof. *)
+     called only at the beginning of a proof. *)
   let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in
   let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom;
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 54e08d0e95..b37e527f47 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -22,7 +22,7 @@
      a query like Check.
 
    The classification works on the assumption that we have 3 states:
-   parsing, execution (global enviroment, etc...), and proof
+   parsing, execution (global environment, etc...), and proof
    state. For example, commands that only alter the proof state are
    considered safe to delegate to a worker.