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/declareops.mli | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index fb46112ea7..7170a8b642 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -11,7 +11,6 @@
 open Declarations
 open Mod_subst
 open Univ
-open Entries
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -39,10 +38,6 @@ val constant_is_polymorphic : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
-(** Side effects *)
-
-val string_of_side_effect : side_effect -> string
-
 (** {6 Inductive types} *)
 
 val eq_recarg : recarg -> recarg -> bool
-- 
cgit v1.2.3