From 9c678306157b2c6199091709ef7bb067f724f80c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 19 Nov 2018 18:18:26 +0100
Subject: 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.
---
 kernel/environ.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'kernel/environ.ml')

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
 
-- 
cgit v1.2.3