From 568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 May 2018 14:51:49 +0200
Subject: Further cleaning of the side-effect API.

We remove internal functions and types from the API.
---
 kernel/term_typing.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 79511e4253..84fc505c4f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -27,6 +27,11 @@ module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
+type side_effect = {
+  from_env : Declarations.structure_body CEphemeron.key;
+  eff      : side_eff list;
+}
+
 module SideEffects :
 sig
   type t
@@ -66,10 +71,14 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 let uniq_seff_rev = SideEffects.repr
-let uniq_seff l = List.rev (SideEffects.repr l)
+let uniq_seff l =
+  let ans = List.rev (SideEffects.repr l) in
+  List.map_append (fun { eff } -> eff) ans
 
 let empty_seff = SideEffects.empty
-let add_seff = SideEffects.add
+let add_seff mb eff effs =
+  let from_env = CEphemeron.create mb in
+  SideEffects.add { eff; from_env } effs
 let concat_seff = SideEffects.concat
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
-- 
cgit v1.2.3