diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 00:56:02 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 00:56:02 +0200 |
| commit | 7f0346ea0cc5d76ff7c5aa6f95cfd43769ae21aa (patch) | |
| tree | 13418ea92850981ed072e7526a99113d02a7f805 /kernel | |
| parent | bcba542aac3e17bab78f74e0fd3600e12cc0e492 (diff) | |
Remove unused type_in_type field in safe_env.
Was left over after Hugo's 9c732a5c878b.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 907ad2a1d..55e767321 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -81,8 +81,7 @@ 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? - - [type_in_type] : does the universe hierarchy collapse? + - [engagement] : are we Set-impredicative? does the universe hierarchy collapse? - [required] : 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. @@ -122,7 +121,6 @@ type safe_environment = univ : Univ.constraints; future_cst : Univ.constraints Future.computation list; engagement : engagement option; - type_in_type : bool; required : vodigest DPMap.t; loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list; @@ -152,7 +150,6 @@ let empty_environment = future_cst = []; univ = Univ.Constraint.empty; engagement = None; - type_in_type = false; required = DPMap.empty; loads = []; local_retroknowledge = []; |