diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 91061c7ca3..1a5c74e682 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -69,6 +69,7 @@ let make_typed t s = { body = t; typ = s } let typed_app f tt = { body = f tt.body; typ = tt.typ } let body_of_type ty = ty.body +let level_of_type t = (t.typ : sorts) let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ))) |