diff options
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 *) |