aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-12-26 10:02:34 +0100
committerGuillaume Melquiond2016-12-26 10:11:41 +0100
commitdd710b9adbe7b27dccd6d4b21b90cb9bd07e5c07 (patch)
tree2953abfc518b395a67634f71ab483516e3324e8b /parsing
parent827370fb97c138c16509bd549eaeddf94ca13c99 (diff)
Fix some documentation typos.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/pcoq.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 54e6423877..a44d942992 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -40,7 +40,7 @@ module Gram : GrammarSig
| (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
|
@@ -128,7 +128,7 @@ val type_of_typed_entry : typed_entry -> entry_type
val object_of_typed_entry : typed_entry -> grammar_object Gram.entry
val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry
-(** Temporary activate camlp4 verbosity *)
+(** Temporarily activate camlp4 verbosity *)
val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit