From f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2020 14:01:00 +0200
Subject: Make explicit that UGraph lower bounds are only of two kinds.

This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
---
 library/global.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index 2acd7e2a67..2767594171 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -22,7 +22,7 @@ val env : unit -> Environ.env
 val env_is_initial : unit -> bool
 
 val universes : unit -> UGraph.t
-val universes_lbound : unit -> Univ.Level.t
+val universes_lbound : unit -> UGraph.Bound.t
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Constr.named_context
 
-- 
cgit v1.2.3