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 225abd60f8..ef01ece185 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -24,7 +24,7 @@ type 'a effect_handler = type _ trust = | Pure : unit trust -| SideEffects : 'a effect_handler -> 'a trust +| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust val translate_local_def : env -> Id.t -> section_def_entry -> constr * Sorts.relevance * types |