diff options
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 800b167ab..0c5f3584e 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -57,7 +57,7 @@ val recarg_length : wf_paths -> int -> int val subst_wf_paths : substitution -> wf_paths -> wf_paths -val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body +val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body val join_constant_body : constant_body -> unit |