Fix some typos in comments.

1 files changed, 8 insertions, 8 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index a2577e2b0..f6a543a1c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -252,7 +252,7 @@ let coq_False_ref =
 
 (*
   [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
-  (the list of expresions on which we will do the matching)
+  (the list of expressions on which we will do the matching)
  *)
 let make_discr_match_el  =
   List.map (fun e -> (e,(Anonymous,None)))
@@ -674,7 +674,7 @@ and build_entry_lc_from_case env funname make_discr
 	   match el with brl end
 	   we first compute the list of lists corresponding to [el] and
 	   combine them .
-	   Then for each elemeent of the combinations,
+	   Then for each element of the combinations,
 	   we compute the result we compute one list per branch in [brl] and
 	   finally we just concatenate those list
 	*)
@@ -720,9 +720,9 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
-	(* alpha convertion to prevent name clashes *)
+	(* alpha conversion to prevent name clashes *)
 	let _,idl,patl,return = alpha_br avoid br in
-	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an indentifier *)
+	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
 	(* building a list of precondition stating that we are not in this branch
 	   (will be used in the following recursive calls)
 	*)
@@ -1149,7 +1149,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
 
-(* debuging wrapper *)
+(* debugging wrapper *)
 let rebuild_cons env nb_args relname args crossed_types rt =
 (*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
 (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
@@ -1163,7 +1163,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 (* naive implementation of parameter detection.
 
    A parameter is an argument which is only preceded by parameters and whose
-   calls are all syntaxically equal.
+   calls are all syntactically equal.
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
@@ -1178,7 +1178,7 @@ let rec compute_cst_params relnames params = function
       compute_cst_params relnames t_params b
   | GCases _ ->
       params  (* If there is still cases at this point they can only be
-		 discriminitation ones *)
+		 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
@@ -1272,7 +1272,7 @@ let do_build_inductive
   in
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
-    let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
+    let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
       let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
 	funargs
       in