diff options
Diffstat (limited to 'engine/univNames.mli')
| -rw-r--r-- | engine/univNames.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/univNames.mli b/engine/univNames.mli index e3bc3193d..837beac26 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -11,7 +11,7 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t -val reference_of_level : Level.t -> Libnames.reference +val qualid_of_level : Level.t -> Libnames.qualid (** Global universe information outside the kernel, to handle polymorphic universes in sections that have to be discharged. *) @@ -29,7 +29,7 @@ val empty_binders : universe_binders val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit val universe_binders_of_global : Names.GlobRef.t -> universe_binders -type univ_name_list = Misctypes.lname list +type univ_name_list = Names.lname list (** [universe_binders_with_opt_names ref u l] |