From 0d9a91113c4112eece0680e433f435fdfb39ea4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Jul 2017 16:33:47 +0200 Subject: Getting rid of simple calls to AUContext.instance. This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API. --- checker/inductive.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'checker/inductive.mli') diff --git a/checker/inductive.mli b/checker/inductive.mli index 698b8b77c..b8cbda7cf 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -26,8 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool val inductive_is_cumulative : mutual_inductive_body -> bool -val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance - val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context val type_of_inductive : env -> mind_specif puniverses -> constr -- cgit v1.2.3