aboutsummaryrefslogtreecommitdiff
path: root/kernel/pre_env.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/pre_env.mli')
-rw-r--r--kernel/pre_env.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 35223db82f..964d709cff 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -36,11 +36,11 @@ type stratification = {
env_engagement : engagement option
}
-type val_kind =
- | VKvalue of (values * Id.Set.t) Ephemeron.key
- | VKnone
+type lazy_val
-type lazy_val = val_kind ref
+val force_lazy_val : lazy_val -> (values * Id.Set.t) option
+val dummy_lazy_val : unit -> lazy_val
+val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
type named_vals = (Id.t * lazy_val) list