diff options
| author | Théo Zimmermann | 2019-05-24 16:36:46 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-24 16:36:46 +0200 |
| commit | 5727443376480be4793757fd5507621ad4f09509 (patch) | |
| tree | 2fff9e86c24d1d6d82c3ed59919d3b3de4112189 /stm | |
| parent | 5596cf352d1c265fd5627dc19416d2b55c10f2b7 (diff) | |
| parent | be40007de49140d403bb1dad1af9f4f1e3fe5003 (diff) | |
Merge PR #10233: Fixing typos - Part 3
Reviewed-by: Zimmi48
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | stm/stm.mli | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 3b5323a3b8..e32b6c9f1c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2657,10 +2657,10 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initalization routine *) +(* Main initialization routine *) 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; @@ -3113,7 +3113,7 @@ let ind_len_loc_of_id sid = let compute_indentation ?loc sid = Option.cata (fun loc -> let open Loc in - (* The effective lenght is the lenght on the last line *) + (* The effective length is the length on the last line *) let len = loc.ep - loc.bp in let prev_indent = match ind_len_loc_of_id sid with | None -> 0 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 |