Fixing typos - Part 3

9 files changed, 12 insertions, 12 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 6dd9a976f9..71d71cd3ca 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -99,7 +99,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   (* This is important: The [Global] and [Proof Theorem] parts of the
      goal_kind are not relevant here as build_constant_by_tactic does
      use the noop terminator; but beware if some day we remove the
-     redundancy on constrant declaration. This opens up an interesting
+     redundancy on constraint declaration. This opens up an interesting
      question, how does abstract behave when discharge is local for example?
   *)
   let goal_kind, suffix = if opaque
@@ -164,7 +164,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let inst = match const.Entries.const_entry_universes with
   | Entries.Monomorphic_entry _ -> EInstance.empty
   | Entries.Polymorphic_entry (_, ctx) ->
-    (* We mimick what the kernel does, that is ensuring that no additional
+    (* We mimic what the kernel does, that is ensuring that no additional
        constraints appear in the body of polymorphic constants. Ideally this
        should be enforced statically. *)
     let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 1fae4c3d9d..1170c1acd0 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -30,7 +30,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
   if check_scheme kind ind then
     (* 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 *)
     let cte, eff = find_scheme kind ind in
     let sigma, cte = Evd.fresh_constant_instance env sigma cte in
     let c = mkConstU cte in
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index e75a61d0c6..1a0b7f84cf 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -30,7 +30,7 @@ open Proofview.Notations
 open Tacmach.New
 open Tactypes
 
-(* This file containts the implementation of the tactics ``Decide
+(* This file contains the implementation of the tactics ``Decide
    Equality'' and ``Compare''. They can be used to decide the
    propositional equality of two objects that belongs to a small
    inductive datatype --i.e., an inductive set such that all the
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 6f3e08ea02..7381d5f77b 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -132,7 +132,7 @@ val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic
 
 (* Replace term *)
 (* [replace_term dir_opt c cl]
-   perfoms replacement of [c] by the first value found in context
+   performs replacement of [c] by the first value found in context
    (according to [dir] if given to get the rewrite direction)  in the clause [cl]
 *)
 val replace_term : bool option -> constr -> clause -> unit Proofview.tactic
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index e1dad9ad20..5ac28cb9e2 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -25,7 +25,7 @@ open Context.Rel.Declaration
 module RelDecl = Context.Rel.Declaration
 
 (* I implemented the following functions which test whether a term t
-   is an inductive but non-recursive type, a general conjuction, a
+   is an inductive but non-recursive type, a general conjunction, a
    general disjunction, or a type with no constructors.
 
    They are more general than matching with or_term, and_term, etc,
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index b8c3ddb0f0..696b11d9db 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -35,7 +35,7 @@ open Coqlib
    contained in the arguments of the application *)
 
 (** I implemented the following functions which test whether a term [t]
-   is an inductive but non-recursive type, a general conjuction, a
+   is an inductive but non-recursive type, a general conjunction, a
    general disjunction, or a type with no constructors.
 
    They are more general than matching with [or_term], [and_term], etc,
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 6efa1ece9c..8cc481e30e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -98,7 +98,7 @@ let get_local_sign sign =
   in
   List.fold_right add_local lid nil_sign
 *)
-(* returs the identifier of lid that was the latest declared in sign.
+(* returns the identifier of lid that was the latest declared in sign.
  * (i.e. is the identifier id of lid such that
  * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
  * for any id'<>id in lid).
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index dcd63fe760..2467671d38 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -481,7 +481,7 @@ module New = struct
       ) <*>
         tclUNIT res
 
-  (* Try the first thats solves the current goal *)
+  (* Try the first that's solves the current goal *)
   let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 
   let tclPROGRESS t =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9dafa8bad9..191f00d104 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3019,14 +3019,14 @@ let specialize (c,lbind) ipat =
       (* We grab names used in product to remember them at re-abstracting phase *)
       let typ_of_c_hd = pf_get_type_of gl c_hd in
       let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in
-      (* accumulator args: arguments to apply to c_hd: all infered
+      (* accumulator args: arguments to apply to c_hd: all inferred
          args + re-abstracted rels *)
       let rec rebuild_lambdas sigma lprd args hd l =
         match lprd , l with
         | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args))
         | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t ->
           (* nme has not been resolved, let us re-abstract it. Same
-             name but type updated by instanciation of other args. *)
+             name but type updated by instantiation of other args. *)
           let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in
           let r = Retyping.relevance_of_type env sigma new_typ_of_t in
           let liftedargs = List.map liftrel args in
@@ -4292,7 +4292,7 @@ let induction_tac with_evars params indvars elim =
   let elimc = contract_letin_in_lam_header sigma elimc in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
   let elimclause = Tacmach.New.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
-  (* elimclause' is built from elimclause by instanciating all args and params. *)
+  (* elimclause' is built from elimclause by instantiating all args and params. *)
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in