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

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index e79cc60798..c6de5b2a1b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -150,8 +150,8 @@ let register_side_effect (c, role) =
   ignore(add_leaf id o);
   update_tables c;
   match role with
-  | Safe_typing.Subproof -> ()
-  | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
+  | Subproof -> ()
+  | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
 
 let declare_constant_common id cst =
   let o = inConstant cst in
-- 
cgit v1.2.3