diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 3be72f3fd..3e7d8a9bd 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -13,15 +13,9 @@ open Sign (*s Constants (internal representation) (Definition/Axiom) *) -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 : constant_value option; + const_body : constr option; const_type : types; const_hyps : named_context; (* New: younger hyp at top *) const_constraints : constraints; @@ -31,12 +25,10 @@ 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 : lazy_constant_value; + const_entry_body : constr; const_entry_type : constr option } (*s Inductive types (internal representation). *) |