aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.mli
diff options
context:
space:
mode:
authorJPR2019-05-23 23:28:55 +0200
committerJPR2019-05-23 23:28:55 +0200
commitd306f5428db0d034aea55d3f0699c67c1f296cc1 (patch)
tree540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /stm/stm.mli
parent5cfdc20560392c2125dbcee31cfd308d5346b428 (diff)
Fixing typos - Part 3
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 24c672c973..5e1e9bf5ad 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -50,7 +50,7 @@ type stm_doc_type =
| VioDoc of string (* file path *)
| Interactive of interactive_top (* module path *)
-(** Coq initalization options:
+(** Coq initialization options:
- [doc_type]: Type of document being created.
@@ -63,7 +63,7 @@ type stm_doc_type =
*)
type stm_init_options = {
(* The STM will set some internal flags differently depending on the
- specified [doc_type]. This distinction should dissappear at some
+ specified [doc_type]. This distinction should disappear at some
some point. *)
doc_type : stm_doc_type;
@@ -86,7 +86,7 @@ type stm_init_options = {
(** The type of a STM document *)
type doc
-(** [init_core] performs some low-level initalization; should go away
+(** [init_core] performs some low-level initialization; should go away
in future releases. *)
val init_core : unit -> unit