From 7f0346ea0cc5d76ff7c5aa6f95cfd43769ae21aa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:56:02 +0200
Subject: Remove unused type_in_type field in safe_env.

Was left over after Hugo's 9c732a5c878b.
---
 kernel/safe_typing.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 907ad2a1d4..55e767321b 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 = [];
-- 
cgit v1.2.3