diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 77d126074..29c991837 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -15,7 +15,7 @@ open Entries type side_effects val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> - constant_def * types * constant_universes + constant_def * types * Univ.universe_context val translate_local_assum : env -> types -> types |