Fixing typos - Part 2

7 files changed, 13 insertions, 13 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 287a374ab1..cffe8a3e78 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -658,7 +658,7 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 
 	*)
 	(fun g ->
-(* 	   observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *)
+(* 	   observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *)
 	   thin [hid] g
 	)
       )
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e9a2c285d0..f51c6dc6be 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -429,11 +429,11 @@ let get_funs_constant mp =
     let l_const = get_funs_constant const f in
     (*
        We need to check that all the functions found are in the same block
-       to prevent Reset stange thing
+       to prevent Reset strange thing
     *)
     let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in
     let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in
-    (* all the paremeter must be equal*)
+    (* all the parameters must be equal*)
     let _check_params =
       let first_params = List.hd l_params  in
       List.iter
@@ -514,7 +514,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
       )
       fas
   in
-  (* We create the first priciple by tactic *)
+  (* We create the first principle by tactic *)
   let first_type,other_princ_types =
     match l_schemes with
 	s::l_schemes -> s,l_schemes
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e15e167ff3..4c67d65816 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1369,7 +1369,7 @@ let do_build_inductive
 	(rebuild_return_type returned_types.(i))
     in
     (* We need to lift back our work topconstr but only with all information
-       We mimick a Set Printing All.
+       We mimic a Set Printing All.
        Then save the graphs and reset Printing options to their primitive values
     *)
     let rel_arities = Array.mapi rel_arity funsargs in
@@ -1438,7 +1438,7 @@ let do_build_inductive
       (rebuild_return_type returned_types.(i))
   in
   (* We need to lift back our work topconstr but only with all information
-     We mimick a Set Printing All.
+     We mimic a Set Printing All.
      Then save the graphs and reset Printing options to their primitive values
   *)
   let rel_arities = Array.mapi rel_arity funsargs in
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 481a8be3ba..24b3690138 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -55,7 +55,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr
     Glob_term.cases_pattern * Id.Map.key list *
       Id.t Id.Map.t
 
-(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
+(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result respects barendregt
    conventions and  does not share bound variables with avoid
 *)
 val alpha_rt : Id.t list -> glob_constr -> glob_constr
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 40f66ce5eb..48cf040919 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -115,7 +115,7 @@ let eq = lazy(EConstr.of_constr (coq_constant "eq"))
 let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 
 (*****************************************************************)
-(* Copy of the standart save mechanism but without the much too  *)
+(* Copy of the standard save mechanism but without the much too  *)
 (* slow reduction function                                       *)
 (*****************************************************************)
 open Entries
@@ -357,7 +357,7 @@ let add_Function is_general f =
 
 let pr_table env sigma = pr_table env sigma !from_function
 (*********************************)
-(* Debuging *)
+(* Debugging *)
 let functional_induction_rewrite_dependent_proofs = ref true
 let function_debug = ref false
 open Goptions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index edb698280f..2a0140f02c 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -591,7 +591,7 @@ let rec reflexivity_with_destruct_cases g =
 
 
 (* [prove_fun_complete funs graphs schemes lemmas_types_infos i]
-   is the tactic used to prove completness lemma.
+   is the tactic used to prove completeness lemma.
 
    [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions
    (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct.
@@ -748,7 +748,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
   let map (c, u) = mkConstU (c, EInstance.make u) in
   let funs_constr = Array.map map funs  in
-  (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+  (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
   funind_purify
     (fun () ->
      let env = Global.env () in
@@ -928,7 +928,7 @@ let revert_graph kn post_tac hid g =
    [hid] is the hypothesis to invert, [fconst] is the function to invert and  [f_correct]
    is the correctness lemma for [fconst].
 
-   The sketch is the follwing~:
+   The sketch is the following~:
    \begin{enumerate}
    \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$
    (fails if it is not possible)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1fca132655..216be3797b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1584,7 +1584,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 			   spc () ++ str"is defined" )
       )
   in
-  (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+  (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
   funind_purify (fun () ->
       let pstate = com_terminate
           tcc_lemma_name