From 929ecfe0cd8cd3edec41416491e286e4c105ffa6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Jun 2019 16:50:32 +0200
Subject: Move the side-effect role out of Entries into Evd.

---
 kernel/entries.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index adb3f6bd29..45b11e97ba 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -107,8 +107,3 @@ type module_entry =
   | MType of module_params_entry * module_struct_entry
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
-
-(** Not used by the kernel. *)
-type side_effect_role =
-  | Subproof
-  | Schema of inductive * string
-- 
cgit v1.2.3