From d929838be77e30db04cd91201542bb52ed3ff7fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 25 Jun 2019 20:57:50 +0200
Subject: Similar purity invariants in the kernel.

---
 kernel/term_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.mli')

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
-- 
cgit v1.2.3