From e42b3b188b365159a60851bb0d4214068bb74dd4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 May 2018 11:16:32 +0200
Subject: Share the role type between the implementations of side-effects.

We simply exploit a type isomorphism to remove the use of dedicated algebraic
types in the kernel which are actually not necessary.
---
 kernel/term_typing.mli | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 6a0ff072f5..3ebc41357e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -46,16 +46,10 @@ 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 :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     constant_body
 
-type side_effect_role =
-  | Subproof
-  | Schema of inductive * string
-
 type exported_side_effect = 
   Constant.t * constant_body * side_effect_role
   
-- 
cgit v1.2.3


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.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 3ebc41357e..b05e05e4dc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -38,11 +38,11 @@ val inline_entry_side_effects :
     yet type checked proof. *)
 
 val empty_seff : side_effects
-val add_seff : side_effect -> side_effects -> side_effects
+val add_seff : Declarations.structure_body -> Entries.side_eff list -> 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
+val uniq_seff : side_effects -> side_eff list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
-- 
cgit v1.2.3