diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index cc5a8954d..787f51c63 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -65,6 +65,8 @@ type typed_term = typed_type judge val make_typed : constr -> sorts -> typed_type val typed_app : (constr -> constr) -> typed_type -> typed_type +val typed_combine : (constr -> constr -> constr) -> (sorts -> sorts -> sorts) + -> (typed_type -> typed_type -> typed_type) val body_of_type : typed_type -> constr val level_of_type : typed_type -> sorts |