diff options
Diffstat (limited to 'engine/univNames.ml')
| -rw-r--r-- | engine/univNames.ml | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index 6e59a7c9e..a68840174 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -14,18 +14,19 @@ open Globnames open Nametab -let reference_of_level l = CAst.make @@ +let qualid_of_level l = match Level.name l with | Some (d, n as na) -> - let qid = - try Nametab.shortest_qualid_of_universe na - with Not_found -> - let name = Id.of_string_soft (string_of_int n) in - Libnames.make_qualid d name - in Libnames.Qualid qid - | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l)) + begin + try Nametab.shortest_qualid_of_universe na + with Not_found -> + let name = Id.of_string_soft (string_of_int n) in + Libnames.make_qualid d name + end + | None -> + Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l) -let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) +let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) @@ -89,7 +90,7 @@ let register_universe_binders ref ubinders = if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) -type univ_name_list = Misctypes.lname list +type univ_name_list = Names.lname list let universe_binders_with_opt_names ref levels = function | None -> universe_binders_of_global ref |