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.

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