diff options
Diffstat (limited to 'engine/univNames.mli')
| -rw-r--r-- | engine/univNames.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/engine/univNames.mli b/engine/univNames.mli index 34a18d6b6e..5f69d199b3 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -19,15 +19,4 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders -val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array - type univ_name_list = Names.lname list - -(** [universe_binders_with_opt_names ref l] - - 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 the bound universe names registered for [ref]. *) -val universe_binders_with_opt_names : AUContext.t -> - univ_name_list option -> universe_binders |