From 568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 May 2018 14:51:49 +0200
Subject: Further cleaning of the side-effect API.

We remove internal functions and types from the API.
---
 kernel/safe_typing.ml | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

(limited to 'kernel/safe_typing.ml')

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)
 
-- 
cgit v1.2.3