Remove the side-effect role from the kernel.

We move the role data into the evarmap instead.

2 files changed, 12 insertions, 17 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 824400b4e3..0b0f14eee7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -232,7 +232,6 @@ type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
   seff_body : Constr.t Declarations.constant_body;
-  seff_role : Entries.side_effect_role;
 }
 
 module SideEffects :
@@ -536,8 +535,7 @@ type 'a effect_entry =
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
 
-type exported_private_constant = 
-  Constant.t * Entries.side_effect_role
+type exported_private_constant = Constant.t
 
 let add_constant_aux ~in_section senv (kn, cb) =
   let l = Constant.label kn in
@@ -699,7 +697,7 @@ let constant_entry_of_side_effect eff =
     const_entry_inline_code = cb.const_inline_code }
 
 let export_eff eff =
-  (eff.seff_constant, eff.seff_body, eff.seff_role)
+  (eff.seff_constant, eff.seff_body)
 
 let export_side_effects mb env (b_ctx, eff) =
       let not_exists e =
@@ -750,9 +748,9 @@ let n_univs cb = match cb.const_universes with
 
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
+  let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
   let bodies = List.map map exported in
-  let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
+  let exported = List.map (fun (kn, _) -> kn) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
@@ -762,7 +760,7 @@ let add_recipe ~in_section l r senv =
   let senv = add_constant_aux ~in_section senv (kn, cb) in
   kn, senv
 
-let add_constant ?role ~in_section l decl senv =
+let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
     let cb = 
       match decl with
@@ -786,9 +784,9 @@ let add_constant ?role ~in_section l decl senv =
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  let eff = match role with
-  | None -> empty_private_constants
-  | Some role ->
+  let eff : a = match side_effect with
+  | PureEntry -> ()
+  | EffectEntry ->
     let body, univs = match cb.const_body with
     | (Primitive _ | Undef _) -> assert false
     | Def c -> (Def c, cb.const_universes)
@@ -808,7 +806,6 @@ let add_constant ?role ~in_section l decl senv =
       from_env = from_env;
       seff_constant = kn;
       seff_body = cb;
-      seff_role = role;
     } in
     SideEffects.add eff empty_private_constants
   in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 770caf5406..3e902303c3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -87,18 +87,16 @@ type 'a effect_entry =
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
 
-type exported_private_constant = 
-  Constant.t * Entries.side_effect_role
+type exported_private_constant = Constant.t
 
 val export_private_constants : in_section:bool ->
   private_constants Entries.proof_output ->
   (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
 
-(** returns the main constant plus a list of auxiliary constants (empty
-    unless one requires the side effects to be exported) *)
+(** returns the main constant plus a certificate of its validity *)
 val add_constant :
-  ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
-    (Constant.t * private_constants) safe_transformer
+  side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
+    (Constant.t * 'a) safe_transformer
 
 val add_recipe :
   in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer