diff options
| author | Maxime Dénès | 2019-07-11 08:53:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-07-11 08:53:55 +0200 |
| commit | 195772efccbac6663501bd5fff63c318d22ee191 (patch) | |
| tree | 604d2f22f6f02958d1d5c6b629478ee7be604961 /kernel/term_typing.mli | |
| parent | 727ba947a05d5e20ee49ef633ce5cadccc35ac57 (diff) | |
| parent | 0b2b3e2baa3e004bf937ea001635b47ed781c9db (diff) | |
Merge PR #10439: Uniform handling of side-effects for opaque definitions
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
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 |