From dd1998f1a9bc2aae2e83aa4e349318d2466b6aea Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 29 Oct 2015 15:39:20 +0100
Subject: Cleanup API and comments of 908dcd613

---
 kernel/safe_typing.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b71cd31b5c..97b74cadb9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -218,8 +218,8 @@ let empty_private_constants = []
 let add_private x xs = x :: xs
 let concat_private xs ys = xs @ ys
 let mk_pure_proof = Term_typing.mk_pure_proof
-let inline_private_constants_in_constr = Term_typing.handle_side_effects
-let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects
+let inline_private_constants_in_constr = Term_typing.inline_side_effects
+let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
 let constant_entry_of_private_constant = function
@@ -517,8 +517,7 @@ let add_constant dir l decl senv =
     match decl with
     | ConstantEntry (true, ce) ->
         let exports, ce =
-          Term_typing.validate_side_effects_for_export
-            senv.revstruct senv.env ce in
+          Term_typing.export_side_effects senv.revstruct senv.env ce in
         exports, ConstantEntry (false, ce)
     | _ -> [], decl
   in
-- 
cgit v1.2.3


From 78edfe09f34db4a28fb41a1f6fd3bb4922d09ec8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Oct 2015 15:09:14 -0400
Subject: Collect subproof universes in handle_side_effects.

---
 kernel/safe_typing.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 97b74cadb9..e0a07dcc3a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -254,7 +254,9 @@ let universes_of_private eff =
           if cb.const_polymorphic then acc
           else (Univ.ContextSet.of_context cb.const_universes) :: acc)
         acc l
-     | Entries.SEsubproof _ -> acc)
+     | Entries.SEsubproof (c, cb, e) ->
+	if cb.const_polymorphic then acc
+	else Univ.ContextSet.of_context cb.const_universes :: acc)
    [] eff
 
 let env_of_safe_env senv = senv.env
-- 
cgit v1.2.3