diff options
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 497856676..ad3e8be4f 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -75,8 +75,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val join_constant_body : Opaqueproof.opaquetab -> constant_body -> unit - (** {6 Hash-consing} *) (** Here, strictly speaking, we don't perform true hash-consing |