diff options
| author | Gaëtan Gilbert | 2018-11-19 18:18:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-21 13:22:47 +0100 |
| commit | 9c678306157b2c6199091709ef7bb067f724f80c (patch) | |
| tree | 28bbb08c4500676b2eca478323243d867cf27c15 /kernel/environ.mli | |
| parent | 70ce3e98991a96f9d7f181a4a6f5b250457f1245 (diff) | |
Refactor typechecking of inductive types
We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 8a2efb2477..6d4d3b282b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -98,6 +98,9 @@ val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool +val is_impredicative_sort : env -> Sorts.t -> bool +val is_impredicative_univ : env -> Univ.Universe.t -> bool + (** is the local context empty *) val empty_context : env -> bool |