From 6e0b660b1e58502b7da477b9725ae8ee4f5d00ed 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/inductive.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 9a321e5ca6..5847d25f6f 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -35,8 +35,6 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 (** {6 Functions to build standard types related to inductive } *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
 
-val inductive_instance : mutual_inductive_body -> universe_instance
-val inductive_context : mutual_inductive_body -> universe_context
 val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
 
 val instantiate_inductive_constraints : 
-- 
cgit v1.2.3