From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 1 Dec 2017 10:11:41 +0100
Subject: Proper nametab handling of global universe names

They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
---
 engine/termops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 07fe902220..a71bdff31e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -288,6 +288,7 @@ let has_no_evar sigma =
   with Exit -> false
 
 let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
+let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
 
 let pr_evar_universe_context ctx =
   let open UState in
-- 
cgit v1.2.3