diff options
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 635b8c47a..0da7c85c7 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -59,6 +59,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body val join_constant_body : constant_body -> unit +val prune_constant_body : constant_body -> constant_body (** {6 Hash-consing} *) |