diff options
Diffstat (limited to 'kernel/constant.mli')
| -rw-r--r-- | kernel/constant.mli | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/kernel/constant.mli b/kernel/constant.mli index 800f95811c..c24280c405 100644 --- a/kernel/constant.mli +++ b/kernel/constant.mli @@ -10,9 +10,15 @@ open Sign (* Constants (internal representation). *) +type lazy_constant_value = + | Cooked of constr + | Recipe of (unit -> constr) + +type constant_value = lazy_constant_value ref + type constant_body = { const_kind : path_kind; - const_body : constr option; + const_body : constant_value option; const_type : typed_type; const_hyps : typed_type signature; const_constraints : constraints; @@ -22,9 +28,11 @@ val is_defined : constant_body -> bool val is_opaque : constant_body -> bool +val cook_constant : constant_value -> constr + (*s Constant declaration. *) type constant_entry= { - const_entry_body : constr; + const_entry_body : lazy_constant_value; const_entry_type : constr option } |