diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univNames.ml | 2 | ||||
| -rw-r--r-- | engine/univNames.mli | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index 5c87fed31c..b7ccd2372f 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -53,8 +53,6 @@ let compute_instance_binders inst ubinders = in Array.map_to_list map (Instance.to_array inst) -let register_universe_binders ref ubinders = () - type univ_name_list = Names.lname list let universe_binders_with_opt_names ref names = diff --git a/engine/univNames.mli b/engine/univNames.mli index 634db9581c..b00c5fda95 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -21,8 +21,6 @@ val empty_binders : universe_binders val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list -val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit - type univ_name_list = Names.lname list (** [universe_binders_with_opt_names ref l] |