diff options
| author | Maxime Dénès | 2019-01-21 14:15:51 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-21 14:15:51 +0100 |
| commit | b8da6225e3867408f5d1ad0c716618c4228a1ad2 (patch) | |
| tree | 28bbb08c4500676b2eca478323243d867cf27c15 /kernel/environ.ml | |
| parent | 05e2222e04323d11429d659b415750cf40e2babd (diff) | |
| parent | 9c678306157b2c6199091709ef7bb067f724f80c (diff) | |
Merge PR #9027: Refactor checking of inductive types
Ack-by: SkySkimmer
Reviewed-by: mattam82
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 38a428d9a1..77820a301e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -238,6 +238,13 @@ let is_impredicative_set env = | ImpredicativeSet -> true | _ -> false +let is_impredicative_sort env = function + | Sorts.Prop -> true + | Sorts.Set -> is_impredicative_set env + | Sorts.Type _ -> false + +let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u) + let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded |