From 665256fec8465ff0adb943063c25f07a6ca54618 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 18 Jul 2017 18:16:43 +0200
Subject: Statically ensuring that inlined entries out of the kernel have no
 effects.

This was an easy to prove property that I somehow overlooked.
---
 kernel/term_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 23c5b6f58..ed53df01f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -654,7 +654,7 @@ let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
-      (body, ctx'), empty_seff);
+      (body, ctx'), ());
 }
 
 let inline_side_effects env body side_eff =
-- 
cgit v1.2.3