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 698b8b77c2..b8cbda7cf7 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


From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 19:11:20 +0200
Subject: Safe API for accessing universe constraints of global references.

Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
---
 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 b8cbda7cf7..8f605935db 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_context : mutual_inductive_body -> Univ.universe_context
-
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
 (* Return type as quoted by the user *)
-- 
cgit v1.2.3