diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 715a83a4af..a40b65f6b9 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -21,9 +21,15 @@ open Sign (*s Constants (Definition/Axiom) *) +type constr_substituted + +val from_val : constr -> constr_substituted +val force : constr_substituted -> constr +val subst_constr_subst : substitution -> constr_substituted -> constr_substituted + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr Lazy.t option; + const_body : constr_substituted option; const_type : types; const_constraints : constraints; const_opaque : bool } |