diff options
| author | Pierre-Marie Pédrot | 2019-06-25 20:57:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-08 20:47:26 +0200 |
| commit | d929838be77e30db04cd91201542bb52ed3ff7fd (patch) | |
| tree | 81a49bd4863424b841963f46025409396756d0bf /kernel/term_typing.mli | |
| parent | 75de485c233dd7bbb6301b49e6702eee205977fb (diff) | |
Similar purity invariants in the kernel.
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 |