From 1e83ae578feea41d34c3ba26a1f74c3c715620a2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 22 May 2019 17:46:37 +0200
Subject: More precise type for Safe_typing export and inlining of private
 constants.

We get rid of the future wrappers, as all callers are immediately forcing
the result.
---
 library/global.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index aa9fc18477..eaa76c3117 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -42,8 +42,8 @@ val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 
 val export_private_constants : in_section:bool ->
-  Safe_typing.private_constants Entries.definition_entry ->
-  unit Entries.definition_entry * Safe_typing.exported_private_constant list
+  Safe_typing.private_constants Entries.proof_output ->
+  Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
 
 val add_constant :
   ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants
-- 
cgit v1.2.3