diff options
| author | Maxime Dénès | 2017-06-06 09:10:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 09:10:45 +0200 |
| commit | 9b44017963a742dacb381a9060f908ce421309fe (patch) | |
| tree | b5a8321c9d6e850ff6dac5fbf0666108697cdccd /lib | |
| parent | 98dc4f985f2ddd47b4d4d6afee901a0a2bb0bde0 (diff) | |
| parent | 62012e2d412d8586bd62b60beeb0b4005a66151f (diff) | |
Merge PR#728: A few typos.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cEphemeron.ml | 4 | ||||
| -rw-r--r-- | lib/cEphemeron.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/lib/cEphemeron.ml b/lib/cEphemeron.ml index a38ea11e10..890e02dc4e 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 1200e4e208..76cd7a5a8a 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 |