diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-24 13:39:06 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-24 13:39:06 +0100 |
| commit | 9ddae1778aef70c55a1347c4d0b28694cf34a5af (patch) | |
| tree | 8d89834ee9ada62eb58dffefba110e9477381164 /parsing | |
| parent | 989553966c7ba1a2cc23fd10fc2633dcb0f98648 (diff) | |
Fix some documentation typos.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ec8dac821..37165f6ce 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -39,7 +39,7 @@ module Gram : module type of Compat.GrammarMake(CLexer) | (together with a constr entry level, e.g. 50, and indications of) | (subentries, e.g. x in constr next level and y constr same level) | - | spliting into tokens by Metasyntax.split_notation_string + | splitting into tokens by Metasyntax.split_notation_string V [String "x"; String "+"; String "y"] : symbol_token list | @@ -96,7 +96,7 @@ module Gram : module type of Compat.GrammarMake(CLexer) *) -(** Temporary activate camlp4 verbosity *) +(** Temporarily activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -232,14 +232,14 @@ type gram_reinit = gram_assoc * gram_position val grammar_extend : 'a Gram.entry -> gram_reinit option -> 'a Extend.extend_statment -> unit -(** Extend the grammar of Coq, without synchronizing it with the bactracking +(** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) (** {5 Extending the parser with summary-synchronized commands} *) module GramState : Store.S -(** Auxilliary state of the grammar. Any added data must be marshallable. *) +(** Auxiliary state of the grammar. Any added data must be marshallable. *) type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be |