Merge PR #888: Stronger kernel types

1 files changed, 12 insertions, 5 deletions

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5bb8ceb1a5..752fdd793e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
   Environ.env -> Constr.constr -> private_constants -> Constr.constr
 val inline_private_constants_in_definition_entry :
-  Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+  Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
 val universes_of_private : private_constants -> Univ.universe_context_set list
 
@@ -94,19 +94,26 @@ val push_named_def :
 
 (** Insertion of global axioms or definitions *)
 
+type 'a effect_entry =
+| EffectEntry : private_constants effect_entry
+| PureEntry : unit effect_entry
+
 type global_declaration =
-                  (* bool: export private constants *)
-  | ConstantEntry of bool * private_constants Entries.constant_entry
+  | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constants Entries.constant_entry * private_constant_role
+  constant * private_constant_role
+
+val export_private_constants : in_section:bool ->
+  private_constants Entries.constant_entry ->
+  (unit Entries.constant_entry * 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) *)
 val add_constant :
   DirPath.t -> Label.t -> global_declaration ->
-    (constant * exported_private_constant list) safe_transformer
+    constant safe_transformer
 
 (** Adding an inductive type *)