6 files changed, 10 insertions, 5 deletions
diff --git a/library/global.ml b/library/global.ml
index 5c847fda96..71cadb3600 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -105,9 +105,9 @@ let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
-let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d)
+let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d)
 let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d)
-let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
+let add_mind ?typing_flags id mie = globalize (Safe_typing.add_mind ?typing_flags (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
diff --git a/library/global.mli b/library/global.mli
index 5faf0e8bbd..c9b9d7f536 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -52,10 +52,12 @@ val export_private_constants :
   Safe_typing.exported_private_constant list
 
 val add_constant :
+  ?typing_flags:Declarations.typing_flags ->
   Id.t -> Safe_typing.global_declaration -> Constant.t
 val add_private_constant :
   Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants
 val add_mind :
+  ?typing_flags:Declarations.typing_flags ->
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
 (** Extra universe constraints *)
diff --git a/library/libnames.ml b/library/libnames.ml
index 88b2e41855..ba1ef1e2f9 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir =
   let (l,a) = split_dirpath dir in
   make_qualid ?loc l a
 
+let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v
+
 let qualid_is_ident qid =
   DirPath.is_empty qid.CAst.v.dirpath
 
diff --git a/library/libnames.mli b/library/libnames.mli
index a384510879..65aca0c87d 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid
 val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
 val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
 val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+val qualid_of_lident : lident -> qualid
 
 val qualid_is_ident : qualid -> bool
 val qualid_path : qualid -> DirPath.t
diff --git a/library/nametab.ml b/library/nametab.ml
index a51c281f2b..d5cc4f8ac5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -562,9 +562,9 @@ let shortest_qualid_of_modtype ?loc kn =
   let sp = MPmap.find kn !the_modtyperevtab in
     MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_universe ?loc kn =
+let shortest_qualid_of_universe ?loc ctx kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab
+    UnivTab.shortest_qualid ?loc ctx sp !the_univtab
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
diff --git a/library/nametab.mli b/library/nametab.mli
index 8a8b59733c..fa27dcab9a 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -206,7 +206,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid
 
 (** {5 Generic name handling} *)