aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
authorHugo Herbelin2015-10-13 11:40:22 +0200
committerHugo Herbelin2015-10-18 20:11:14 +0200
commitc8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff (patch)
tree2db781cc2a505a805fc53abac8d422b1192aef1e /stm
parentc70ee60ed1603658eb33f4ae39b1a0be81bf45c6 (diff)
Miscellaneous typos, spacing, US spelling in comments or variable names.
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 5bb46fd368..88a1fbbf48 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -639,7 +639,7 @@ end = struct (* {{{ *)
proof,
Summary.project_summary (States.summary_of_state system) summary_pstate
- let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
+ let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
let is_cached ?(cache=`No) id =
if Stateid.equal id !cur_id then
@@ -1912,7 +1912,7 @@ let init () =
Backtrack.record ();
Slaves.init ();
if Flags.async_proofs_is_master () then begin
- prerr_endline "Initialising workers";
+ prerr_endline "Initializing workers";
Query.init ();
let opts = match !Flags.async_proofs_private_flags with
| None -> []