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.ml | 7 ------- checker/inductive.mli | 2 -- 2 files changed, 9 deletions(-) (limited to 'checker') diff --git a/checker/inductive.ml b/checker/inductive.ml index a145165aa..1271a02b0 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -66,13 +66,6 @@ let inductive_is_cumulative mib = | Polymorphic_ind ctx -> false | Cumulative_ind cumi -> true -let inductive_polymorphic_context mib = - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.UContext.empty - | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx - | Cumulative_ind cumi -> - Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) - (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) diff --git a/checker/inductive.mli b/checker/inductive.mli index b8cbda7cf..8f605935d 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