diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cProfile.mli | 2 | ||||
| -rw-r--r-- | lib/envars.mli | 2 | ||||
| -rw-r--r-- | lib/feedback.mli | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 2 | ||||
| -rw-r--r-- | lib/pp_diff.mli | 2 | ||||
| -rw-r--r-- | lib/spawn.mli | 2 | ||||
| -rw-r--r-- | lib/util.ml | 2 | ||||
| -rw-r--r-- | lib/util.mli | 2 |
9 files changed, 9 insertions, 9 deletions
diff --git a/lib/cProfile.mli b/lib/cProfile.mli index 764faf8d1a..00babe1a47 100644 --- a/lib/cProfile.mli +++ b/lib/cProfile.mli @@ -18,7 +18,7 @@ To trace a function "f" you first need to get a key for it by using : let fkey = declare_profile "f";; -(the string is used to print the profile infomation). Warning: this +(the string is used to print the profile information). Warning: this function does a side effect. Choose the ident you want instead "fkey". Then if the function has ONE argument add the following just after diff --git a/lib/envars.mli b/lib/envars.mli index ebf86d0650..558fe74042 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -38,7 +38,7 @@ val datadir : unit -> string (** [configdir] is the path to the installed config directory. *) val configdir : unit -> string -(** [set_coqlib] must be runned once before any access to [coqlib] *) +(** [set_coqlib] must be run once before any access to [coqlib] *) val set_coqlib : fail:(string -> string) -> unit (** [set_user_coqlib path] sets the coqlib directory explicitedly. *) diff --git a/lib/feedback.mli b/lib/feedback.mli index f407e2fd5b..c9e6ca1266 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -56,7 +56,7 @@ type feedback = { (** {6 Feedback sent, even asynchronously, to the user interface} *) -(* The interpreter assignes an state_id to the ast, and feedbacks happening +(* The interpreter assigns a state_id to the ast, and feedbacks happening * during interpretation are attached to it. *) diff --git a/lib/flags.mli b/lib/flags.mli index a70a23b902..535b46950e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,7 +64,7 @@ val beautify : bool ref val beautify_file : bool ref (* Coq quiet mode. Note that normal mode is called "verbose" here, - whereas [quiet] supresses normal output such as goals in coqtop *) + whereas [quiet] suppresses normal output such as goals in coqtop *) val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b diff --git a/lib/pp.mli b/lib/pp.mli index 4ce6a535c8..bc20a66824 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -18,7 +18,7 @@ (* to interpret. *) (* *) (* The datatype has a public view to allow serialization or advanced *) -(* uses, however regular users are _strongly_ warned againt its use, *) +(* uses, however regular users are _strongly_ warned against its use, *) (* they should instead rely on the available functions below. *) (* *) (* Box order and number is indeed an important factor. Try to create *) diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli index 03468271d2..0eec18bd5a 100644 --- a/lib/pp_diff.mli +++ b/lib/pp_diff.mli @@ -88,7 +88,7 @@ Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends in the middle of the string. Whitespace just before or just after a diff will not be part of the highlight. -Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be +Preexisting tags in pp may contain only a single Ppcmd_string. Those tags will be placed inside the diff tags to ensure proper nesting of tags within spans of "start.diff.*" ... "end.diff.*". diff --git a/lib/spawn.mli b/lib/spawn.mli index 944aa27a7f..24bbded4f1 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -9,7 +9,7 @@ (************************************************************************) (* This module implements spawning/killing managed processes with a - * synchronous or asynchronous comunication channel that works with + * synchronous or asynchronous communication channel that works with * threads or with a glib like main loop model. * * This module requires no threads and no main loop model. It takes care diff --git a/lib/util.ml b/lib/util.ml index 38d73d3453..6e8b8de5dc 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -14,7 +14,7 @@ let on_fst f (a,b) = (f a,b) let on_snd f (a,b) = (a,f b) let map_pair f (a,b) = (f a,f b) -(* Mapping under pairs *) +(* Mapping under triplets *) let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) diff --git a/lib/util.mli b/lib/util.mli index 1eb60f509a..9a00ee3440 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,7 +17,7 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(** Mapping under triple *) +(** Mapping under triplets *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd |