diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 94ce20615e..46bcebcd84 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -59,6 +59,8 @@ type 'a judge = { body : constr; typ : 'a } type typed_type = sorts judge type typed_term = typed_type judge +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 |