diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 19:11:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | 012f5fb722a9d5dcef82c800aa54ed50c0a58957 (patch) | |
| tree | fbe0e3ae6901faba4f14b8cd4dbda019ce9a7829 /checker | |
| parent | b8a7222e670f69e024d50394afd88204e15d1b29 (diff) | |
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.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/inductive.ml | 7 | ||||
| -rw-r--r-- | checker/inductive.mli | 2 |
2 files changed, 0 insertions, 9 deletions
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 *) |