diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9c75829d5b..012ddae775 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -80,8 +80,6 @@ val check_cofix : env -> cofixpoint -> unit val type_of_inductive_knowing_parameters : env -> one_inductive_body -> types array -> types -val set_inductive_level : env -> sorts -> types -> types - val max_inductive_sort : sorts array -> universe val instantiate_universes : env -> Sign.rel_context -> |