From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 kernel/declareops.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 35490ceef9..23a44433b3 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -15,6 +15,10 @@ open Univ
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
+val universes_context : universes -> AUContext.t
+
+val abstract_universes : Entries.universes_entry -> Univ.universe_level_subst * universes
+
 (** {6 Arities} *)
 
 val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
-- 
cgit v1.2.3