diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 71a6b7a39..f7464013f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -81,7 +81,8 @@ open Declarations These fields could be deduced from [revstruct], but they allow faster name freshness checks. - [univ] and [future_cst] : current and future universe constraints - - [engagement] : are we Set-impredicative ? + - [engagement] : are we Set-impredicative? + - [type_in_type] : does the universe hierarchy collapse? - [imports] : names and digests of Require'd libraries since big-bang. This field will only grow - [loads] : list of libraries Require'd inside the current module. @@ -121,6 +122,7 @@ type safe_environment = univ : Univ.constraints; future_cst : Univ.constraints Future.computation list; engagement : engagement option; + type_in_type : bool; imports : vodigest DPMap.t; loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list} @@ -143,6 +145,7 @@ let empty_environment = future_cst = []; univ = Univ.Constraint.empty; engagement = None; + type_in_type = false; imports = DPMap.empty; loads = []; local_retroknowledge = [] } @@ -179,6 +182,10 @@ let check_engagement env c = Errors.error "Needs option -impredicative-set." | _ -> () +let set_type_in_type senv = + { senv with + env = Environ.set_type_in_type senv.env; + type_in_type = true } (** {6 Stm machinery } *) |