diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index a40b65f6b9..1bae20294d 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -25,7 +25,6 @@ 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 *) |