Further simplication: do not recreate entries for side-effects.

This is actually useless, the code does not depend on the value of the
entry for side-effects.

4 files changed, 8 insertions, 11 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ccd6e9cf9..04051f2e2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -502,7 +502,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * unit Entries.constant_entry * private_constant_role
+  constant * private_constant_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
@@ -528,8 +528,8 @@ let add_constant_aux no_section senv (kn, cb) =
 
 let export_private_constants ~in_section ce senv =
   let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
-  let bodies = List.map (fun (kn, cb, _, _) -> (kn, cb)) exported in
-  let exported = List.map (fun (kn, _, ce, r) -> (kn, ce, r)) exported in
+  let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+  let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
   let no_section = not in_section in
   let senv = List.fold_left (add_constant_aux no_section) senv bodies in
   (ce, exported), senv
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 715226107..148fdca67 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -103,7 +103,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * unit Entries.constant_entry * private_constant_role
+  constant * private_constant_role
 
 val export_private_constants : in_section:bool ->
   private_constants Entries.constant_entry ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 03bd8426f..23c5b6f58 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -544,7 +544,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * unit constant_entry * side_effect_role
+  constant * constant_body * side_effect_role
 
 let export_side_effects mb env ce =
   match ce with
@@ -596,7 +596,7 @@ let export_side_effects mb env ce =
              List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
                let ce = constant_entry_of_side_effect ocb u in
                let cb = translate_constant Pure env kn ce in
-               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
+               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) 
              (env,[]) cbs in
            translate_seff sl rest (cbs @ acc) env
         | Some sl, cbs :: rest ->
@@ -604,7 +604,7 @@ let export_side_effects mb env ce =
            let cbs = List.map turn_direct cbs in
            let env = List.fold_left push_seff env cbs in
            let ecbs = List.map (fun (kn,cb,u,r) ->
-             kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+             kn, cb, r) cbs in
            translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
      in
        translate_seff trusted seff [] env
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 082ed7ed0..5914c4a95 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -55,7 +55,7 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * unit constant_entry * side_effect_role
+  constant * constant_body * side_effect_role
   
 (* Given a constant entry containing side effects it exports them (either
  * by re-checking them or trusting them).  Returns the constant bodies to
@@ -65,9 +65,6 @@ val export_side_effects :
   structure_body -> env -> side_effects constant_entry ->
     exported_side_effect list * unit constant_entry
 
-val constant_entry_of_side_effect :
-  constant_body -> seff_env -> unit constant_entry
-
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body