diff options
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index a960099ed..621ca5e84 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -21,7 +21,9 @@ val pr_with_global_universes : Level.t -> Pp.t (** Local universe name <-> level mapping *) -type universe_binders = (Id.t * Univ.Level.t) list +type universe_binders = Univ.Level.t Names.Id.Map.t + +val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit val universe_binders_of_global : Globnames.global_reference -> universe_binders |