diff options
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 0da7c85c7..54eed5ea6 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -14,7 +14,6 @@ open Mod_subst (** {6 Constants} *) -val subst_const_def : substitution -> constant_def -> constant_def val subst_const_body : substitution -> constant_body -> constant_body (** Is there a actual body in const_body ? *) |