From 665256fec8465ff0adb943063c25f07a6ca54618 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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/safe_typing.mli | 2 +-
 kernel/term_typing.ml  | 2 +-
 kernel/term_typing.mli | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 148fdca678..752fdd793e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
   Environ.env -> Constr.constr -> private_constants -> Constr.constr
 val inline_private_constants_in_definition_entry :
-  Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+  Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
 val universes_of_private : private_constants -> Univ.universe_context_set list
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 23c5b6f58e..ed53df01f1 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 =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 5914c4a954..24153343e7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr
     redexes. *)
 
 val inline_entry_side_effects :
-  env -> side_effects definition_entry -> side_effects definition_entry
+  env -> side_effects definition_entry -> unit definition_entry
 (** Same as {!inline_side_effects} but applied to entries. Only modifies the
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
-- 
cgit v1.2.3