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 f593b4547..177ae9d45 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -59,7 +59,6 @@ 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} *) |