diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-03 09:11:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-03 20:33:00 +0200 |
| commit | 9075aa75fa4f10cab85273201b9b82dd78affef5 (patch) | |
| tree | 4e7db2e99ff6fc2dd05d949305bc6abbe3e1cb6a /parsing/pcoq.mli | |
| parent | c2279eea0b8666282e640637a74947ba554627d6 (diff) | |
Statment -> Statement
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 36e5e420a..00ca53884 100644 --- a/parsing/pcoq.mli +++ b/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, |