diff options
| author | Enrico Tassi | 2014-01-07 10:24:12 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-07 10:24:40 +0100 |
| commit | 81492757797caef50d4eb3eb185f813463da883d (patch) | |
| tree | c71a4c4c17e1b5b5585cf41e291b57731ba98473 /kernel/pre_env.ml | |
| parent | 093529c6d4f8eba7370c30b97d8d648340039374 (diff) | |
STM: additional fix for STM + vm_compute
Thanks again Maximes.
This time the C value was stored in the env_(named|rel)_val of
the environment
Diffstat (limited to 'kernel/pre_env.ml')
| -rw-r--r-- | kernel/pre_env.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index b548348e05..5040df5aae 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -50,7 +50,7 @@ type stratification = { } type val_kind = - | VKvalue of values * Id.Set.t + | VKvalue of (values * Id.Set.t) Ephemeron.key | VKnone type lazy_val = val_kind ref |