From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jun 2016 18:25:02 +0200
Subject: Moving the typing_flags to the environment.

---
 kernel/declarations.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 639cd061bc..ef4d398c1f 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,9 +14,8 @@ open Term
    inductive definitions, modules and module types *)
 
 type set_predicativity = ImpredicativeSet | PredicativeSet
-type type_hierarchy = TypeInType | StratifiedType
 
-type engagement = set_predicativity * type_hierarchy
+type engagement = set_predicativity
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
-- 
cgit v1.2.3