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 2ab03e50fe..5d75df4bf2 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -208,6 +208,7 @@ type ('constr, 'types) kind_of_term = term *) val kind_of_term : constr -> (constr, types) kind_of_term +val kind_of_term2 : constr -> ((constr,types) kind_of_term,constr) kind_of_term (* Experimental *) type ('constr, 'types) kind_of_type = |