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