From 6023b16dddfb043c6c80815c726936b02735c9cc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 27 Sep 2018 13:46:20 +0200
Subject: Simplify declaration of universe names

Declaring the universe to the kernel/section mechanism is centralized
to [Declare.declare_universe_context].
Then the universe name object really is only about the user visible
names.
---
 library/nametab.ml  | 3 +++
 library/nametab.mli | 2 ++
 2 files changed, 5 insertions(+)

(limited to 'library')

diff --git a/library/nametab.ml b/library/nametab.ml
index 840cf8e380..06ace373c3 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -30,6 +30,9 @@ let error_global_not_found qid =
 *)
 type visibility = Until of int | Exactly of int
 
+let map_visibility f = function
+  | Until i -> Until (f i)
+  | Exactly i -> Exactly (f i)
 
 (* Data structure for nametabs *******************************************)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 57e9141db9..1c3322bfb1 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -75,6 +75,8 @@ val error_global_not_found : qualid -> 'a
 
 type visibility = Until of int | Exactly of int
 
+val map_visibility : (int -> int) -> visibility -> visibility
+
 val push : visibility -> full_path -> GlobRef.t -> unit
 val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
-- 
cgit v1.2.3