From d324c858be652659a5062332f00e7d20393a48be Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 12:35:49 +0200
Subject: Safe_typing.push_named_assum: don't take universes

The caller should push them first
---
 library/global.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index 51307b3604..d034bc4208 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -38,7 +38,7 @@ val sprop_allowed : unit -> bool
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_assum : (Id.t * Constr.types) -> unit
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 
 val export_private_constants : in_section:bool ->
-- 
cgit v1.2.3