diff options
Diffstat (limited to 'kernel/mod_typing.mli')
| -rw-r--r-- | kernel/mod_typing.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index e3045555f..eb7dbe994 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -27,3 +27,5 @@ val add_module_constraints : env -> module_body -> env val add_struct_expr_constraints : env -> struct_expr_body -> env +val struct_expr_constraints : struct_expr_body -> Univ.constraints + |