From 9f5586d88880cbb98c92edfe9c33c76564f1a19c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 16 Jan 2015 22:17:03 +0100
Subject: Make native compiler handle universe polymorphic definitions.

One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
---
 kernel/declareops.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/declareops.mli')

diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 02090ade5d..47a82cc6c0 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -8,6 +8,8 @@
 
 open Declarations
 open Mod_subst
+open Univ
+open Context
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -75,6 +77,9 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
 
+val inductive_instance : mutual_inductive_body -> universe_instance
+val inductive_context : mutual_inductive_body -> universe_context
+
 (** {6 Hash-consing} *)
 
 (** Here, strictly speaking, we don't perform true hash-consing
-- 
cgit v1.2.3