Fixing typos - Part 2

5 files changed, 6 insertions, 6 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 963b7189f9..f772da69a4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -207,7 +207,7 @@ end) = struct
   let mk_relation env evd a = 
     app_poly env evd relation [| a |]
 
-  (** Build an infered signature from constraints on the arguments and expected output
+  (** Build an inferred signature from constraints on the arguments and expected output
       relation *)
     
   let build_signature evars env m (cstrs : (types * types option) option list)
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 0eb7726a18..8bd69dd4fd 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag =
   | General (* returns all possible successes *)
   | Select  (* returns all successes of the first matching branch *)
-  | Once    (* returns the first success in a maching branch
+  | Once    (* returns the first success in a matching branch
                (not necessarily the first) *)
 type global_flag = (* [gfail] or [fail] *)
   | TacGlobal
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index fd303f5d94..f839c3e886 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag =
   | General (* returns all possible successes *)
   | Select  (* returns all successes of the first matching branch *)
-  | Once    (* returns the first success in a maching branch
+  | Once    (* returns the first success in a matching branch
                (not necessarily the first) *)
 type global_flag = (* [gfail] or [fail] *)
   | TacGlobal
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 800be2565d..4a0b01bcdc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function
   | NamedHyp id ->
       (* If a name is bound, it has to be a quantified hypothesis *)
       (* user has to use other names for variables if these ones clash with *)
-      (* a name intented to be used as a (non-variable) identifier *)
+      (* a name intended to be used as a (non-variable) identifier *)
       try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id)
       with Not_found -> NamedHyp id
 
@@ -2075,7 +2075,7 @@ let _ =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun; poly; extra; } in
     let tac = interp_tactic ist tac in
-    (* EJGA: We sould also pass the proof name if desired, for now
+    (* EJGA: We should also pass the proof name if desired, for now
        poly seems like enough to get reasonable behavior in practice
      *)
     let name, poly = Id.of_string "ltac_gen", poly in
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 2b5e496168..7783661787 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -128,7 +128,7 @@ module PatternMatching (E:StaticEnvironment) = struct
 
   (** To focus on the algorithmic portion of pattern-matching, the
       bookkeeping is relegated to a monad: the composition of the
-      bactracking monad of {!IStream.t} with a "writer" effect. *)
+      backtracking monad of {!IStream.t} with a "writer" effect. *)
   (* spiwack: as we don't benefit from the various stream optimisations
      of Haskell, it may be costly to give the monad in direct style such as
      here. We may want to use some continuation passing style. *)