From ea8185d872f242f8ebf4274ebe550ed81107150a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 12 Mar 2017 19:57:48 +0100
Subject: Making the side_effects type opaque.

We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.
---
 kernel/term_typing.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 89b5fc40e3..5330fb32ba 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,6 +12,8 @@ open Environ
 open Declarations
 open Entries
 
+type side_effects
+
 val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
@@ -29,7 +31,10 @@ val inline_entry_side_effects :
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val uniq_seff : side_effects -> side_effects
+val empty_seff : side_effects
+val add_seff : side_effect -> side_effects -> side_effects
+val concat_seff : side_effects -> side_effects -> side_effects
+val uniq_seff : side_effects -> side_effect list
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
-- 
cgit v1.2.3


From 91dbe4af7b2a435142dcf40902082f90f07cc8be Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 Mar 2017 08:48:22 +0100
Subject: Documenting the API of side-effects.

---
 kernel/term_typing.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 5330fb32ba..075389ea53 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -34,7 +34,12 @@ val inline_entry_side_effects :
 val empty_seff : side_effects
 val add_seff : side_effect -> side_effects -> side_effects
 val concat_seff : side_effects -> side_effects -> side_effects
+(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
+    [e1] must be more recent than those of [e2]. *)
 val uniq_seff : side_effects -> side_effect list
+(** Return the list of individual side-effects in the order of their
+    creation. *)
+
 val equal_eff : side_effect -> side_effect -> bool
 
 val translate_constant :
-- 
cgit v1.2.3