From a2ec08199d023b102df7806db8ed1e71c3ed27ce Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Dec 2018 16:22:18 +0100
Subject: Make ugraph implementation abstract wrt universe specifics

This should give better visibility of universe specific operations vs
generic graph operations.
---
 kernel/uGraph.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4dbfac5c73..e1a5d50425 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -22,9 +22,6 @@ val check_eq_level : Level.t check_function
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : t
 
-(** Check if we are in the initial case *)
-val is_initial_universes : t -> bool
-
 (** Check equality of instances w.r.t. a universe graph *)
 val check_eq_instances : Instance.t check_function
 
-- 
cgit v1.2.3