Merge PR coq#7691: Fixing spelling of statment/statement in two API t…

…ypes

parsing/extend.ml

@@ -116,14 +116,14 @@ and 'a rules =
 type 'a production_rule =
 | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
 
-type 'a single_extend_statment =
+type 'a single_extend_statement =
   string option *
   (** Level *)
   gram_assoc option *
   (** Associativity *)
   'a production_rule list
   (** Symbol list with the interpretation function *)
 
-type 'a extend_statment =
+type 'a extend_statement =
   gram_position option *
-  'a single_extend_statment list
+  'a single_extend_statement list

parsing/pcoq.ml

@@ -79,10 +79,10 @@ module type S =
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
   type production_rule = symbol list * action
-  type single_extend_statment =
+  type single_extend_statement =
       string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
+  type extend_statement =
+      Gramext.position option * single_extend_statement list
   type coq_parsable
 
   val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
@@ -105,10 +105,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
   type production_rule = symbol list * action
-  type single_extend_statment =
+  type single_extend_statement =
       string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
+  type extend_statement =
+      Gramext.position option * single_extend_statement list
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
@@ -207,9 +207,9 @@ let camlp5_verbosity silent f x =
 
 (** Grammar extensions *)
 
-(** NB: [extend_statment =
-         gram_position option * single_extend_statment list]
-    and [single_extend_statment =
+(** NB: [extend_statement =
+         gram_position option * single_extend_statement list]
+    and [single_extend_statement =
          string option * gram_assoc option * production_rule list]
     and [production_rule = symbol list * action]
 
@@ -263,7 +263,7 @@ let of_coq_extend_statement (pos, st) =
 type gram_reinit = gram_assoc * gram_position
 
 type extend_rule =
-| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule
+| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule
 
 type ext_kind =
   | ByGrammar of extend_rule

parsing/pcoq.mli

@@ -65,10 +65,10 @@ module type S =
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
   type production_rule = symbol list * action
-  type single_extend_statment =
+  type single_extend_statement =
       string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
+  type extend_statement =
+      Gramext.position option * single_extend_statement list
 
   type coq_parsable
 
@@ -264,7 +264,7 @@ type gram_reinit = gram_assoc * gram_position
 (** Type of reinitialization data *)
 
 val grammar_extend : 'a Gram.entry -> gram_reinit option ->
-  'a Extend.extend_statment -> unit
+  'a Extend.extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
@@ -279,7 +279,7 @@ type 'a grammar_command
     marshallable. *)
 
 type extend_rule =
-| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule
+| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statement -> extend_rule
 
 type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 (** Grammar extension entry point. Given some ['a] and a current grammar state,