diff options
| author | Gaëtan Gilbert | 2020-06-22 12:55:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-25 14:14:11 +0200 |
| commit | 50361dc784c8967e7c4b254102e2cb21cb7e9f9e (patch) | |
| tree | 425cbfb89a7c1336b8bdf6fdffd404e1add68cf9 /engine/univNames.mli | |
| parent | ba355fb8eb41cd25cf7bd1ece860c93d32e5793c (diff) | |
Make compute_instance_binders internal to UState
Diffstat (limited to 'engine/univNames.mli')
| -rw-r--r-- | engine/univNames.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/univNames.mli b/engine/univNames.mli index 34a18d6b6e..da9ffc3564 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -19,8 +19,6 @@ 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] |