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.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3e6c4858e0..5db5de21b4 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -292,13 +292,6 @@ let hcons_mind mib =
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_universes = hcons_mind_universes mib.mind_universes }
 
-(** {6 Stm machinery } *)
-
-let string_of_side_effect { Entries.eff } = match eff with
-  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")"
-  | Entries.SEscheme (cl,_) ->
-      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")"
-
 (** Hashconsing of modules *)
 
 let hcons_functorize hty he hself f = match f with
-- 
cgit v1.2.3