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.

5 files changed, 20 insertions, 28 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index d82b8f215..70f422b51 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -102,11 +102,12 @@ let declare_variable id obj =
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
-  cst_decl : global_declaration;
+  cst_decl : global_declaration option;
+  (** [None] when the declaration is a side-effect and has already been defined
+      in the global environment. *)
   cst_hyps : Dischargedhypsmap.discharged_hyps;
   cst_kind : logical_kind;
   cst_locl : bool;
-  cst_was_seff : bool;
 }
 
 type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
@@ -146,13 +147,14 @@ let cache_constant ((sp,kn), obj) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' =
-    if obj.cst_was_seff then begin
+    match obj.cst_decl with
+    | None ->
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
-    end else
+    | Some decl ->
       let () = check_exists sp in
-      Global.add_constant dir id obj.cst_decl
+      Global.add_constant dir id decl
   in
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
@@ -174,19 +176,14 @@ let discharge_constant ((sp, kn), obj) =
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
   let abstract = (named_of_variable_context hyps, subst, uctx) in
   let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
-  Some { obj with cst_was_seff = false; cst_hyps = new_hyps; cst_decl = new_decl; }
+  Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = 
-  ConstantEntry
-    (PureEntry, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
-
 let dummy_constant cst = {
-  cst_decl = dummy_constant_entry;
+  cst_decl = None;
   cst_hyps = [];
   cst_kind = cst.cst_kind;
   cst_locl = cst.cst_locl;
-  cst_was_seff = false;
 }
 
 let classify_constant cst = Substitute (dummy_constant cst)
@@ -249,13 +246,12 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
       export, ConstantEntry (PureEntry, cd)
     | _ -> [], ConstantEntry (EffectEntry, cd)
   in
-  let iter_eff (c, cd, role) =
+  let iter_eff (c, role) =
     let o = inConstant {
-      cst_decl = ConstantEntry (PureEntry, cd);
+      cst_decl = None;
       cst_hyps = [] ;
       cst_kind = IsProof Theorem;
       cst_locl = false;
-      cst_was_seff = true
     } in
     let id = Label.to_id (pi3 (Constant.repr3 c)) in
     ignore(add_leaf id o);
@@ -267,11 +263,10 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
   in
   let () = List.iter iter_eff export in
   let cst = {
-    cst_decl = decl;
+    cst_decl = Some decl;
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
-    cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
   let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
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