diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 21:01:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-06-04 19:25:22 +0200 |
| commit | 62012e2d412d8586bd62b60beeb0b4005a66151f (patch) | |
| tree | 53c3f21b2f972a383c4b603bcae11bd13d257a6f | |
| parent | b91f5d1adbd039809e31b5311d06b376829de1fc (diff) | |
A few typos.
| -rw-r--r-- | kernel/names.ml | 2 | ||||
| -rw-r--r-- | kernel/names.mli | 4 | ||||
| -rw-r--r-- | lib/cEphemeron.ml | 4 | ||||
| -rw-r--r-- | lib/cEphemeron.mli | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index ae3403335..d7c0a5e98 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -590,7 +590,7 @@ module Constant = KerPair module Cmap = HMap.Make(Constant.CanOrd) (** A map whose keys are constants (values of the {!Constant.t} type). - Keys are ordered wrt. "cannonical form" of the constant. *) + Keys are ordered wrt. "canonical form" of the constant. *) module Cmap_env = HMap.Make(Constant.UserOrd) (** A map whose keys are constants (values of the {!Constant.t} type). diff --git a/kernel/names.mli b/kernel/names.mli index c73eb197b..004d52d4b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -379,9 +379,9 @@ module Cset_env : CSig.SetS with type elt = Constant.t module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset (** A map whose keys are constants (values of the {!Constant.t} type). - Keys are ordered wrt. "cannonical form" of the constant. *) + Keys are ordered wrt. "canonical form" of the constant. *) -module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env +module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env (** A map whose keys are constants (values of the {!Constant.t} type). Keys are ordered wrt. "user form" of the constant. *) diff --git a/lib/cEphemeron.ml b/lib/cEphemeron.ml index a38ea11e1..890e02dc4 100644 --- a/lib/cEphemeron.ml +++ b/lib/cEphemeron.ml @@ -35,10 +35,10 @@ end) would make the key always reachable) *) let values : Obj.t HT.t = HT.create 1001 -(* To avoid a race contidion between the finalization function and +(* To avoid a race condition between the finalization function and get/create on the values hashtable, the finalization function just enqueues in an imperative list the item to be collected. Being the list - imperative, even if the Gc enqueue an item while run_collection is operating, + imperative, even if the Gc enqueues an item while run_collection is operating, the tail of the list is eventually set to Empty on completion. Kudos to the authors of Why3 that came up with this solution for their implementation of weak hash tables! *) diff --git a/lib/cEphemeron.mli b/lib/cEphemeron.mli index 1200e4e20..76cd7a5a8 100644 --- a/lib/cEphemeron.mli +++ b/lib/cEphemeron.mli @@ -26,7 +26,7 @@ Proposed solution: Turn all occurrences of [bad] into [bad key] in your data structure. - Use [crate bad_val] to obtain a unique key [k] for [bad_val], and store + Use [create bad_val] to obtain a unique key [k] for [bad_val], and store [k] in the data structure. Use [get k] to obtain [bad_val]. An ['a key] can always be marshalled. When marshalled, a key loses its |