Move side-effect typing into Safe_env.

This reduces the attack surface of the API, as actually there is only a back
and forth between the two modules, and side-effects validity certificates are
intuitively nothing more than safe environments.

1 files changed, 8 insertions, 34 deletions

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ab25090b00..3dc498ca1c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,53 +14,27 @@ open Environ
 open Declarations
 open Entries
 
-type side_effects
+(** Handlers are used to manage side-effects. The ['a] type stands for the type
+    of side-effects, and it is parametric because they are only defined later
+    on. Handlers inline the provided side-effects into the term, and return
+    the set of additional global constraints that need to be added for the term
+    to be well typed. *)
+type 'a effect_handler =
+  env -> Constr.t -> Univ.ContextSet.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
 type _ trust =
 | Pure : unit trust
-| SideEffects : structure_body -> side_effects trust
+| SideEffects : 'a effect_handler -> 'a trust
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
   constr * types
 
 val translate_local_assum : env -> types -> types
 
-val mk_pure_proof : constr -> side_effects proof_output
-
-val inline_side_effects : env -> constr -> side_effects -> constr
-(** Returns the term where side effects have been turned into let-ins or beta
-    redexes. *)
-
-val inline_entry_side_effects :
-  env -> side_effects definition_entry -> unit definition_entry
-(** Same as {!inline_side_effects} but applied to entries. Only modifies the
-    {!Entries.const_entry_body} field. It is meant to get a term out of a not
-    yet type checked proof. *)
-
-val empty_seff : side_effects
-val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects
-val concat_seff : side_effects -> side_effects -> side_effects
-(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
-    [e1] must be more recent than those of [e2]. *)
-val uniq_seff : side_effects -> side_eff list
-(** Return the list of individual side-effects in the order of their
-    creation. *)
-
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     constant_body
 
-type exported_side_effect = 
-  Constant.t * 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
- * be pushed in the safe_env by safe typing.  The main constant entry
- * needs to be translated as usual after this step. *)
-val export_side_effects :
-  structure_body -> env -> side_effects definition_entry ->
-    exported_side_effect list * unit definition_entry
-
 val translate_mind :
   env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body