Fixing typos - Part 2

6 files changed, 11 insertions, 11 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bb66658a37..fe50bd4b08 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -107,7 +107,7 @@ let _show_inactive_notations () =
 let deactivate_notation nr =
   match nr with
   | SynDefRule kn ->
-     (* shouldn't we check wether it is well defined? *)
+     (* shouldn't we check whether it is well defined? *)
      inactive_notations_table := IRuleSet.add nr !inactive_notations_table
   | NotationRule (scopt, ntn) ->
      match availability_of_notation (scopt, ntn) (scopt, []) with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 753065b7dd..31f3736bae 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1229,7 +1229,7 @@ let add_local_defs_and_check_length loc env g pl args = match g with
      let maxargs = Inductiveops.constructor_nalldecls env cstr in
      if List.length pl' + List.length args > maxargs then
        error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
-     (* Two possibilities: either the args are given with explict
+     (* Two possibilities: either the args are given with explicit
      variables for local definitions, then we give the explicit args
      extended with local defs, so that there is nothing more to be
      added later on; or the args are not enough to have all arguments,
@@ -1467,7 +1467,7 @@ let alias_of als = match als.alias_ids with
 
     @returns a raw_case_pattern_expr :
     - no notations and syntactic definition
-    - global reference and identifeir instead of reference
+    - global reference and identifier instead of reference
 
 *)
 
@@ -1642,7 +1642,7 @@ let drop_notations_pattern looked_for genv =
     | CPatCast (_,_) ->
       (* We raise an error if the pattern contains a cast, due to
          current restrictions on casts in patterns. Cast in patterns
-         are supportted only in local binders and only at top
+         are supported only in local binders and only at top
          level. In fact, they are currently eliminated by the
          parser. The only reason why they are in the
          [cases_pattern_expr] type is that the parser needs to factor
diff --git a/interp/declare.mli b/interp/declare.mli
index 2ffde31fc0..795d9a767d 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -40,7 +40,7 @@ type internal_flag =
   | InternalTacticRequest
   | UserIndividualRequest
 
-(* Defaut definition entries, transparent with no secctx or proj information *)
+(* Default definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?univs:Entries.universes_entry ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 806fe93297..f3cdd64633 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -96,11 +96,11 @@ let set_maximality imps b =
   this kind if there is enough arguments to infer them)
 
 - [DepFlex] means that the implicit argument can be found by unification
-  along a collapsable path only (e.g. as x in (P x) where P is another
+  along a collapsible path only (e.g. as x in (P x) where P is another
   argument) (we do (defensively) print the arguments of this kind)
 
 - [DepFlexAndRigid] means that the least argument from which the
-  implicit argument can be inferred is following a collapsable path
+  implicit argument can be inferred is following a collapsible path
   but there is a greater argument from where the implicit argument is
   inferable following a rigid path (useful to know how to print a
   partial application)
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ccdd448460..1099074c63 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -34,7 +34,7 @@ val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
 
 (** {6 ... } *)
 (** An [implicits_list] is a list of positions telling which arguments
-    of a reference can be automatically infered *)
+    of a reference can be automatically inferred *)
 
 
 type argument_position =
@@ -50,11 +50,11 @@ type implicit_explanation =
 	  this kind if there is enough arguments to infer them) *)
   | DepFlex of argument_position
       (** means that the implicit argument can be found by unification
-	  along a collapsable path only (e.g. as x in (P x) where P is another
+          along a collapsible path only (e.g. as x in (P x) where P is another
 	  argument) (we do (defensively) print the arguments of this kind) *)
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
       (** means that the least argument from which the
-	  implicit argument can be inferred is following a collapsable path
+          implicit argument can be inferred is following a collapsible path
 	  but there is a greater argument from where the implicit argument is
 	  inferable following a rigid path (useful to know how to print a
 	  partial application) *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 49273c4146..a7e1de736c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -48,7 +48,7 @@ let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
     match onlyparse with
     | None ->
       (* Redeclare it to be used as (short) name in case an other (distfix)
-	 notation was declared inbetween *)
+         notation was declared in between *)
       Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
     | _ -> ()
   end