From 316592a31b463568f5136757c3570eaa8e1f0167 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 25 Sep 2020 15:31:51 +0200
Subject: Put type-in-type flag in ugraph.

Fix #13086.
---
 kernel/uGraph.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c9fbd7f694..87b3634e28 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -16,6 +16,15 @@ type t
 val set_cumulative_sprop : bool -> t -> t
 (** Makes the system incomplete. *)
 
+val set_type_in_type : bool -> t -> t
+
+(** When [type_in_type], functions adding constraints do not fail and
+   may instead ignore inconsistent constraints.
+
+    Checking functions such as [check_leq] always return [true].
+*)
+val type_in_type : t -> bool
+
 type 'a check_function = t -> 'a -> 'a -> bool
 
 val check_leq : Universe.t check_function
@@ -25,6 +34,9 @@ val check_eq_level : Level.t check_function
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : t
 
+(** Initial universes, but keeping options such as type in type from the argument. *)
+val initial_universes_with : t -> t
+
 (** Check equality of instances w.r.t. a universe graph *)
 val check_eq_instances : Instance.t check_function
 
-- 
cgit v1.2.3