Further cleaning of the side-effect API.

We remove internal functions and types from the API.

7 files changed, 32 insertions, 37 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 493550e5e5..53284e0e9a 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -120,6 +120,7 @@ type seff_env =
      Same as the constant_body's but not in an ephemeron *)
   | `Opaque of Constr.t * Univ.ContextSet.t ]
 
+(** Not used by the kernel. *)
 type side_effect_role =
   | Subproof
   | Schema of inductive * string
@@ -130,8 +131,3 @@ type side_eff = {
   seff_env : seff_env;
   seff_role : side_effect_role;
 }
-
-type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff list;
-}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1547a11390..f2b5ed4383 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -233,28 +233,23 @@ let make_eff env cst r =
 let private_con_of_con env c =
   let open Entries in
   let eff = [make_eff env c Subproof] in
-  let from_env = CEphemeron.create env.revstruct in
-  add_private { eff; from_env; } empty_private_constants
+  add_private env.revstruct eff empty_private_constants
 
 let private_con_of_scheme ~kind env cl =
   let open Entries in
   let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
-  let from_env = CEphemeron.create env.revstruct in
-  add_private { eff; from_env; } empty_private_constants
+  add_private env.revstruct eff empty_private_constants
 
 let universes_of_private eff =
   let open Entries in
-  let fold acc { eff } =
-    let fold acc eff =
-      let acc = match eff.seff_env with
-      | `Nothing -> acc
-      | `Opaque (_, ctx) -> ctx :: acc
-      in
-      match eff.seff_body.const_universes with
-      | Monomorphic_const ctx -> ctx :: acc
-      | Polymorphic_const _ -> acc
+  let fold acc eff =
+    let acc = match eff.seff_env with
+    | `Nothing -> acc
+    | `Opaque (_, ctx) -> ctx :: acc
     in
-    List.fold_left fold acc eff
+    match eff.seff_body.const_universes with
+    | Monomorphic_const ctx -> ctx :: acc
+    | Polymorphic_const _ -> acc
   in
   List.fold_left fold [] (Term_typing.uniq_seff eff)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c8df57911f..990e07da45 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -44,7 +44,7 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 type private_constants
 
 val side_effects_of_private_constants :
-  private_constants -> Entries.side_effect list
+  private_constants -> Entries.side_eff list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 79511e4253..84fc505c4f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -27,6 +27,11 @@ module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
+type side_effect = {
+  from_env : Declarations.structure_body CEphemeron.key;
+  eff      : side_eff list;
+}
+
 module SideEffects :
 sig
   type t
@@ -66,10 +71,14 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 let uniq_seff_rev = SideEffects.repr
-let uniq_seff l = List.rev (SideEffects.repr l)
+let uniq_seff l =
+  let ans = List.rev (SideEffects.repr l) in
+  List.map_append (fun { eff } -> eff) ans
 
 let empty_seff = SideEffects.empty
-let add_seff = SideEffects.add
+let add_seff mb eff effs =
+  let from_env = CEphemeron.create mb in
+  SideEffects.add { eff; from_env } effs
 let concat_seff = SideEffects.concat
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 3ebc41357e..b05e05e4dc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -38,11 +38,11 @@ val inline_entry_side_effects :
     yet type checked proof. *)
 
 val empty_seff : side_effects
-val add_seff : side_effect -> side_effects -> 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_effect list
+val uniq_seff : side_effects -> side_eff list
 (** Return the list of individual side-effects in the order of their
     creation. *)
 
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 05d5eaa9e9..198e057ebc 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -55,12 +55,9 @@ let add_if_undefined env eff =
   with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
 
 (* Add the side effects to the monad's environment, if not already done. *)
-let add_side_effect env { Entries.eff } =
+let add_side_effects env eff =
   List.fold_left add_if_undefined env eff
 
-let add_side_effects env effects =
-  List.fold_left (fun env eff -> add_side_effect env eff) env effects
-
 let generic_refine ~typecheck f gl =
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1b086d69cc..880a11becd 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -71,15 +71,13 @@ let adjust_guardness_conditions const = function
 	  List.interval 0 (List.length ((lam_assum c))))
 	  lemma_guard (Array.to_list fixdefs) in
 *)
-              let add c cb e =
-                let exists c e =
-                  try ignore(Environ.lookup_constant c e); true
-                  with Not_found -> false in 
-                if exists c e then e else Environ.add_constant c cb e in
-              let env = List.fold_left (fun env { eff } ->
-                let fold acc eff = add eff.seff_constant eff.seff_body acc in
-                List.fold_left fold env eff)
-                env (Safe_typing.side_effects_of_private_constants eff) in
+              let fold env eff =
+                try
+                  let _ = Environ.lookup_constant eff.seff_constant env in
+                  env
+                with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+              in
+              let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in
               let indexes =
                 search_guard env
                   possible_indexes fixdecls in