diff options
| author | Pierre-Marie Pédrot | 2018-09-13 13:47:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | aaee23f06e4ac345238cb84edc1c16fafe6b6b3d (patch) | |
| tree | b42f3df8504a5c258f4b5c213d1b3d47158a4a67 /engine/univNames.mli | |
| parent | 51dad02266f0bea735d496839c559b472bc4553e (diff) | |
Store universe binder names as a mere list of names.
This is the only information we care about. The printing mechanism is only
called on polymorphic constants, as the naming of global monomorphic levels
is performed in another module.
Diffstat (limited to 'engine/univNames.mli')
| -rw-r--r-- | engine/univNames.mli | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/engine/univNames.mli b/engine/univNames.mli index 837beac267..d794d7b744 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -27,15 +27,14 @@ type universe_binders = Univ.Level.t Names.Id.Map.t 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 = Names.lname list -(** [universe_binders_with_opt_names ref u l] +(** [universe_binders_with_opt_names ref l] - If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous). - May error if the lengths mismatch. + If [l] is [Some univs] return the universe binders naming the bound levels + of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. - Otherwise return [universe_binders_of_global ref]. *) + Otherwise return the bound universe names registered for [ref]. *) val universe_binders_with_opt_names : Names.GlobRef.t -> - Univ.Level.t list -> univ_name_list option -> universe_binders + univ_name_list option -> universe_binders |