diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 7dd9aa7864..fcb45befa0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -122,14 +122,6 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let set_inductive_level env s t = - let sign,s' = dest_prod_assum env t in - if family_of_sort s <> family_of_sort (destSort s') then - (* This induces reductions if user_arity <> nf_arity *) - mkArity (sign,s) - else - t - let sort_as_univ = function | Type u -> u | Prop Null -> neutral_univ |