From 24d0027f0344bca7abce3b8fa8c2a1e42ecf1a00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 13 Sep 2014 10:44:40 +0200
Subject: Providing a -type-in-type option for collapsing the universe
 hierarchy.

---
 library/global.ml  | 1 +
 library/global.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index adfb7cafed..80238d8e2d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,6 +77,7 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 9e47c16ff1..7dcfdbd3a0 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,6 +27,7 @@ val named_context : unit -> Context.named_context
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
+val set_type_in_type : unit -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-- 
cgit v1.2.3