diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 5929250db..0de831668 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -595,7 +595,7 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val hcons_constr: (constant -> constant) * - (kernel_name -> kernel_name) * + (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) * (name -> name) * (identifier -> identifier) * |